Featured Weighted Automata

TL;DR

This paper introduces featured weighted automata, combining feature-annotated transition systems with weighted automata, enabling the analysis of quantitative properties across all feature configurations simultaneously.

Contribution

It extends weighted automata to include feature annotations, providing algorithms to compute properties for all feature sets at once, with applications to reachability and energy analysis.

Findings

Algorithms for featured weighted automata are developed.

Methods extend weighted automata techniques to feature-rich models.

Applications include minimum reachability and energy property analysis.

Abstract

A featured transition system is a transition system in which the transitions are annotated with feature expressions: Boolean expressions on a finite number of given features. Depending on its feature expression, each individual transition can be enabled when some features are present, and disabled for other sets of features. The behavior of a featured transition system hence depends on a given set of features. There are algorithms for featured transition systems which can check their properties for all sets of features at once, for example for LTL or CTL properties. Here we introduce a model of featured weighted automata which combines featured transition systems and (semiring-) weighted automata. We show that methods and techniques from weighted automata extend to featured weighted automata and devise algorithms to compute quantitative properties of featured weighted automata for all sets of features at once. We show applications to minimum reachability and to energy properties.

Equations

$$|\mathcal{S}|=\inf \{w(\pi )\mid \pi \text{ accepting finite path in S}\}.$$

$$x(y\oplus z)=xy\oplus xz(y\oplus z)x=yx\oplus zx0\otimes x=0=x\otimes 0$$

$$|\mathcal{S}|=⨁\{w(\pi )\mid \pi \text{ accepting finite path in S}\}$$

$$x\big{(}\bigoplus_{n\geq 0}y^{n}\big{)}z=\bigoplus_{n\geq 0}xy^{n}z$$

$$M^{\ast }=\left[\begin{array}{cc}(a\oplus b{d}^{\ast }c{)}^{\ast }& (a\oplus b{d}^{\ast }c{)}^{\ast }b{d}^{\ast }\\ (d\oplus c{a}^{\ast }b{)}^{\ast }c{a}^{\ast }& (d\oplus c{a}^{\ast }b{)}^{\ast }\end{array}\right].$$

$$\text{for all }x\le y:f(y)-f(x)\ge y-x.$$

$$(x\oplus y)v$$

$$(xy)v$$

$$x\otimes 0$$

$$x{y}^{\ast }v=\underset{n\ge 0}{⨁}x{y}^{n}v.$$

$$M_i^{\omega }=\underset{1\le k_1,k_2,\dots \le n}{⨁}{M}_{i,k_1}{M}_{k_1,k_2}\cdots$$

$$M^{\omega }=\left[\begin{array}{c}(a\oplus b{d}^{\ast }c{)}^{\omega }\oplus (a\oplus b{d}^{\ast }c{)}^{\ast }b{d}^{\omega }\\ (d\oplus c{a}^{\ast }b{)}^{\omega }\oplus (d\oplus c{a}^{\ast }b{)}^{\ast }c{a}^{\omega }\end{array}\right].$$

$$M^{{\omega }_k}=\left[\begin{array}{c}(a\oplus b{d}^{\ast }c{)}^{\omega }\\ d^{\ast }c(a\oplus b{d}^{\ast }c{)}^{\omega }\end{array}\right].$$

$$\Vert \mathcal{S}\Vert =⨁\{w(\pi )\mid \pi \text{ Bu¨chi accepting infinite path in S}\}$$

$$\Vert \mathcal{S}\Vert =\alpha M^{{\omega }_k}.$$

$$f^{\omega }(x)=\{\begin{array}{ll}\text{ff}& \text{if }x=\perp \text{ or }f(x)<x,\\ \text{tt}& \text{otherwise}.\end{array}$$

$$\displaystyle\big{(}\phi_{1}\phi_{2}^{*}\phi_{3}\big{)}(p)$$

$$={\varphi }_1(p){\varphi }_2(p{)}^{\ast }{\varphi }_3(p)$$

$$\displaystyle=\phi_{1}(p)\big{(}\bigoplus_{n\geq 0}\phi_{2}(p)^{n}\big{)}\phi_{3}(p)$$

$$=\underset{n\ge 0}{⨁}{\varphi }_1(p){\varphi }_2(p{)}^n{\varphi }_3(p)$$

$$=\underset{n\ge 0}{⨁}{\varphi }_1(p){\varphi }_2^n(p){\varphi }_3(p)$$

$$\displaystyle=\big{(}\bigoplus_{n\geq 0}\phi_{1}\phi_{2}^{n}\phi_{3}\big{)}(p)$$

Full text

Here we introduce a model of featured weighted automata which combines featured transition systems and (semiring-) weighted automata. We show that methods and techniques from weighted automata extend to featured weighted automata and devise algorithms to compute quantitative properties of featured weighted automata for all sets of features at once. We show applications to minimum reachability and to energy properties.

††conference: FormaliSE; May 2017; Buenos Aires, Argentina††journalyear: 2017

1. Introduction

A featured transition system (DBLP:journals/tse/ClassenCSHLR13, ) is a transition system in which the transitions are annotated with feature expressions: Boolean expressions involving a finite number of given features. Depending on its feature expression, each individual transition can be enabled when some features are present, and disabled for other sets of features. For any set of features, a given featured transition system projects to a transition system which contains precisely the transitions which are enabled for that set of features.

Standard problems such as reachability or safety can be posed for featured transition systems, where the interest now is to check these properties for all sets of features at once. Hence, for example for reachability, given a featured transition system and a set of accepting states, one wants to construct a feature expression $\phi$ such that an accepting state is reachable iff the set of features satisfies $\phi$.

For quantitative properties of transition systems, the model of (semiring-) weighted automata has proven useful (book/DrosteKV09, ). This provides a uniform framework to treat problems such as minimum reachability, maximum flow, energy problems (DBLP:journals/corr/EsikFL15a, ), and others. Here we extend techniques from weighted automata to featured weighted automata, i.e., weighted automata in which the transitions are annotated with feature expressions. This extension makes it possible to check quantitative properties for all sets of features at once.

To be precise, a featured transition system induces a (projection) function from sets of features to transition systems, mapping each set of features to the behavior under these features. Similarly, we will define projections of featured weighted automata, mapping sets of features to weighted automata. Values of weighted automata are an abstract encoding of their behavior; we will see how to compute values of featured weighted automata as functions from feature expressions to behaviors.

We also develop an application of our techniques to featured energy problems. Energy problems are important in areas such as embedded systems or autonomous systems. They are concerned with the question whether a given system admits infinite schedules during which (1) certain tasks can be repeatedly accomplished and (2) the system never runs out of energy (or other specified resources). Starting with (DBLP:conf/formats/BouyerFLMS08, ), formal modeling and analysis of such problems has attracted some attention (conf/ictac/FahrenbergJLS11, ; DBLP:conf/lata/Quaas11, ; DBLP:conf/icalp/ChatterjeeD10, ; DBLP:conf/hybrid/BouyerFLM10, ; DBLP:conf/atva/EsikFLQ13, ; DBLP:conf/qest/BouyerLM12, ; DBLP:conf/csl/DegorreDGRT10, ).

Featured transition systems have applications in software product lines, where they are used as abstract representations of the behaviors of variability models (DBLP:journals/csur/ThumAKSS14, ). This representation allows one to analyze all behaviors of a software product line at once, as opposed to analyzing each product on its own. Similarly, featured weighted automata can be used as abstract representations of quantitative behaviors of software product lines, and the present work enables analysis of quantitative behaviors of all products in a software product line at once.

Contributions and structure of the paper.

We start in Sect. 2 by revisiting minimum reachability in featured transition systems with transitions weighted by real numbers. This has to some extent already been done in (DBLP:conf/icse/CordySHL13, ), but we reformulate it in order to prepare for the generalization in the following sections.

In Sect. 3, we introduce featured weighted automata and show some first examples. Instead of semirings, we will work with (featured) automata weighted in ∗-continuous Kleene algebras; this is for convenience of presentation only, and all our work (except for Sect. 5) can be extended to a more general (for example non-idempotent) setting. In Sect. 4, we then show how methods and techniques from weighted automata can be transferred to featured weighted automata.

In the last Sect. 5, we extend our results to develop an application to featured energy problems. This is based on the recent result in (DBLP:journals/corr/EsikFL15a, ) that energy problems can be stated as Büchi problems in automata weighted in ∗-continuous Kleene $\omega$-algebras, which are certain types of semimodules over ∗-continuous Kleene algebras; hence we need to extend our results to such semimodules.

The paper is followed by a separate appendix which contains some of the proofs of our results.

2. Minimum Reachability in Real-Weighted Featured Automata

A real-weighted automaton $\mathcal{S}=(S,I,F,T)$ consists of a finite set $S$ of states, subsets $I,F\subseteq S$ of initial and accepting states, and a finite set $T\subseteq S\times\mathbbm{R}_{\geq 0}\times S$ of weighted transitions. Here $\mathbbm{R}_{\geq 0}$ denotes the set of non-negative real numbers.

A finite path in such a real-weighted automaton $\mathcal{S}$ is a finite alternating sequence $\pi=(s_{0},x_{0},s_{1},x_{1},\dotsc,x_{k},s_{k+1})$ of transitions $(s_{0},x_{0},s_{1}),\dotsc,(s_{k},x_{k},s_{k+1})\in T$. The weight of $\pi$ is the sum $w(\pi)=x_{0}+\dotsm+x_{k}\in\mathbbm{R}_{\geq 0}$. A finite path $\pi$ as above is said to be accepting if $s_{0}\in I$ and $s_{k+1}\in F$. The minimum reachability problem for real-weighted automata asks, given a real-weighted automaton $\mathcal{S}$ as above, to compute the value

[TABLE]

That is, $|\mathcal{S}|$ is the minimum weight of all finite paths from an initial to an accepting state in $\mathcal{S}$. This being a multi-source-multi-target shortest path problem, it can for example be solved using the Floyd-Warshall relaxation algorithm.

Let $N$ be a set of features and $\textit{px}\subseteq 2^{N}$ a set of products over $N$. A feature guard is a Boolean expression over $N$, and we denote the set of these by $\mathbbm{B}(N)$. We write $p\models\gamma$ if $p\in\textit{px}$ satisfies $\gamma\in\mathbbm{B}(N)$ and $\llbracket\gamma\rrbracket=\{p\in\textit{px}\mid p\models\gamma\}$. Note that $\llbracket\gamma\rrbracket$ is a set of sets of features.

Definition 2.1.

A real-weighted featured automaton $(S,I,F,T,\gamma)$ consists of a finite set $S$ of states, subsets $I,F\subseteq S$ of initial and accepting states, a finite set $T\subseteq S\times\mathbbm{R}_{\geq 0}\times S$ of weighted transitions, and a feature guard mapping $\gamma:T\to\mathbbm{B}(N)$.

The projection of a real-weighted featured automaton $\mathcal{F}=$ $(S,I,F,T,\gamma)$ to a product $p\in\textit{px}$ is the real-weighted automaton $\textup{{proj}}_{p}(\mathcal{F})=(S,I,F,T^{\prime})$ with $T^{\prime}=\{t\in T\mid p\models\gamma(t)\}$.

For each product $p\in\textit{px}$, we could solve the shortest path problem in $\textup{{proj}}_{p}(\mathcal{F})$ by computing $|\textup{{proj}}_{p}(\mathcal{F})|$. Instead, we develop an algorithm which computes all these values at the same time. Its output will, thus, be a function $|\mathcal{F}|:\textit{px}\to\mathbbm{R}_{\geq 0}$, with the property that for every $p\in\textit{px}$, $|\mathcal{F}|(p)=|\textup{{proj}}_{p}(\mathcal{F})|$.

As a symbolic representation of functions $\textit{px}\to\mathbbm{R}_{\geq 0}$, we use injective functions from guard partitions to $\mathbbm{R}_{\geq 0}$. Intuitively, a guard partition is a set of feature guards which partitions px into classes such that within each class, $f$ has the same value for all products, and between different classes, $f$ has different values.

Definition 2.2.

A guard partition of px is a set $P\subseteq\mathbbm{B}(N)$ such that $\llbracket\bigvee P\rrbracket=\textit{px}$, $\llbracket\gamma\rrbracket\neq\emptyset$ for all $\gamma\in P$, and $\llbracket\gamma_{1}\rrbracket\cap\llbracket\gamma_{2}\rrbracket=\emptyset$ for all $\gamma_{1},\gamma_{2}\in P$ with $\gamma_{1}\neq\gamma_{2}$. The set of all guard partitions of px is denoted $\textit{GP}\subseteq 2^{\mathbbm{B}(N)}$.

A guard partition is a logical analogue to a partition of the set of products px: any guard partition induces a partition of px, and any partition of px can be obtained by a guard partition. In particular, for any guard partition $P$ and any product px, there is precisely one $\gamma\in P$ for which $\textit{px}\models\gamma$.

Let $\textit{GP}[\mathbbm{R}_{\geq 0}]=\{f:P\to\mathbbm{R}_{\geq 0}\mid P\in\textit{GP},\forall\gamma_{1},\gamma_{2}\in P:\gamma_{1}\neq\gamma_{2}\Rightarrow f(\gamma_{1})\neq f(\gamma_{2})\}$ denote the set of injective functions from guard partitions to $\mathbbm{R}_{\geq 0}$.

We use injective functions $P\to\mathbbm{R}_{\geq 0}$ as symbolic representations of functions $\textit{px}\to\mathbbm{R}_{\geq 0}$, because they provide the most concise such representation. Indeed, if a function $f:P\to\mathbbm{R}_{\geq 0}$ is not injective, then there are feature guards $\gamma_{1},\gamma_{2}\in P$ for which $f(\gamma_{1})=f(\gamma_{2})$, so we can obtain a more concise representation of $f$ by letting $P^{\prime}=P\setminus\{\gamma_{1},\gamma_{2}\}\cup\{\gamma_{1}\lor\gamma_{2}\}$ and $f^{\prime}:P^{\prime}\to\mathbbm{R}_{\geq 0}$ be defined by $f^{\prime}(\delta)=f(\delta)$ for $\delta\neq\gamma_{1}\lor\gamma_{2}$ and $f^{\prime}(\gamma_{1}\lor\gamma_{2})=f(\gamma_{1})$.

We show in Fig. 1 an algorithm to compute a symbolic representation of $|\mathcal{F}|$. The algorithm performs, in lines 14 to 17, a symbolic Floyd-Warshall relaxation to compute a matrix $D$ which as entries $D(i,j)$ has functions in $\textit{GP}[\mathbbm{R}_{\geq 0}]$ that for each product return the shortest path from state $s_{i}$ to state $s_{j}$.

The relaxation procedure Relax($i,j,k$) is performed by comparing $D(i,j)$ to the sum $D(i,k)+D(k,j)$ and updating $D(i,j)$ if the sum is smaller. The result of the comparison depends on the products for which the different paths are enabled, hence the comparison and update are done for each feature expression $\gamma_{1}$ in the partition for $D(i,j)$ and all feature expressions $\gamma_{2}$, $\gamma_{3}$ in the partitions for $D(i,k)$ and $D(k,j)$, respectively. The comparison has to be done only if these partitions overlap (line 32), and in case the sum is smaller, $D(i,j)$ is updated in a call to a split-and-combine procedure.

Using the procedure Split, in lines 35 to 44, $D(i,j)$ is updated at the $\gamma_{1}\land(\gamma_{2}\land\gamma_{3})$ part of its partition. If $\llbracket\gamma_{1}\land(\gamma_{2}\land\gamma_{3})\rrbracket$ is not smaller than $\llbracket\gamma_{1}\rrbracket$ (line 36), then $D(i,j)(\gamma_{1})$ is set to its new value. Afterwards, we need to call a Combine procedure to see whether $D(i,j)$ has the same value at any other part $\delta$ of its partition (line 48) and, in the affirmative case, to update the partition of $D(i,j)$ by joining the two parts (line 50f).

If the feature expression $\gamma_{1}\land(\gamma_{2}\land\gamma_{3})$ on which to update $D(i,j)$ is a strict subset of $\gamma_{1}$ (line 39), then the $\gamma_{1}$ part of the partition of $D(i,j)$ needs to be split into two parts: $\gamma_{1}\land(\gamma_{2}\land\gamma_{3})$, on which $D(i,j)$ is to be updated, and $\gamma_{1}\land\neg(\gamma_{2}\land\gamma_{3})$, on which its value stays the same. Again, we need to call the Combine procedure afterwards to potentially combine feature expressions in the partition of $D(i,j)$.

Once relaxation has finished in line 18, we need to find $f:=\min\{D(i,j)\mid s_{i}\in I,s_{j}\in F\}$. As this again depends on which features are present, we need to compute this minimum in a way similar to what we did in the Relax procedure: for each feature expression in the partition $P$ of $f$ and each overlapping feature expression in the partition of $D(i,j)$, we compare the two values and use the Split procedure to update $f$ if $D(i,j)$ is smaller.

A variant of the algorithm in Fig. 1 has been implemented in (DBLP:conf/splc/OlaecheaFAL16, ), as part of an effort to compute minimum limit-average cost in real-weighted featured automata. Several experiments in (DBLP:conf/splc/OlaecheaFAL16, ) show that our algorithm is significantly faster than an approach which separately solves the minimum reachability problem for each product.

3. Featured Weighted Automata

We proceed to introduce a generalization of the setting in the previous section. Here $\mathbbm{R}_{\geq 0}$ is replaced by an abstract ∗-continuous Kleene algebra. This allows us to develop an abstract setting for analysis of featured weighted automata, and to re-use our techniques developed in the previous section to solve quantitative problems in other concrete settings.

3.1. Weighted Automata

Recall that a semiring (book/DrosteKV09, ) $K=(K,\oplus,\otimes,0,1)$ consists of a commutative monoid $(K,\oplus,0)$ and a monoid $(K,\otimes,1)$ such that the distributive and zero laws

[TABLE]

hold for all $x,y,z\in K$ (here we have omitted the multiplication sign $\otimes$ in some expressions, and we shall also do so in the future). It follows that the product distributes over all finite sums.

A (finite) weighted automaton (book/DrosteKV09, ) over a semiring $K$ (or a $K$-weighted automaton for short) is a tuple $\mathcal{S}=(S,I,F,T)$ consisting of a finite set $S$ of states, a subset $I\subseteq S$ of initial states, a subset $F\subseteq S$ of accepting states, and a finite set $T\subseteq S\times K\times S$ of transitions.

A finite path in such a $K$-weighted automaton $\mathcal{S}=(S,I,F,T)$ is a finite alternating sequence $\pi=(s_{0},x_{0},s_{1},\dotsc,x_{k},s_{k+1})$ of transitions $(s_{0},x_{0},s_{1}),\dotsc,(s_{k},x_{k},s_{k+1})\in T$. The weight of $\pi$ is the product $w(\pi)=x_{0}\dotsm x_{k}\in K$. A finite path $\pi$ as above is said to be accepting if $s_{0}\in I$ and $s_{k+1}\in F$. The reachability value $|\mathcal{S}|$ of $\mathcal{S}$ is defined to be the sum of the weights of all its accepting finite paths:

[TABLE]

As the set of accepting finite paths generally will be infinite, one has to assume that such sums exist in $K$ for this definition to make sense. This is the subject of Sect. 3.4 below.

3.2. Examples

The Boolean semiring is $\mathbbm{B}=(\{\textup{{ff}},\textup{{tt}}\},\mathord{\lor},\mathord{\land},\textup{{ff}},\textup{{tt}})$, with disjunction as $\oplus$ and conjunction as $\otimes$. A $\mathbbm{B}$-weighted automaton $\mathcal{S}$ hence has its transitions annotated with ff or tt. For a finite path $\pi=(s_{0},x_{0},s_{1},\dotsc,x_{k},s_{k+1})$, we have $w(\pi)=\textup{{tt}}$ iff all $x_{0}=\dotsm=x_{k}=\textup{{tt}}$. Hence $|\mathcal{S}|=\textup{{tt}}$ iff there exists an accepting finite path in $\mathcal{S}$ which involves only tt-labeled transitions. That is, $\mathbbm{B}$-weighted automata are equivalent to ordinary (unlabeled) automata, where the equivalence consists in removing all ff-labeled transitions.

The tropical semiring is $\mathbbm{T}=(\mathbbm{R}_{\geq 0}\cup\{\infty\},\mathord{\wedge},\mathord{+},\infty,0)$, where $\mathbbm{R}_{\geq 0}\cup\{\infty\}$ denotes the set of extended real numbers, with minimum as $\oplus$ and addition as $\otimes$. The weight of a finite path is now the sum of its transition weights, and the reachability value of a $\mathbbm{T}$-weighted automaton is the minimum of all its accepting finite paths’ weights. Hence $\mathbbm{T}$-weighted automata are precisely the real-weighted automata of Sect. 2, and to compute their reachability values is to solve the minimum reachability problem.

The fuzzy semiring is $\mathbbm{F}=(\mathbbm{R}_{\geq 0}\cup\{\infty\},\mathord{\vee},\mathord{\wedge},0,\infty)$, with maximum as $\oplus$ and minimum as $\otimes$. Here, the weight of a finite path is the minimum of its transition weights, and the reachability value of an $\mathbbm{F}$-weighted automaton is the maximum of all its accepting finite paths’ weights. This value is hence the maximum flow in a weighted automaton: the maximum available capacity along any finite path from an initial to a accepting state.

3.3. Featured Weighted Automata

We now extend weighted automata with features, for modeling quantitative behavior of software product lines. Let $K$ be a semiring and denote by $\textit{GP}[K]=\{f:P\to K\mid P\in\textit{GP},\forall\gamma_{1},\gamma_{2}\in P:\gamma_{1}\neq\gamma_{2}\Rightarrow f(\gamma_{1})\neq f(\gamma_{2})\}$ the set of injective functions from guard partitions to $K$.

Definition 3.1.

A featured weighted automaton over $K$ and px is a tuple $(S,I,F,T)$ consisting of a finite set $S$ of states, subsets $I,F\subseteq S$ of initial and accepting states, and a finite set $T\subseteq S\times\textit{GP}[K]\times S$ of transitions.

Similarly to what we did in Sect. 2, the transition labels in $\textit{GP}[K]$ are to be seen as syntactic representations of functions from products to $K$; we will say more about this below.

Example 3.2.

For $K=\mathbbm{B}$ the Boolean semiring, featured $\mathbbm{B}$-weighted automata are standard (unlabeled) featured automata: for any feature guard $\gamma\in\mathbbm{B}(N)$, $\{\gamma,\neg\gamma\}$ is a guard partition of px, moreover, for $K=\mathbbm{B}$, any mapping in $\textit{GP}[K]$ is equivalent to one from such a guard partition. Hence transitions labeled with feature guards (as in standard featured automata) are the same as transitions labeled with functions from guard partitions to $\{\textup{{ff}},\textup{{tt}}\}$.

Definition 3.3.

For $f:P\to K\in\textit{GP}[K]$ and $p\in\textit{px}$, let $\gamma\in P$ be the unique feature guard for which $p\models\gamma$ and define $\llbracket f\rrbracket(p)=f(\gamma)$. This defines the semantic representation of $f$ as the function $\llbracket f\rrbracket:\textit{px}\to K$.

Definition 3.4.

Let $\mathcal{F}=(S,I,F,T)$ be a featured $K$-weighted automaton and $p\in\textit{px}$. The projection of $\mathcal{F}$ to $p$ is the $K$-weighted automaton $\textup{{proj}}_{p}(\mathcal{F})=(S,I,F,T^{\prime})$, where $T^{\prime}=\{(s,\llbracket f\rrbracket(p),s^{\prime})\mid(s,f,s^{\prime})\in T\}$.

The behavior of a featured $K$-weighted automaton is hence given relative to products: given a featured $K$-weighted automaton $\mathcal{F}$ and a product $p$, $|\textup{{proj}}_{p}(\mathcal{F})|$, provided that it exists, will be the behavior of $\mathcal{F}$ when restricted to the particular product $p$. The purpose of this paper is to show how the values $|\textup{{proj}}_{p}(\mathcal{F})|$ can be computed for all $p\in\textit{px}$ at once.

3.4. ∗-Continuous Kleene Algebras

We finish this section by introducing extra structure and properties into our semiring $K$ which will ensure that the infinite sums $|\mathcal{S}|$ always exist. This is for convenience only, and all our work can be extended to a more general (for example non-idempotent) setting. Recall that a semiring $K=(K,\oplus,\otimes,0,1)$ is idempotent (book/DrosteKV09, ) if $x\oplus x=x$ for every $x\in K$.

A ∗-continuous Kleene algebra (DBLP:journals/iandc/Kozen94, ) is an idempotent semiring $K=(K,\oplus,\otimes,0,1)$ in which all infinite sums of the form $\bigoplus_{n\geq 0}x^{n}$, $x\in K$, exist, and such that

[TABLE]

for all $x,y,z\in K$. Intuitively, automata weighted over a ∗-continuous Kleene algebra allow for loop abstraction, in that the global effects of a loop (right-hand side of (1)) can be computed locally (left-hand side of (1)). In any ∗-continuous Kleene algebra $K$ one can define a unary star operation $\mathord{{}^{*}}:K\to K$ by $x^{*}=\bigoplus_{n\geq 0}x^{n}$.

For any semiring $K$ and $n\geq 1$, we can form the matrix semiring $K^{n\times n}$ whose elements are $n$-by-$n$ matrices of elements of $K$ and whose sum and product are given as the usual matrix sum and product. It is known (DBLP:conf/mfcs/Kozen90, ) that when $K$ is a ∗-continuous Kleene algebra, then $K^{n\times n}$ is also a ∗-continuous Kleene algebra, with the ∗-operation defined by $M^{*}_{i,j}=\smash{\bigoplus_{m\geq 0}}\bigoplus\{M_{k_{1},k_{2}}\dotsm M_{k_{m-1},k_{m}}\mid 1\leq k_{1},\dotsc,k_{m}\leq n,k_{1}=i,k_{m}=j\}$ for all $M\in K^{n\times n}$ and $1\leq i,j\leq n$. Also, if $n\geq 2$ and $M=\left[\begin{smallmatrix}a&b\\ c&d\end{smallmatrix}\right]$, where $a$ and $d$ are square matrices of dimension less than $n$, then

[TABLE]

The matrix representation (book/DrosteKV09, ) of a $K$-weighted automaton $\mathcal{S}=(S,I,F,T)$, with $n=\#S$ the number of states, is given by the triple $(\alpha,M,k)$, where $\alpha\in\{0,1\}^{n}$ is the initial vector, $M\in K^{n\times n}$ is the transition matrix, and $0\leq k\leq n$. These are given as follows: order $S=\{1,\dotsc,n\}$ such that $i\in F$ iff $i\leq k$, i.e., such that the first $k$ states are accepting, and define $\alpha$ and $M$ by $\alpha_{i}=1$ iff $i\in I$ and $M_{i,j}=\bigoplus\{x\mid(i,x,j)\in T\}$.

It can be shown (inbook/EsikK09, ) that if $\mathcal{S}$ is a weighted automaton over a ∗-continuous Kleene algebra, then the reachability value of $\mathcal{S}$ is defined and $|\mathcal{S}|=\alpha M^{*}\kappa$, where $\kappa\in\{0,1\}^{n}$ is the vector given by $\kappa_{i}=1$ for $i\leq k$ and $\kappa_{i}=0$ for $i>k$.

Example 3.5.

Our example semirings $\mathbbm{B}$, $\mathbbm{T}$ and $\mathbbm{F}$ share the property of being bounded. In general terms, a semiring $K$ is said to be bounded (book/DrosteKV09, ) if $x\oplus 1=1$ for all $x\in K$. Note that this implies idempotency: for all $x\in K$, $x\oplus x=x(1\oplus 1)=x\otimes 1=x$. If $K$ is bounded, then $x^{*}=1\oplus\dotsm=1$ for all $x\in K$, and $K$ is a ∗-continuous Kleene algebra (journals/mfm/EsikK02, ).

In $\mathbbm{B}$, $x\oplus 1=x\lor\textup{{tt}}=\textup{{tt}}$; in $\mathbbm{T}$, $x\oplus 1=x\land 0=0$; and in $\mathbbm{F}$, $x\oplus 1=x\lor\infty=\infty$; so these three semirings are indeed bounded. Operationally, the fact that $x^{*}=1$ means that loops can be disregarded: for all $x,y,z\in K$, $\bigoplus_{n\geq 0}xy^{n}z=xy^{*}z=xz$. In lieu of the examples in Sect. 3.2, it is clear that this property holds for $\mathbbm{B}$-, $\mathbbm{T}$- and $\mathbbm{F}$-weighted automata: for reachability, loops are unimportant; for minimum reachability, likewise; and for maximum flow, taking a loop can only decrease the flow, hence would be disadvantageous.

4. Analysis of Featured Weighted Automata

Let $K$ be a ∗-continuous Kleene algebra. In this section we take a closer look at the functions in $\textit{GP}[K]$ and define semiring operations on them. We show that with these operations, $\textit{GP}[K]$ itself is a ∗-continuous Kleene algebra. This means that we can treat featured $K$-weighted automata as $\textit{GP}[K]$-weighted automata.

We first need to define an operation on partitions which turns functions $f:P\to K$ from a partition $P\in\textit{GP}$ into injective functions, providing the most concise representation, by changing their domain. Intuitively, this canonicalization of $f$ changes the partition $P$ into a coarser one by forming disjunctions of feature guards on which $f$ has the same value:

Definition 4.1.

Let $P\in\textit{GP}$ and $f:P\to K$. Introduce an equivalence relation $\mathord{\sim}\subseteq P\times P$ by $\gamma_{1}\sim\gamma_{2}$ iff $f(\gamma_{1})=f(\gamma_{2})$ and let $P^{\prime}=P/\mathord{\sim}$ be the quotient. Let $\tilde{P}=\{\bigvee\Gamma\mid\Gamma\in P^{\prime}\}$, then $\tilde{P}\in\textit{GP}$. For every $\tilde{\gamma}\in\tilde{P}$ there is an equivalence class $\Gamma\in P^{\prime}$ for which $\tilde{\gamma}=\bigvee\Gamma$, and $f$ passes to these equivalence classes by definition, so we can define $\tilde{f}:\tilde{P}\to K$, the canonicalization of $f$, by $\tilde{f}(\tilde{\gamma})=f(\Gamma)$.

We show an algorithm which implements canonicalization in Fig. 2. The function $K$Combine takes as input a function $f:P\to K$ and builds its canonicalization $\tilde{f}:\tilde{P}\to K$ by taking disjunctions of feature expressions in the partition $P$. Note the similarity of its inner loop to the Combine procedure of Fig. 1: the procedure in Fig. 1 only updates the partition of $f$ in one place, whereas $K$Combine needs to check the whole partition.

Lemma 4.2.

Let $P\in\textit{GP}$, $f:P\to K$, and $\tilde{f}:\tilde{P}\to K$ the canonicalization of $f$. Then $\tilde{f}$ is injective, hence $\tilde{f}\in\textit{GP}[K]$. Also, for any $\gamma\in P$ there is a unique element $\tilde{\gamma}\in\tilde{P}$ such that $\llbracket\gamma\rrbracket\subseteq\llbracket\tilde{\gamma}\rrbracket$.

Definition 4.3.

Let $P_{1},P_{2}\in\textit{GP}$. The intersection of $P_{1}$ and $P_{2}$ is the partition $P=P_{1}\wedge P_{2}\in\textit{GP}$ given as $P=\{\gamma_{1}\land\gamma_{2}\mid\gamma_{1}\in P_{1},\gamma_{2}\in P_{2},\llbracket\gamma_{1}\land\gamma_{2}\rrbracket\neq\emptyset\}$.

Lemma 4.4.

Let $P_{1},P_{2}\in\textit{GP}$ and $\gamma\in P_{1}\wedge P_{2}$. There are unique elements $\gamma_{1}\in P_{1}$, $\gamma_{2}\in P_{2}$ such that $\gamma=\gamma_{1}\land\gamma_{2}$.

We can hence write the elements of $P_{1}\wedge P_{2}$ as $\gamma_{1}\land\gamma_{2}$ without ambiguity. We are ready to define operations $\oplus$, $\otimes$ and ∗ on functions in $\textit{GP}[K]$.

Definition 4.5.

Let $f_{1}:P_{1}\to K,f_{2}:P_{2}\to K\in\textit{GP}[K]$. Define functions $s^{\prime},p^{\prime}:P_{1}\wedge P_{2}\to K$ and $t^{\prime}:P_{1}\to K$ by $s^{\prime}(\gamma_{1}\land\gamma_{2})=f_{1}(\gamma_{1})\oplus f_{2}(\gamma_{2})$, $p^{\prime}(\gamma_{1}\land\gamma_{2})=f_{1}(\gamma_{1})\otimes f_{2}(\gamma_{2})$, and $t^{\prime}(\gamma_{1})=f_{1}(\gamma_{1})^{*}$. Let $s,p,t\in\textit{GP}[K]$ be the canonicalizations of $s^{\prime}$, $p^{\prime}$ and $t^{\prime}$, respectively, then we define $f_{1}\oplus f_{2}=s$, $f_{1}\otimes f_{2}=p$, and $f_{1}^{*}=t$.

Figure 3 shows algorithms to compute these operations in $\textit{GP}[K]$. Note how these are similar to the Split procedure in Fig. 1.

Let $\mathbb{0},\mathbb{1}:\{\textup{{tt}}\}\to K$ be the functions given by $\mathbb{0}(\textup{{tt}})=0$ and $\mathbb{1}(\textup{{tt}})=1$. Then $\mathbb{0},\mathbb{1}\in\textit{GP}[K]$.

Lemma 4.6.

Let $f_{1},f_{2}\in\textit{GP}[K]$ and $p\in\textit{px}$. Then $\llbracket f_{1}\oplus f_{2}\rrbracket(p)=\llbracket f_{1}\rrbracket(p)\oplus\llbracket f_{2}\rrbracket(p)$, $\llbracket f_{1}\otimes f_{2}\rrbracket(p)=\llbracket f_{1}\rrbracket(p)\otimes\llbracket f_{2}\rrbracket(p)$, and $\llbracket f_{1}^{*}\rrbracket(p)=\llbracket f\rrbracket_{1}(p)^{*}$.

Lemma 4.7.

Let $f_{1},f_{2}\in\textit{GP}[K]$. Then $f_{1}=f_{2}$ iff $\llbracket f_{1}\rrbracket=\llbracket f_{2}\rrbracket$.

Proposition 4.8.

The structure $(\textit{GP}[K],\oplus,\otimes,\mathbb{0},\mathbb{1})$ forms a∗-continuous Kleene algebra.

Lemma 4.9.

For $n\geq 1$, $M\in\textit{GP}[K]^{n\times n}$, and $p\in\textit{px}$, $\llbracket M^{*}\rrbracket(p)=\llbracket M\rrbracket(p)^{*}$.

We are ready to give the central result of this paper, stating that for a given featured weighted automaton $\mathcal{F}$, computing $|\mathcal{F}|$ suffices to obtain all projected values.

Theorem 4.10.

Let $\mathcal{F}$ be a featured weighted automaton over $K$ and $p\in\textit{px}$. Then $|\textup{{proj}}_{p}(\mathcal{F})|=\llbracket|\mathcal{F}|\rrbracket(p)$.

Proof.

We have $\llbracket|\mathcal{F}|\rrbracket(p)=\llbracket\alpha M^{*}\kappa\rrbracket(p)=\llbracket\alpha\rrbracket(p)\llbracket M\rrbracket(p)^{*}\llbracket\kappa\rrbracket(p)$ by Lemmas 4.6 and 4.9. Noting that the matrix representation of $\textup{{proj}}_{p}(\mathcal{F})$ is $(\llbracket\alpha\rrbracket(p),\llbracket M\rrbracket(p),k)$, the proof is finished. ∎

5. Featured Energy Problems

In this final section we apply the theoretical results of this paper to featured energy problems.

5.1. Energy Problems

The energy semiring (DBLP:conf/atva/EsikFLQ13, ) is the structure $\mathbbm{E}=(\mathcal{E},\mathord{\vee},\mathord{\circ},\bot,\top)$. Here $\mathcal{E}$ is the set of energy functions, which are partial functions $f:\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}\to\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}$ on extended real numbers ($f(x)=\bot$ meaning that $f$ is undefined at $x$) with the property that

[TABLE]

These have been introduced in (DBLP:conf/atva/EsikFLQ13, ) as a general framework to handle formal energy problems as below. The operations in the semiring are (pointwise) maximum as $\oplus$ and function composition as $\otimes$, and the neutral elements are the functions $\bot$, id given by $\bot(x)=\bot$ and $\textup{{id}}(x)=x$ for all $x\in\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}$.

Definition 5.1.

An energy automaton is a tuple $(S,I,F,T)$ consisting of a finite set $S$ of states, subsets $I,F\subseteq S$ of initial and accepting states, and a finite set $T\subseteq S\times\mathcal{E}\times S$ of transitions.

Hence the transition labels in energy automata are functions which proscribe how a real-valued variable evolves along a transition. An energy problem asks, then, whether some state is reachable when given a certain initial energy, or whether the automaton admits infinite accepting runs from some initial energy:

A global state of an energy automaton is a pair $q=(s,x)$ with $s\in S$ and $x\in\mathbbm{R}_{\geq 0}$. A transition between global states is of the form $((s,x),f,(s^{\prime},x^{\prime}))$ such that $(s,f,s^{\prime})\in T$ and $x^{\prime}=f(x)$. A (finite or infinite) run of the automaton is a (finite or infinite) path in the graph of global states and transitions.

As the input to a decision problem must be in some way finitely representable, we will state them for subclasses $\mathcal{E}^{\prime}\subseteq\mathcal{E}$ of computable energy functions (but note that we give no technical meaning to the term “computable” other that “finitely representable”); an $\mathcal{E}^{\prime}$-automaton is an energy automaton $(S,I,F,T)$ with $T\subseteq S\times\mathcal{E}^{\prime}\times S$.

Problem 1 (Reachability).

Given a subset $\mathcal{E}^{\prime}\subseteq\mathcal{E}$ of computable functions, an $\mathcal{E}^{\prime}$-automaton $\mathcal{S}=(S,I,F,T)$ and a computable initial energy $x_{0}\in\mathbbm{R}_{\geq 0}$: do there exist $s_{0}\in I$ and a finite run of $\mathcal{S}$ from $(s_{0},x_{0})$ which ends in a state in $F$?

Problem 2 (Büchi acceptance).

Given a subset $\mathcal{E}^{\prime}\subseteq\mathcal{E}$ of computable functions, an $\mathcal{E}^{\prime}$-automaton $\mathcal{S}=(S,I,F,T)$ and a computable initial energy $x_{0}\in\mathbbm{R}_{\geq 0}$: do there exist $s_{0}\in I$ and an infinite run of $\mathcal{S}$ from $(s_{0},x_{0})$ which visits $F$ infinitely often?

As customary, a run such as in the statements above is said to be accepting.

5.2. ∗-Continuous Kleene $\omega$-Algebras

We need a few algebraic notions connected to infinite runs in weighted automata before we can continue. An idempotent semiring-semimodule pair (journals/sgf/EsikK07, ; book/BloomE93, ) $(K,V)$ consists of an idempotent semiring $K=(K,\oplus,\otimes,0,1)$ and a commutative idempotent monoid $V=(V,\oplus,0)$ which is equipped with a left $K$-action $K\times V\to V$, $(x,v)\mapsto xv$, satisfying the following axioms for all $x,y\in K$ and $u,v\in V$:

[TABLE]

Also non-idempotent versions of these are in use, but we will only need the idempotent one here.

A generalized ∗-continuous Kleene algebra (DBLP:conf/dlt/EsikFL15, ) is an idempotent semiring-semimodule pair $(K,V)$ where $K$ is a ∗-continuous Kleene algebra such that for all $x,y\in K$ and for all $v\in V$,

[TABLE]

A ∗-continuous Kleene $\omega$-algebra (DBLP:conf/dlt/EsikFL15, ) consists of a generalized ∗-continuous Kleene algebra $(K,V)$ together with an infinite product operation $K^{\omega}\to V$ which maps every infinite sequence $x_{0},x_{1},\dotsc$ in $K$ to an element $\prod_{n}x_{n}$ of $V$. The infinite product is subject to the following conditions:

• •

For all $x_{0},x_{1},\dotsc\in K$, $\prod_{n}x_{n}=x_{0}\prod_{n}x_{n+1}$.

• •

Let $x_{0},x_{1},\dotsc\in K$ and $0=n_{0}\leq n_{1}\leq\dotsm$ a sequence which increases without a bound. Let $y_{k}=x_{n_{k}}\dotsm x_{n_{k+1}-1}$ for all $k\geq 0$. Then $\prod_{n}x_{n}=\prod_{k}y_{k}$.

• •

For all $x_{0},x_{1},\dotsc,y,z\in K$, we have $\prod_{n}(x_{n}(y\oplus z))=\bigoplus_{x_{0}^{\prime},x_{1}^{\prime},\dotsc\in\{y,z\}\;}\prod_{n}x_{n}x_{n}^{\prime}$.

• •

For all $x,y_{0},y_{1},\dotsc\in K$, $\prod_{n}x^{*}y_{n}=\bigoplus_{k_{0},k_{1},\dotsc\geq 0\;}\prod_{n}x^{k_{n}}y_{n}$.

For any idempotent semiring-semimodule pair $(K,V)$ and $n\geq 1$, we can form the matrix semiring-semimodule pair $(K^{n\times n},V^{n})$ whose elements are $n\times n$-matrices of elements of $K$ and $n$-dimensional (column) vectors of elements of $V$, with the action of $K^{n\times n}$ on $V^{n}$ given by the usual matrix-vector product.

When $(K,V)$ is a ∗-continuous Kleene $\omega$-algebra, then $(K^{n\times n},V^{n})$ is a generalized ∗-continuous Kleene algebra (DBLP:conf/dlt/EsikFL15, ). By (DBLP:conf/dlt/EsikFL15, , Lemma 17), there is an $\omega$-operation on $K^{n\times n}$ defined by

[TABLE]

for all $M\in K^{n\times n}$ and $1\leq i\leq n$. Also, if $n\geq 2$ and $M=\left[\begin{smallmatrix}a&b\\ c&d\end{smallmatrix}\right]$, where $a$ and $d$ are square matrices of dimension less than $n$, then

[TABLE]

We also need another matrix-$\omega$-power below. Let $n\geq 2$, $k<n$ and $M\in K^{n\times n}$, and write $M=\left[\begin{smallmatrix}a&b\\ c&d\end{smallmatrix}\right]$ as above, with $a\in K^{k\times k}$ top left $k$-by-$k$ part of $M$. We define

[TABLE]

Let $(K,V)$ be a ∗-continuous Kleene $\omega$-algebra and $\mathcal{S}=(S,I,F,T)$ a $K$-weighted automaton. An infinite path in $\mathcal{S}$ is an infinite alternating sequence $\pi=(s_{0},x_{0},s_{1},x_{1},s_{2},\dotsc)$ of transitions $(s_{0},x_{0},s_{1}),$ $(s_{1},x_{1},s_{2}),\dotsc\in T$. The weight of $\pi$ is the infinite product $w(\pi)=\prod_{n}x_{n}\in V$.

An infinite path $\pi=(s_{0},x_{0},s_{1},x_{1},\dotsc)$ in $\mathcal{S}$ is said to be Büchi accepting if $s_{0}\in I$ and the set $\{n\in\mathbbm{N}\mid s_{n}\in F\}$ is infinite. The Büchi value $\|\mathcal{S}\|$ of $\mathcal{S}$ is defined to be the sum of the weights of all its Büchi accepting infinite paths:

[TABLE]

Let $(\alpha,M,k)$ be the matrix representation of $\mathcal{S}$. It can be shown (DBLP:conf/dlt/EsikFL15, ) that

[TABLE]

5.3. Featured Energy Problems

Recall that $\mathcal{E}$ denotes the set of energy functions: functions $f:\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}\to\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}$ with the property (3) that whenever $x\leq y$, then $f(y)-f(x)\geq y-x$; and that $\mathbbm{E}=(\mathcal{E},\mathord{\vee},\mathord{\circ},\bot,\top)$ is the semiring of energy functions.

Lemma 5.2 ((DBLP:journals/corr/EsikFL15a, )).

$\mathbbm{E}$* is a ∗-continuous Kleene algebra.*

Let $\mathbbm{B}=\{\textup{{ff}},\textup{{tt}}\}$ be the Boolean lattice. We say that a function $f:\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}\to\mathbbm{B}$ is $\infty$-continuous if $f=\bot$ or for all $X\subseteq\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}$ with $\bigvee X=\infty$, $\bigvee f(X)=\textup{{tt}}$.

Let $\mathcal{V}$ be the set of $\infty$-continuous functions $f:\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}\to\mathbbm{B}$. With operation $\vee$ defined by $(f\vee g)(x)=f(x)\lor g(x)$ and unit $\bot$ given by $\bot(x)=\textup{{ff}}$ for all $x\in\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}$, $\mathbbm{V}=(\mathcal{V},\vee,\bot)$ forms a commutative idempotent monoid. Then $(\mathbbm{E},\mathbbm{V})$ is an idempotent semiring-semimodule pair.

Define an infinite product $\mathcal{E}\to\mathcal{V}$ as follows: Let $f_{0},f_{1},\dotsc\in\mathcal{E}$ be an infinite sequence and $x\in\mathbbm{R}_{\geq 0}\cup\{\bot,\infty\}$. Let $x_{0}=f_{0}(x)$ and, for each $k\geq 1$, $x_{k}=f_{k}(x_{k-1})$. Thus $x_{0},x_{1},\dotsc$ is the infinite sequence of values obtained by application of finite prefixes of the function sequence $f_{0},f_{1},\dotsc$. Then $(\prod_{n}f_{n})(x)=\textup{{ff}}$ if there is an index $k$ for which $x_{k}=\bot$ and $(\prod_{n}f_{n})(x)=\textup{{tt}}$ otherwise.

It can be shown (DBLP:journals/corr/EsikFL15a, ) that $\prod_{n}f_{n}$ is $\infty$-continuous for any infinite sequence $f_{0},f_{1},\dotsc\in\mathcal{E}$, hence this defines indeed a mapping $\mathcal{E}^{\omega}\to\mathcal{V}$.

Lemma 5.3 ((DBLP:journals/corr/EsikFL15a, )).

$(\mathbbm{E},\mathbbm{V})$* is a ∗-continuous Kleene $\omega$-algebra.*

Hence the energy problems stated at the end of Sect. 5.1 can be solved by computing reachability and Büchi values of energy automata:

Proposition 5.4 ((DBLP:journals/corr/EsikFL15a, )).

Let $\mathcal{S}=(S,I,F,T)$ be an energy automaton and $x_{0}\in\mathbbm{R}_{\geq 0}$.

• •

There exist $s_{0}\in I$ and a finite run of $\mathcal{S}$ from $(s_{0},x_{0})$ which ends in a state in $F$ iff $|\mathcal{S}|(x_{0})\neq\bot$.

• •

There exist $s_{0}\in I$ and an infinite run of $\mathcal{S}$ from $(s_{0},x_{0})$ which visits $F$ infinitely often iff $\|\mathcal{S}\|(x_{0})=\textup{{tt}}$.

We now define energy problems for featured automata. Recall that $N$ denotes a set of features and $\textit{px}\subseteq 2^{N}$ a set of products over $N$.

Definition 5.5.

A featured energy automaton over px is a tuple $(S,I,F,T)$ consisting of a finite set $S$ of states, subsets $I,F\subseteq S$ of initial and accepting states, and a finite set $T\subseteq S\times\textit{GP}[\mathcal{E}]\times S$ of transitions.

Hence transitions in featured energy automata are labeled with (injective) functions from guard partitions to energy functions.

Lemma 5.6.

For $f\in\mathcal{E}$, $f^{\omega}\in\mathcal{V}$ is given by

[TABLE]

Definition 5.7.

Let $f:P\to\mathcal{E}\in\textit{GP}[\mathcal{E}]$ and define $w^{\prime}:P\to\mathcal{V}$ by $w^{\prime}(\gamma)=f(\gamma)^{\omega}$. Let $w\in\textit{GP}[\mathcal{V}]$ be the canonicalization of $w^{\prime}$, then we define $f^{\omega}=w$.

Lemma 5.8.

For $n\geq 1$, $k<n$, $M\in\textit{GP}[\mathcal{E}]^{n\times n}$, and $p\in\textit{px}$, $\llbracket M^{\omega}\rrbracket(p)=\llbracket M\rrbracket(p)^{\omega}$ and $\llbracket M^{\omega_{k}}\rrbracket(p)=\llbracket M\rrbracket(p)^{\omega_{k}}$.

Theorem 5.9.

Let $\mathcal{F}$ be a featured energy automaton and $p\in\textit{px}$. Then $\|\textup{{proj}}_{p}(\mathcal{F})\|=\llbracket\|\mathcal{F}\|\rrbracket(p)$.

Proof.

We have $\llbracket\|\mathcal{F}\|\rrbracket(p)=\llbracket\alpha M^{\omega_{k}}\rrbracket(p)=\llbracket\alpha\rrbracket(p)\llbracket M\rrbracket(p)^{\omega_{k}}$ by Lemmas 4.6 and 5.8. As the matrix representation of $\textup{{proj}}_{p}(\mathcal{F})$ is $(\llbracket\alpha\rrbracket(p),\llbracket M\rrbracket(p),k)$, the result follows. ∎

6. Conclusion

We have introduced featured (semiring-) weighted automata and shown that, essentially, verification of their properties can be reduced to checking properties of weighted automata. This is because, from a mathematical point of view, a featured weighted automaton over a semiring $K$ is the same as a weighted automaton over the semiring of functions from products (sets of features) to $K$.

Representing functions from products to $K$ as injective functions from partitions of the set of products to $K$, we have exposed algorithms which will compute featured weighted reachability in case $K$ is a ∗-continuous Kleene algebra. It is easy to see that these extend to the non-idempotent case of $K$ being a Conway semiring. The essence in our approach does not lie in these technical details, but in the fact that we pass from $K$ to a semiring of functions into $K$; this typically preserves properties one is interested in.

We have also seen that energy properties are preserved when passing from the weighted to the featured weighted setting; generally, if $(K,V)$ is a ∗-continuous Kleene $\omega$-algebra, then the semiring-semimodule pair of functions from products to $K$ and $V$, respectively, will also be such.

We are interested in extending the setting of this paper to other weighted structures beyond semirings, for example the valuation monoids of (DBLP:journals/ijfcs/DrosteM11, ). This will enable feature-based treatment of properties such as limit-average cost and will be useful for an extension to the timed setting of (DBLP:conf/splc/CordySHL12, ). From a practical point of view, we have shown in (DBLP:conf/splc/OlaecheaFAL16, ) that efficient algorithms are available for the limit-average setting.

Appendix: Proofs

Proof of Lemma 4.2.

To see that $\tilde{f}$ is injective, let $\tilde{\gamma}_{1},\tilde{\gamma}_{2}\in\tilde{P}$ and assume $\tilde{f}(\tilde{\gamma}_{1})=\tilde{f}(\tilde{\gamma}_{2})$. Let $\Gamma_{1},\Gamma_{2}\in P^{\prime}$ such that $\tilde{\gamma}_{1}=\bigvee\Gamma_{1}$ and $\tilde{\gamma}_{2}=\bigvee\Gamma_{2}$, then $f(\Gamma_{1})=f(\Gamma_{2})$ and hence $\Gamma_{1}=\Gamma_{2}$, i.e., $\tilde{\gamma}_{1}=\tilde{\gamma}_{2}$.

For the second claim, let $\gamma\in P$, then $\gamma\in\Gamma$ for some $\Gamma\in P^{\prime}$, hence $\llbracket\gamma\rrbracket\subseteq\llbracket\bigvee\Gamma\rrbracket$. To see uniqueness, let $\tilde{\gamma}_{1},\tilde{\gamma}_{2}\in\tilde{P}$ and assume $\llbracket\gamma\rrbracket\subseteq\llbracket\tilde{\gamma}_{1}\rrbracket$ and $\llbracket\gamma\rrbracket\subseteq\llbracket\tilde{\gamma}_{2}\rrbracket$. As $\llbracket\gamma\rrbracket\neq\emptyset$, this implies that $\llbracket\tilde{\gamma}_{1}\rrbracket\cap\llbracket\tilde{\gamma}_{2}\rrbracket\neq\emptyset$, hence $\tilde{\gamma}_{1}=\tilde{\gamma}_{2}$. ∎

Proof of Lemma 4.4.

Existence of $\gamma_{1}$ and $\gamma_{2}$ is obvious by definition of $P_{1}\wedge P_{2}$. For uniqueness, assume that there is $\gamma_{1}^{\prime}\in P_{1}$ with $\gamma_{1}^{\prime}\neq\gamma_{1}$ and $\gamma=\gamma_{1}^{\prime}\land\gamma_{2}$. Then $\gamma=\gamma_{1}\land\gamma_{1}^{\prime}\land\gamma$, but as $P_{1}$ is a partition, $\llbracket\gamma_{1}\land\gamma_{1}^{\prime}\rrbracket=\llbracket\gamma_{1}\rrbracket\cap\llbracket\gamma_{1}^{\prime}\rrbracket=\emptyset$, hence $\llbracket\gamma\rrbracket=\emptyset$, a contradiction. ∎

Proof of Lemma 4.6.

Let $f_{1}:P_{1}\to K$ and $f_{2}:P_{2}\to K$. Let $\gamma_{1}\in P_{1}$, $\gamma_{2}\in P_{2}$ be the unique feature guards for which $p\models\gamma_{1}$ and $p\models\gamma_{2}$, then $\llbracket f_{1}\rrbracket(p)=f_{1}(\gamma_{1})$ and $\llbracket f_{2}\rrbracket(p)=f_{2}(\gamma_{2})$.

We have $p\in\llbracket\gamma_{1}\land\gamma_{2}\rrbracket$, hence $\llbracket\gamma_{1}\land\gamma_{2}\rrbracket\neq\emptyset$, so that $\gamma_{1}\land\gamma_{2}\in P_{1}\wedge P_{2}$. Using the notation of Def. 4.5, $s^{\prime}(\gamma_{1}\land\gamma_{2})=f_{1}(\gamma_{1})\oplus f_{2}(\gamma_{2})=\llbracket f_{1}\rrbracket(p)\oplus\llbracket f_{2}\rrbracket(p)$. Write $s:P\to K$ and let $\tilde{\gamma}\in P$ be such that $\llbracket\gamma_{1}\land\gamma_{2}\rrbracket\subseteq\llbracket\tilde{\gamma}\rrbracket$, cf. Lemma 4.2. Then $p\models\tilde{\gamma}$, hence $\llbracket f_{1}\oplus f_{2}\rrbracket(p)=(f_{1}\oplus f_{2})(\tilde{\gamma})=s^{\prime}(\gamma_{1}\land\gamma_{2})$. The proofs for $\otimes$ and ∗ are similar. ∎

Proof of Lemma 4.7.

It is clear that $f_{1}=f_{2}$ implies $\llbracket f_{2}\rrbracket=\llbracket f_{2}\rrbracket$. For the other direction, write $f_{1}:P_{1}\to K$ and $f_{2}:P_{2}\to K$. For each $p\in\textit{px}$, let $\gamma_{p}=\bigwedge_{f\in p}f\land\bigwedge_{f\notin p}\neg f\in\mathbbm{B}(N)$ denote its characteristic feature guard; note that $\llbracket\gamma_{p}\rrbracket=\{p\}$.

Let $P\in\textit{GP}$ be the guard partition $P=\{\gamma_{p}\mid p\in\textit{px}\}$, and define functions $f_{1}^{\prime},f_{2}^{\prime}:P\to K$ by $f_{1}^{\prime}(\gamma_{p})=\llbracket f_{1}\rrbracket(p)$ and $f_{2}^{\prime}(\gamma_{p})=\llbracket f_{2}\rrbracket(p)$. By definition, $f_{1}$ is the canonicalization of $f_{1}^{\prime}$ and $f_{2}$ the canonicalization of $f_{2}^{\prime}$. By construction, $\llbracket f_{1}\rrbracket=\llbracket f_{2}\rrbracket$ implies $f_{1}^{\prime}=f_{2}^{\prime}$, hence $f_{1}=f_{2}$. ∎

Proof of Prop. 4.8.

We show that the set $K^{\textit{px}}$ of functions from px to $K$ forms a ∗-continuous Kleene algebra; the theorem is then clear from Lemmas 4.6 and 4.7. For functions $\phi_{1},\phi_{2}:\textit{px}\to K$, define $\phi_{1}\oplus\phi_{2}$, $\phi_{1}\otimes\phi_{2}$ and $\phi_{1}^{*}$ by $(\phi_{1}\oplus\phi_{2})(p)=\phi_{1}(p)\oplus\phi_{2}(p)$, $(\phi_{1}\otimes\phi_{2})(p)=\phi_{1}(p)\otimes\phi_{2}(p)$, and $\phi_{1}^{*}(p)=\phi_{1}(p)^{*}$. Let $0,1:\textit{px}\to K$ be the functions $0(p)=0$, $1(p)=1$. Then $(K^{\textit{px}},\oplus,\otimes,0,1)$ forms an idempotent semiring.

We miss to show ∗-continuity. Let $p\in\textit{px}$ and $\phi_{1},\phi_{2},\phi_{3}:\textit{px}\to K$, then

[TABLE]

∎

Proof of Lemma 4.9.

As the formula for computing $M^{*}$ involves only additions, multiplications and stars, this is clear by Lemma 4.6. ∎

Proof of Lemma 5.6.

The claim is clear for $x=\bot$, so let $x\neq\bot$. If $f(x)\geq x$, then also $f^{n}(x)\geq x$ for all $n\geq 0$, hence $f^{\omega}(x)=\textup{{tt}}$ by definition.

If $f(x)<x$, then $f(x)\leq x-M$, with $M=x-f(x)>0$. By (3), $f^{n}(x)\leq x-nM$ for all $n\geq 0$, hence there must be $k\geq 0$ for which $f^{k}(x)=\bot$, whence $f^{\omega}(x)=\textup{{ff}}$. ∎

Proof of Lemma 5.8.

The formulas for $M^{\omega}$ and $M^{\omega_{k}}$ involve only additions, multiplications, stars, and $\omega$s. Invoking Lemmas 4.6 and 4.9, we see that the proof will be finished once we show that for $f\in\textit{GP}[\mathcal{E}]$, $\llbracket f^{\omega}\rrbracket(p)=\llbracket f\rrbracket(p)^{\omega}$.

Write $f:P\to\mathcal{E}$ and let $\gamma\in P$ be the unique feature guard for which $p\models\gamma$. Then $\llbracket f\rrbracket(p)=f(\gamma)$. Using the notation of Def. 5.7, $w^{\prime}(\gamma)=\llbracket f\rrbracket(p)^{\omega}$. Write $w:P^{\prime}\to\mathcal{V}$ and let $\tilde{\gamma}\in P^{\prime}$ be such that $\llbracket\gamma\rrbracket\subseteq\llbracket\tilde{\gamma}\rrbracket$, cf. Lemma 4.2. Then $p\models\tilde{\gamma}$, hence $\llbracket f^{\omega}\rrbracket(p)=f^{\omega}(\tilde{\gamma})=w^{\prime}(\gamma)$. ∎