Discrete Event Dyn Syst (2010) 20:103–137 DOI 10.1007/s10626-008-0057-0

Model Checking for a Class of Weighted Automata Peter Buchholz · Peter Kemper

Received: 2 November 2007 / Accepted: 19 December 2008 / Published online: 15 January 2009 © Springer Science + Business Media, LLC 2009

Abstract A large number of different model checking approaches has been proposed during the last decade. The different approaches are applicable to different model types including untimed, timed, probabilistic and stochastic models. This paper presents a new framework for model checking techniques which includes some of the known approaches and enlarges the class of models to which model checking can be applied to the general class of weighted automata. The approach allows an easy adaption of model checking to models which have not been considered yet for this purpose. Examples for those new model types for which model checking can be applied are max/plus or min/plus automata which are well established models to describe different forms of dynamic systems and optimization problems. In this context, model checking can be used to verify temporal or quantitative properties of a system. The paper first presents briefly our class of weighted automata, as a very general model type. Then Valued Computational Tree Logic (CTL$) is introduced as a natural extension of the well known branching time logic CTL. Afterwards, algorithms to check a weighted automaton with respect to a CTL$ formula are presented. As a last result, bisimulation equivalence is extended to weighted automata and CTL$. Keywords Finite automata · Weighted automata · Semirings · Model checking · Valued computational tree logic · Bisimulation

P. Buchholz (B) Informatik IV, TU Dortmund, 44221 Dortmund, Germany e-mail: [email protected] P. Kemper Department of Computer Science, College of William and Mary, Williamsburg, VA 23187-8795, USA e-mail: [email protected]

104

Discrete Event Dyn Syst (2010) 20:103–137

1 Introduction Model checking of finite state systems is an established approach for the automatic or semi-automatic analysis of dynamic systems from different application areas. The basic model checking approaches have been proposed for untimed models and allow one to check the functional correctness of systems. The general idea of this kind of model checking is to determine the set of states of a finite state automaton which satisfy a formula of a temporal logic. Common examples of modal logics to express formulas are Linear Time Logic (LTL) or Computational Tree Logic (CTL). For both logics, efficient analysis algorithms exist that allow the handling of extremely large automata. Nowadays, several software tools are available that include model checking algorithms, allow the automatic analysis of dynamic systems and have been applied to practical examples from different application areas such as hardware verification or software engineering. An enormous number of papers on model checking and related topics exists, for surveys we refer to Clarke et al. (1996, 1999), Clarke and Kurshan (1996) and Berard et al. (2001) as textbooks. For several application areas, the proof of functional correctness is not sufficient to assure the correct behavior of a system. For instance, in real-time systems, it has to be assured that a function of a reactive system performs correctly and takes place in a given time interval. For other systems, we may tolerate some erroneous behavior if it occurs only with a sufficiently small probability. In this and similar situations, a basic proof of correctness is not sufficient. Consequently, model checking approaches have been extended to also handle timed, probabilistic and stochastic systems. In Hansson and Jonsson (1994), an extended version of the temporal logic CTL is presented that is denoted as Probabilistic Real Time Computational Tree Logic (PCTL). This logic allows the definition of properties which state that something will happen with a given probability in a fixed time interval. The logic is interpreted over finite Discrete Time Markov Chains (DTMCs). The timing is defined by the number of transitions that occur and probabilities are defined by the transition probabilities of the DTMC. PCTL is a useful logic to express requirements for real time systems with constant delays. Another extension of CTL which is denoted as min–max CTL is described in Dasgupta et al. (2001). This logic allows one to formulate assumptions that include the minimal or maximal weight of a path. Other model checking approaches analyze different forms of timed automata (Alur and Dill 1994) that are possibly augmented by different timing models (Bryans et al. 2003). Extensions of CT L for this class of models such as weighted CTL (WCTL) can be found in Brihaye et al. (2004) and Bouyer (2006). Brihaye et al study a model-checking problem for a particular class of hybrid automata. They consider WCTL, a logic that evaluates numerical constraints based on costs that can be assigned to both states and transitions. Bouyer considers the same logic and class of automata in Bouyer (2006) for model-checking and games. Both papers take interest in recognizing for what notions of time (dense or discrete) and which numbers of clocks WCTL model-checking is undecidable or not. For “continuous time Markov” chains, a family of related logics based on the Continuous Stochastic Logic (CSL) (Baier et al. 2003) has been developed, whose members vary with respect to the consideration of states and actions as for asCSL (Baier et al. 2007) or the specification of formulas by timed automata as for CSLT A (Donatelli et al. 2007). These logics differ from the other mentioned approaches and also from the approach proposed here because they are based on stochastic timing.

Discrete Event Dyn Syst (2010) 20:103–137

105

The mentioned approaches for model checking are all similar but differ in various details. In particular, the different logics are all interpreted over an appropriate automata model. Those automata models differ; for instance untimed automata are used for standard model checking, probabilistic automata for timed and probabilistic model checking, stochastic automata for stochastic model checking and various other forms of timed automata have been considered as well. By considering the wide area of finite state automata, one can notice that in addition to these types of automata other models have been proposed and applied successfully in different application areas. Examples are min/plus, max/plus, or min/max automata that have been used for the analysis of real time systems (Baccelli et al. 1999), communication systems (Baccelli and Hong 2000), and discrete event systems (Baccelli et al. 1992; Gaubert 1995). Furthermore, similar models have been applied for natural language processing (Mohri et al. 1996) or image compression (Jiang et al. 2000). It is quite natural, and for most of the mentioned applications also very useful, to extend model checking approaches to all these types of automata. Since the class of weighted automata provides in some sense a superset of different automata types, which includes different forms of probabilistic automata and also untimed automata, one may strive for a general framework for model checking which can be applied to a wide variety of different types of weighted automata without defining a new approach for each type. Such a framework is of theoretical interest for a better understanding of model checking and for a common ground in model checking for various application areas. From a methodological point of view, it gives direct access to model checking techniques for various types of automata that do not profit from these techniques yet. Finally, it supports tool development: in an object oriented setting, implementation of a specific model checker can inherit basic techniques from a more general class that implements techniques valid for the whole framework. A first prototype tool for this purpose has been developed recently (Dragan 2007). Weighted automata (Eilenberg 1974; Kuich and Salomaa 1986) are a well known class of automata where transitions are labeled with labels from a finite alphabet and, additionally, receive weights or costs that are elements of some semiring. A key observation is that the algebraic structure of a semiring (Golan 1999) is sufficient to define model checking for weighted automata. The advantage is that by selecting appropriate semirings, one obtains different types of automata that include most of the above mentioned types. This general type of automata is suitable to define a bisimulation as we did in Buchholz (2008) and Buchholz and Kemper (2003b). In Buchholz and Kemper (2001), the process algebra GPA has been introduced for the specification of models in a compositional way such that the underlying semantic model is a weighted automaton in the case of a finite set of states. In this paper, we develop a model checking approach for weighted automata. The approach allows us to check formulas of the newly defined logic Valued Computational Tree Logic (CTL$) over a weighted automaton.1 Algorithms for model checking are developed and it will be shown that by an appropriate definition of

1 The

proposed approach is based on earlier but unpublished work (Buchholz and Kemper 2003a) where a first version of CTL$ has been developed. Compared to Buchholz and Kemper (2003a) the current paper is more complete, several errors have been corrected and more general algorithms for model checking have been developed.

106

Discrete Event Dyn Syst (2010) 20:103–137

the semiring used for the definition of transitions weights, we naturally define model checking approaches for different model types without developing new approaches in each case. The special cases include untimed, probabilistic, min/plus, max/plus, and min/max automata such that known model checking approaches are covered and new approaches are introduced in the case of min/plus, max/plus, and min/max automata. By the use of other semirings for transition weights, the proposed approach applies to a wide class of automata models. In other words, we develop some form of a generic approach for model checking that is applicable to other model classes and that includes algorithms to perform model checking. The structure of the paper is as follows. In the next section, we present the automata model that is considered in this paper. In Section 3, we define CTL$, a logic for weighted automata that is an extension of the well known branching time logic CTL for untimed automata. Section 4 introduces algorithms to check a CTL$ formula according to an automaton with transition weights. We consider algorithms with explicit state representations for clarity at this point. A treatment by symbolic representations such as multi terminal binary decision diagrams (MTBDDs) or edgevalued decision diagrams is feasible but not in the focus of this paper. In Section 5, bisimulation is briefly defined for weighted automata and it is proved that bisimilar automata are indistinguishable under CTL$ formulas. Afterwards, in Section 6, we present several examples of weighted automata for specific semirings and derive some complexity results. We conclude in Section 7.

2 Weighted automata To present our general automata model, we first introduce semirings that are needed to define labels for transitions. Afterwards the automata model is defined.  ,  and Definition 2.1 A semiring (IK, + · , 0,  1) is a set IK with binary operations +  · defined on IK such that the following axioms are satisfied: , 1. + · are associative,  is commutative, 2. +  and  3. right and left distributive laws hold for + ·, 4.  0 and  1 are the additive and multiplicative identities with  0 =  1, 5. k · 0 = 0 · k = 0 holds for all k ∈ IK. Semirings can show specific properties such as idempotency, commutativity, or being ordered; properties that we formally define as follows. Definition 2.2 A semiring can have the following properties: •

It is ordered with some order relation ≤ if a ≤ b or b ≤ a for all a, b ∈ IK. –

An ordered semiring preserves the order if for all a, b , c ∈ IK: c≤b +  c , a a≤b ⇒a+ · c ≤ b · c and c · a ≤ c · b.

• •

It is partially ordered if ≤ is a partial order. It is commutative if multiplication is commutative.

Discrete Event Dyn Syst (2010) 20:103–137

• •

107

 a = a for all a ∈ IK). It is idempotent if addition is idempotent (i.e., if a + It is closed if infinite addition is defined and behaves as finite addition (i.e., converges towards some value in the semiring).

We define a < b if a ≤ b and a  = b . The supremum sup(a, b ) of a, b ∈ IK is a if a > b and b otherwise, the infimum inf(a, b ) is a if a < b and b otherwise. To make the notation simpler, we use sometimes IK for the whole semiring, ab is used for a ·b and an is used for the n fold product. The well known Boolean semiring (IB, ∨, ∧, 0, 1) is order preserving, commutative, idempotent, and closed whereas (IR≥0 , +, ∗, 0, 1) is order preserving and commutative, but not idempotent and not closed. The semirings (IR≥0 ∪ {−∞}, max, +, −∞, 0) and (IR≥0 ∪ {∞}, min, +, ∞, 0) are order preserving, idempotent, and commutative, but not closed. However, they are closed if ∞ or −∞ respectively are added as elements.  a3 +  ... = a+  a2 + Furthermore, we define for a ∈ IK the unary operation a∗ =  1+  ∞    n=1 an (Aho et al. 1974; Fletcher 1980). If a∗ ∈ / IK we write a∗ = ⊥. For 1 + (IB, ∨, ∧, 0, 1), a∗ = 1. For (IR≥0 , +, ∗, 0, 1), a∗ = (1 − a)−1 if a < 1 and ⊥ otherwise. If we extend the semiring to (IR≥0 ∪ {∞}, +, ∗, 0, 1) then a∗ = ∞ for a ≥ 1. If we consider (IR ∪ {∞}, +, ∗, 0, 1), then we see the well-known results for a geometric series ⎧ ⎨ (1 − a)−1 for − 1 < a < 1 , ∗ for 1 ≤ a , a = ∞ ⎩ ⊥ otherwise . The operation a∗ will later be used to compute results for infinite paths in weighted automata. Definition 2.3 A finite weighted automaton over semiring IK and over a finite alphabet L is a 4 tuple A = (S , α, T, β), where 1. S = {s0 , . . . , sn−1 } is the finite state space,2 2. α : S → IK is the initial weight function, 3. T : S × L × S → IK is the transition function, 4. β : S → IK is the final weight function. The transition function T computes a transition weight for each label and each pair of states. Independently of the used semiring, T(x, a, y) =  0 implies that no a-labeled transition between state x and state y exists. This is a common assumption which is often implicitly made when defining transition systems. The definition assures that between two states there exists at most one transition that is labeled with a fixed label a. For some automata models, initial and final weight functions are useful to be able to define sets of initial and final states, for others this generality is not necessary. If this is the case, the functions may be substituted by constant  1, which is the neutral element with respect to multiplication; this allows us to proceed with a uniform formal treatment.

the state space is isomorphic to the set of integers {0, . . . , n − 1}, we use this notation for the set of states, whenever possible.

2 Since

108

Discrete Event Dyn Syst (2010) 20:103–137

The class of weighted automata is well known in automata theory (Eilenberg 1974). The formulation applied here is proposed in Buchholz (2008). In Buchholz and Kemper (2001), a process algebra is presented that is based on the above concepts in the sense that its dynamic behavior yields an automaton with transition weights; however, a term in a process algebra may define an automaton with an infinite number of states. Different semirings yield completely different automata. Before we present some concrete cases for particular semirings, we consider general methods to analyze the behavior of automata with transition weights. The behavior of a weighted automaton considers the weights of paths between states where a path is described by a finite or infinite sequence of transition labels. Algorithms to compute paths and their corresponding weights for weighted automata, respectively directed graphs with edge weights are known. The total cost of all paths between each pair of nodes (states) can be computed in O(n3 ) by an algorithm described by Aho et al. (1974) and generalized by Fletcher (1980) for the case of weights taken from a closed semiring. Finding the shortest distances for a single node to all other nodes can be computed with a generic algorithm presented by Mohri, which either applies to acyclic graphs with weights taken from any semiring or to directed graphs in general if the semiring is commutative and k-closed for that graph (Mohri 2002), a restriction that is necessary to bound the impact of cycles in the graph. The complexity of Mohri’s generic algorithm depends on the semiring and the type of graph. For the case of acyclic graphs, its topological single-source shortest distance variant is shown to be linear. To analyze the behavior of an automaton over all paths, we present an approach that is based on vector-matrix computations because this is a convenient approach to compute these results. Since we consider automata over finite state spaces and finite sets of transition labels, each automaton can be described by sets of IKn×n matrices and IKn vectors.  Thus, we define for each a ∈ L a matrix Ma with Ma (x, y) = T(x, a, y) and M =  a∈L Ma as a matrix that collects all weights independently of the labels. Furthermore, we define a row vector a with a(x) = α(x) and a column vector b with b(x) = β(x). To complete the notation, let I be the n × n identity matrix over semiring IK, let 0 be a n × n matrix with all elements equal to  0, let ei ∈ IKn be a row vector with  1 in position i  (0 ≤ i < n) and 0 elsewhere and let eT be a column vector where all elements equal to  1. It is straightforward to define matrix sum and product using the operations of the semiring instead of the usual multiplication and addition. We start with the analysis of paths and introduce some notations first. We use x, y, z for states and i, j, k for running indices in sums or products. A path of automaton A is defined as a sequence of states and transitions starting in a state x ∈ S with α(x)  =  0. In automata theory paths may be defined by sequences of states or transitions or both. We use here a definition that observes transitions via their labels and states. However, the approach can be easily restricted to observe only states or only transitions. Let π be a path, π s the sequence of states in the path and π t the transition labels. We denote by πis ∈ S (i = 0, 1, 2, . . .) the i-th state in the path and by π tj ∈ L ( j = 1, 2, . . .) the j-th transition label. Thus, π = (π0s π1t π1s . . . ) is a path t s of automaton A if α(π0s )  =  0 and T(πis , πi+1 , πi+1 ) =  0 for all i. A path might be of infinite or finite length. In the finite case, index i runs from 0 to |π | where |π | is the length of the path, i.e., the largest index i in the path. Let σ be the set of paths of automaton A, σx the set of paths that start in state x, σ m (σ ≤m ) the set of paths of

Discrete Event Dyn Syst (2010) 20:103–137

109

length m (≤ m) and σxm (σx≤m ) the set of paths of length m (≤ m) that start in state x. For each finite path, we can compute the weights as (ce = costs each) · ce(π ) = α(π0s )

  |π| i=0

t s s T(πis , πi+1 , πi+1 ) · β(π|π| )

(1)

m where  i=1 ai = a1  · ... · am and the case of finite m might be extended to m = ∞, if the semiring is appropriately chosen such that the infinite product can be computed. If we focus on observing the behavior of an automaton by considering a sequence of labels seq = a1 , . . . , am with ai ∈ L for a path π , then one does not want to distinguish among paths π and π  that produce the same sequence seq. Thus, define σ (seq) as the set of paths that are labeled with seq and let σx (seq) be the set of all paths labeled with seq that start in state x. The weights summed over all paths with labeling seq starting in state x are given by (ca = costs all)

m 

 ·b, (2) ce(π ) = a(x) · ex  · Mai  cax (seq) = π∈σx (seq)

i=1

and the weights of all paths of length m with an arbitrary labeling is computed as · ex  · Mm  · bT . cax (∗m ) = a(x)

(3)

The above computation of weights assumes that a specific initial state is known. Alternatively, one can consider the case that vector a defines the weights of initial states. The weights of all paths for a sequence of labels seq are then defined as

m 

 ca(seq) = · b and ca(∗m ) = a ce(π ) = a · Mai  · Mm  · b. (4) π∈σ (seq)

i=1

Apart from the weights of paths, we consider possible terminating states and the weights of reaching those states. These values are described by a row vector m

 dseq = a · Mai , (5) i=1

such that ca(seq) = dseq  · b. Example 2.1 We consider a simple model of a driving test to illustrate the concept, Fig. 1 gives an automaton with S = {A, B, . . . , H, L} and L = {l, d, f, e}. Let L be the initial state, so we define the initialization function α(s) =  1 if s = L and  0 otherwise. When a student starts, he/she takes a couple of lessons, which are transitions with label l (lesson). After at least one lesson, the student may be confident to start the test (state A) and drive around with the examiner (actions with label d for drive). While driving the examiner may decide to finish (actions with label f ) and to assign the desired driver’s license in state H (Hooray). Alternatively, the student may make some errors (actions with label e for error) that lead him/her to less hopeful situations D, E, or F where, after further driving, the examiner will finally decide to finish (actions with label f ) and refuse the license. This yields state G. From there, the poor student can only return to L and take some more lessons. State H is the desired result, so we define β(s) =  1 if s = H and  0 otherwise. We will consider this example with different semirings and different transition functions (assignment of weights),

110

Discrete Event Dyn Syst (2010) 20:103–137

Fig. 1 Example automaton, a driving test model

f d

A

B

d d

H

d f

l

l

C

f

e

L

D

e

e e e

d f

l

e

d F

E f

d

f

G

e.g., the Boolean semiring (IB, ∨, ∧, 0, 1) is useful to ask for existence of paths that lead to a driver’s license (state H), or whether all paths lead to this state, i.e., if success is guaranteed. For the Boolean semiring, function T is defined by assigning  1 = 1 to all arcs present in Fig. 1. ([0, 1], +, ·, 0, 1) is useful to achieve a probabilistic model, where actions are randomly selected and one may ask for the probability to succeed. If one asks for trouble, one can use (IR≥0 ∪ {−∞}, max, +, −∞, 0) to look for the hardest path to success, and (IR≥0 ∪ {∞}, min, +, ∞, 0) for the one with minimal stress, given that weights indicate how much energy is necessary to perform that action.

3 Valued computational tree logic The usual way of describing dynamic properties of a system is by temporal logics which exist in various forms. Very popular is the branching time logic CTL (Clarke et al. 1986). CTL formulas are interpreted over labeled transition systems and efficient algorithms for model checking finite systems exist (Burch et al. 1992) and have been implemented in software tools (Berard et al. 2001). CTL allows us to check properties of paths of an automaton where an universal- or existential-quantifier has to precede any path quantifier. Since CTL is defined for transition systems where transitions are not weighted, it cannot be used to derive non-functional properties. To express such properties, the logic has to be extended as done by several authors. The logic RTCTL is described in Emerson et al. (1992) as an extension of CTL. RTCTL, in contrast to CTL, allows us to take timing considerations into account. Thus, it can be expressed that a property will become true within 50 time units or that a property holds for 20 time units. Time is discrete in this model and one transition takes exactly one time step. In Hansson and Jonsson (1994), the logic PCTL is introduced that can be used to describe properties that hold for some time (or after some time) and hold with at least a given probability. Thus, this logic extends RTCTL

Discrete Event Dyn Syst (2010) 20:103–137

111

with respect to probabilities. Formulas of PCTL are interpreted over discrete time Markov chains (DTMCs) and the model checking problem for PCTL is polytime decidable (Beauquier and Slissenko 1998). In this model, time is also discrete and one transition lasts one time step. In this paper, we extend CTL by defining a logic for weighted automata. Since our automata model contains transition labels we extend our logic by propositions that allow us to reason over labeled transitions as it is done in Hennessy-Milner logic (Hennessy and Milner 1985; Milner 1989). In this respect, Valued Computational Tree Logic (CTL$) might not be the natural name for the logic. However, since CTL is included in the logic CTL$ as a special case of automata over the Boolean semiring, we choose this name. We first define basic CTL$ formulas, introduce informally the semantics of a formula, and define some derived expressions afterwards. Later we show also that CTL$ includes also RTCTL and PCTL, if applied for automata over the corresponding semirings. Definition 3.1 For a given set of atomic propositions, the syntax of a CTL$ formula for an ordered or partially ordered semiring IK is defined inductively as follows: • • • •

An atomic state proposition  is a CTL$ formula, if 1 and 2 are CTL$ formulas, then ¬1 and 1 ∨ 2 are CTL$ formulas, if  is a CTL$ formula, a ∈ L and p ∈ IK, then [a] p . and [∗] p . are both CTL$ formulas, if 1 and 2 are CTL$ formulas, t is a nonnegative integer or ∞ and p ∈ IK, then t t 1 U  p 2 and 1 AU  p 2 are CTL$ formulas

where ∈ {<, ≤, =, ≥, >}. Formulas of CTL$ are interpreted over weighted automata. A necessary condition to interpret a formula for an automaton is that both use the same semiring IK, which will be assumed in the sequel. Atomic propositions of the kind  : S → IB describe elementary properties that hold or do not hold in a state x ∈ S of an automaton. The goal of model checking is to compute the set of states for which a CTL$ formula  holds. Before we define formally for which states a formula holds, we present the intuitive meaning of the formulas, i.e., we describe under which conditions formula  holds for state x. • • • • •

An atomic proposition  is true in x ∈ S , if the proposition holds in x. ¬ is true in x if  is false in x; 1 ∨ 2 is true in x if 1 or 2 is true in x. [a] p . is true in x if w  p holds where w denotes the sum of weights of alabeled transitions that leave x and end in some state where  holds. [∗] p . is similar, but the labels of transitions do not matter. t 1 U  p 2 is true in x, if the sum of weights w of all paths in a certain set observes w  p. That set consists of all paths that start in x, fulfill 1 until they reach a state where 2 is fulfilled and that are not longer than t. t t 1 AU  p 2 is true in x, if 1 U  p 2 holds in x and additionally, for all paths π ∈ σx , there exists some u ≤ t such that 1 holds in πvs with v < u and 2 holds in πus . This operator is more strict than the previous one, it requires all paths to observe conditions.

112

Discrete Event Dyn Syst (2010) 20:103–137

We use the notations x |=  if formula  holds in x and x  |=  if this is not the case (i.e., x  |=  ⇔ x |= ¬). The meaning of the first two cases above is obvious. For a formal definition of the last three cases, we make use of a description by vectors and matrices and introduce some additional notations first. For some matrix R ∈ IKn×n and two CT L$ formulas 1 and 2 , let R[1 , 2 ] ∈ IKn×n be defined as  R(x, y) if x |= 1 and y |= 2 R[1 , 2 ](x, y) =  0 otherwise Consequently, matrix M[1 , 2 ] (Ma [1 , 2 ]) contains all transitions (labeled with a ∈ L) that start in a state where 1 holds and end in a state where 2 holds and I[, ] is a matrix that contains  1 in the main diagonal whenever  holds for the corresponding state and all other elements are  0. Furthermore, let for some vector x, x[] = xI[, ]. With these notations, we can formally define the meaning of the presented CTL$-formulas using vectors and matrices rather than considering specific paths. • • •

x |= [a] p . if and only if w  p with w = ex Ma (e[])T . x |= [∗] p . if and only if w  p with w = ex M(e[])T . t x |= 1 U  p 2 if and only if w  p with ⎧ t−1  ⎪ ⎨ a(x)ex  k=0 (M[1 ∧ ¬2 , 1 ∧ ¬2 ])k w= if t > 0 and x  |= 2 M[1 ∧ ¬2 , 2 ]b[2 ] ⎪ ⎩ a[2 ](x)b[2 ](x) if t = 0 or x |= 2

•

If 2 already holds in x or paths of length 0 are considered, then the weight is given by the product of the initial weight from vector a and the final weight from vector b. Observe that a[](x) = b[](x) =  0 for x  |= . For a path length > 0 the weights of paths through states where 1 but not 2 holds until they reach a state where 2 holds are added. t t x |= 1 AU  p 2 if and only if x |= 1 U  p 2 where the weight is computed as before and for all π ∈ σx there exists some m ≤ t such that πms |= 2 ∧ (πis |= 1 ∧ πis  |= 2 ) for 0 ≤ i < m.

CTL$ contains an universal but no existential quantifier. The reason for this decision is that the existential quantifier can be described by the general path quantifier U using U >t 0 , if a · b = 0 implies a =  0 or b =  0 (i.e., the semiring is entire Baccelli et al. 1992, p. 155). For instance, the Boolean semiring is a case where U >t 0 is suitable to decide existence of a path. Another reason for not introducing an existential quantifier for paths is that in general semirings this quantifier is not indistinguishable under the notion of bisimulation we use in Section 5. Thus, bisimilar automata (see Section 5) still might be distinguished via CTL$ formulas including path quantifiers considering single paths. This is in some sense against the idea of bisimulation and its connection to logics.

Discrete Event Dyn Syst (2010) 20:103–137

113

Note that the quantifier AU first requires that U holds and additionally it has to be checked whether the condition holds for all paths. The latter can be checked using a procedure that is derived from the procedures used in CTL to check A[1 U2 ] (see e.g. Berard et al. 2001, p. 49). Since the original algorithm only works for t ≥ n, we provide below a slightly extended version of the algorithm that can be applied to all path lengths. To apply the algorithm, transition weights a  =  0 are interpreted as 1 and transition weight  0 is interpreted as 0. AU is necessary to make CTL$ equivalent to CTL if weighted automata are defined over the Boolean semiring. Since CTL$ shall not be less expressive than CTL, AU must be included. Several other operators can be derived from the basic operators of CTL$. The operators ∧ and → are derived in the obvious way. With the help of negation, one t can show that for path formulas with 1 U  p 2 , not all operators for comparisons t  are essential for an ordered semiring. We present the relation for 1 U  p 2 and omit index p, for readability.   1 U t 2 ) 1 U ≤t 2 = ¬(1 U >t 2 ) 1 U ≥t 2 = (1 U =t 2 ) ∨ (1 U >t 2 )

1 U =t 2 = (1 U ≥t 2 ) ∧ ¬(1 U >t 2 )

The last equality shows that we may as well use ∈ {>, ≥} to derive all other t relations for 1 U  p 2 . This will be done in the following section because > and ≥ can be easily checked in the algorithms. Similarly, we have the following relation for [a] p where p is again omitted for readability. [a]< = ¬ ([a]= ∨ [a]> ) , [a]≤ = ¬[a]> , [a]≥ = [a]= ∨ [a]> and [a]= = [a]≥ ∧ ¬[a]> Again, it is sufficient to consider ∈ {>, ≥}. If the semiring is only partially ordered, we cannot conclude that ¬( p ≥ q) implies p < q. Consequently, for partially ordered semirings all comparison operators are required. The following abbreviations are defined by extending the corresponding CTL$ formulas. • •

AX p  = [∗] p . ∧ [∗]=0 .¬ and U X p  = [∗] p . t t t t AF p  = true AU  p  and U F p  = true U  p .

X corresponds to a next operator. F denotes a finally operator. Such operators are common syntactic sugar of modal logics. Note that [∗]=0 .¬ ensures absence of any transition to a state x |= ¬, if the semiring is zero sum free.

4 Model checking CTL$ formulas To perform model checking in a more efficient way, we first restrict the semiring used for transition valuation. We assume that the semiring is ordered, and that the order is preserved by the operations. Observe that these conditions are satisfied in most

114

Discrete Event Dyn Syst (2010) 20:103–137

semirings of relevance in practice, for instance in the examples presented below. To illustrate the point, (IR, +, ·, 0, 1) is ordered but does not preserve the order due to the fact that a ≤ b does not imply a · c ≤ b · c if c < 0, but (IR≥0 , +, ·, 0, 1) preserves the order. At the end of the section, we show how the proposed algorithms can be extended to more general semirings. We follow other model checking approaches as Clarke et al. (1986) and define how a formula is checked in an inductive manner over the length of a formula. • • • • •

leng() = 1 if  is an atomic proposition, leng(¬) = leng() + 1, leng(1 ∨ 2 ) = max(leng(1 ), leng(2 )) + 1, leng([a] p .) = leng([∗] p .) = leng() + 1, and t t leng(1 U  p 2 ) = leng(1 AU  p 2 ) = max(leng(1 ), leng(2 )) + 1.

As in CTL model checking the set of states satisfying a formula of length l is computed after all sets of states that satisfy sub-formulas of length < l are known. Computation of the sets of states that observe atomic propositions, ¬, or 1 ∨ 2 , is identical to the corresponding computations in CTL. Thus, the new cases are t t [a] p ., 1 U  p 2 , and 1 AU  p 2 . We describe a procedure for each of the three formulas that computes for each state whether it observes the formula or not. We present only cases of ∈ {>, ≥}, since the other cases can be derived from these cases as shown above. Let marked(x) be a variable that is true if x |=  and false otherwise. For the presentation of the algorithms, we use the vector matrix representation of the automaton which is also well suited for an implementation of the algorithms. An algorithm to compute [a] p ..

The inner for-loop can be left if sum  p because due to our assumptions the value of sum cannot be reduced with respect to ≤ or <. A modification of the algorithm to compute [∗] p . is immediate.

Discrete Event Dyn Syst (2010) 20:103–137

115

t An algorithm to compute 1 U  p 2 for t < ∞.

Steps 1 through 13 of the algorithm describe the initialization phase, several special cases are decided directly. A state x that satisfies 2 also satisfies 1 U ≥t p 2 if a(x)  · b(x)  p. If “” = “≥” and (a(x)  · b(x) < p), then x does not satisfy the formula, because on all paths starting in x, 2 immediately holds for the first time

116

Discrete Event Dyn Syst (2010) 20:103–137

and the weights of these paths are too small such that the whole formula is false. For states where 1 and 2 both do not hold, the formula is false too. In the remaining cases, it is not clear yet whether the formula holds or not and those states are marked as undecided with respect to this formula. u, v, w are arrays of length n to represent column vectors. In steps 14 through 25, transitions of the automaton between states where 1 but not 2 holds are mimicked step by step. In each step l, we compute per state x, where only 1 holds, the sum of weights of paths of length l that end in a state where 2 holds and that pass through states where only 1 holds. These weights are collected in vector w. The weights of all those paths of length of at most l are accumulated in vector u. The iteration stops if t steps have been computed, which means that all paths of length ≤ t have been considered, or if all states are classified, i.e., no state is marked as undecided. After leaving the iteration over all paths of length ≤ t, all states that are still marked undecided do not satisfy the formula because no appropriate path can be found for them. The procedure eventually stops for finite t. For some semirings we may even reduce t to n, if t > n holds, as shown in the examples below.  t t  t Rk as subproblems. Evaluation of 1 U  p 2 involves computation of R and k=0 In the algorithms given so far, those subproblems are solved by successive matrixvector multiplications, which avoids an explicit computation of P = Rt and Q =   t Rk . If the space used to represent P or Q is tolerable for an application, those k=0 matrices can be computed with less steps by using iterated squaring if the semiring is idempotent. Iterated squaring is well known, e.g., to compute a transitive closure of the graph which corresponds to the Boolean semiring. To compute P, we can use  a binary representation of t = lj=0 δ j2 j with l = log(t) and δ j ∈ {0, 1} such that l j j 1 2 l P =  j=0 δ jR2 and R2 is obtained by computing a sequence R, R2 , R2 , . . . , R2 with l matrix–matrix multiplications. Iterated squaring to compute P works for semirings in general. In case of an idempotent semiring, we can use that approach t  I)t =  k=0 Rk in case of for Q as well. It is straightforward to verify that (R + an idempotent semiring. We briefly recall the induction argument for this known result. Obviously, the result is true for t = 0. For t > 0, we first use the induction hypothesis and the idempotency of the semiring, in this way we have (R + I)t = t−1 t−1 t t   k=0 Rk =  k=0 Rk . Hence, (R + I)t−1  · (R + I) =  k=0 Rk  · (R + I) =  k=1 Rk + t−1 for idempotent semirings, we can for instance compute  k=0 (M[1 ∧ ¬2 , 1 ∧ k t ¬2 ]) and (M[1 ∧ ¬2 , 1 ∧ ¬2 ]) with at most log(t) matrix–matrix multiplications and additions. For t = ∞, the situation is different. In principle, we can use the above procedure, but it cannot be assured whether it stops or yields an infinite computation. The crucial point is the computation of the infinite sum of matrices N[1 ∧ ¬2 , 1 ∧ ¬2 ] =



∞ k=0

(M[1 ∧ ¬2 , 1 ∧ ¬2 ])k .

The following relation holds if M[1 ∧ ¬2 , 1 ∧ ¬2 ] can be reordered to an upper triangular matrix. 

∞ k=0

(M[1 ∧ ¬2 , 1 ∧ ¬2 ])k =



n k=0

(M[1 ∧ ¬2 , 1 ∧ ¬2 ])k

Discrete Event Dyn Syst (2010) 20:103–137

117

The relation is true since Rk = 0 for k > n if R ∈ IKn,n is an upper triangular matrix. In this case and for t ≥ n t n x |= 1 U  p 2 ⇔ x |= 1 U  p 2

such that the above algorithm for finite t can be applied for the infinite case as well. For the general case where M[1 ∧ ¬2 , 1 ∧ ¬2 ] cannot be reordered to an upper triangular form, the algorithm from Fletcher (1980) can be applied. Let C ∈ IKn×n×n and initialize C(0, x, y) = M[1 ∧ ¬2 , 1 ∧ ¬2 ](x, y). Then the following algorithm is used.

C(z, x, y) contains the weights of all paths between x and y that pass through states with indices < z. Consequently, N[1 ∧ ¬2 , 1 ∧ ¬2 ](x, y) = C(n, x, y) (see Fletcher 1980). The computational complexity of the algorithm is O(n3 ), assuming that addition, multiplication and closure each take constant time, and the values can be computed if a∗ can be computed for all values that appear in the inner loop. ∞ If N[1 ∧ ¬2 , 1 ∧ ¬2 ] is available, then 1 U  p 2 can be checked using an extension of the algorithm for the finite case, where the steps 14 through 25 are substituted by the following steps.

t t An algorithm to compute 1 AU  p 2 . To analyze x |= 1 AU  p 2 , we have to t evaluate if two conditions hold. We start with x |= 1 U  p 2 and use the algorithm we presented above. If this condition holds, we then check the second condition, namely if for all paths π ∈ σx there exists some l ≤ t such that πls |= 2 ∧ (πis |= 1 ∧ πis  |= 2 ) for 0 ≤ i < l. This condition depends on the weights of transitions only in a very limited manner; it only distinguishes if weights are  0 or not. If the value of t allows us to consider long enough paths, i.e., t ≥ n, the condition can be checked in the same way as A[1 U2 ] in CTL. An algorithm to check this formula in CTL is given in Berard et al. (2001, p. 41). We present here an extended version that allows one to consider only paths up to length t. This algorithm corresponds to the algorithm

118

Discrete Event Dyn Syst (2010) 20:103–137

checking 1 AU ≤t 2 in RTCTL which is proposed in Emerson et al. (1992, p. 337). Let marked be an array of length n that is initialized as follows: ⎧ if x |= 2 ⎨ true if x  |= 1 and x  |= 2 marked(x) = f alse ⎩ undecided otherwise Additionally, we use for each state x a counter x.nb that counts the number of successors. Furthermore, we use a Boolean matrix B with B(x, y) = 1 if Ma (x, y)  =  0 for some a ∈ L and B(x, y) = 0 otherwise. The following algorithm is applied.

We now consider correctness and termination of the algorithm. The algorithm terminates since in the first step all states x with marked(x) = true are added to L, in subsequent steps a state x is inserted into L only if marked(x) is changed from undecided to true. Afterwards the value marked(x) is not modified again. Thus, each state can be added to L, resp. L at most once, each newly added state remains in L only for one iteration of the while-loop (lines 5-14,) and the algorithm terminates if L becomes empty. t To show the correctness, let Kt be the set of all states x |= 1 AU  p 2 , i.e., by s definition, for all π ∈ σx there exists some l ≤ t such that πl |= 2 and πis |= 1 and πis  |= 2 for 0 ≤ i < l. Let Lt = Kt \ Kt−1 for t > 0 and L0 = K0 . Obviously Kt = t ∪l=0 Ll . L0 contains all states x |= 2 . Lt with t > 0 contains only states x |= 1 . A

Discrete Event Dyn Syst (2010) 20:103–137

119

state x  |= 2 that belongs to Kt can only have successor states in Kt−1 because Kt−1 contains all states that fulfill 1 AU ≤t−1 2 ; having any successor y ∈ / Kt−1 implies ≤t that x does not fulfill 1 AU 2 . In the same way it can be argued that x ∈ Lt has to have at least one successor in Lt−1 because otherwise x would belong to Kt−1 . Consequently, if Lt = ∅, then Kt = Kt+s for all s ≥ 0. In step k (each step is one iteration of the while-loop in lines 5-14), the algorithm computes the set L = Lk from L = Lk−1 and Kk = {x|marked(x) = true} which can be shown by induction. For t = 0, L is initialized with all states where 2 is fulfilled, so L = L0 is correct and the while-loop in lines 5-14 is skipped (zero iterations) since there is no need to compute L = L1 . K0 is correct due to the initialization of marked(x). For t > 0, iterations through the while-loop take place and we assume that set L = Lk−1 and {x|marked(x) = true} = Kk−1 at the beginning of a step k, where k is the value of the variable k. A state y is put into L , if y |= 1 (due to marked(y)=undecided), if it has at least one successor x ∈ Lk−1 , and if all its successors are in Kk−1 . Thus, L = Lk and L becomes L in the next iteration. Since marked(y) := true (line 11) for all y added to L also Kk = {x|marked(x) = true} = k−1 l L is updated accordingly in each iteration of the while-loop. If L Kk−1 ∪ L = ∪l=0 becomes empty, then the algorithm can be stopped and it can also be stopped if k > t since then all paths up to length t have been considered and all states that are not marked true are the origin of a path violating the required conditions. The computational complexity for the algorithm is in O(nz) where nz is the number of non-zero elements in M which is at most n2 . t t Thus, we have x |= 1 AU  p 2 if and only if x |= 1 U  p 2 and marked(x) = true. Checking CTL$ formulas is also possible for more general semirings that are not order preserving. The proposed algorithms can still be applied given that those parts are removed that terminate a loop due to w  p. All decisions that rely on comparisons w  p must be delayed until the end of the procedures since values can change in a non-monotonic manner. We give some complexity results of the algorithms for different semirings at the end of Section 6.

5 Bisimulation for weighted automata Bisimulation for weighted automata has been introduced in Buchholz (2008) and Buchholz and Kemper (2001). In Buchholz and Kemper (2001), it has been shown that bisimulation is a congruence with respect to the operations of the process algebra GPA. Here, we briefly rephrase and slightly extend the definition for bisimulation given in Buchholz (2008) and Buchholz and Kemper (2001) and prove afterwards that bisimilar states of an automaton are indistinguishable under CTL$ formulas. We consider here only equivalence relations as bisimulations. Let R be an equivalence relation on S × S . S /R is the set of equivalence classes of R, C ∈ S /R is an equivalence class of R and C[x] is the equivalence class to which state x ∈ S belongs. If we consider equivalence classes of different equivalence relations R i , we use CRi for an equivalence class from S /Ri . We define for C ⊆ S : Ma (x, C) =  y∈C Ma (x, y).

120

Discrete Event Dyn Syst (2010) 20:103–137

Definition 5.1 An equivalence relation R for an automaton A is a bisimulation if and only if ∀(x, y) ∈ R, ∀C ∈ S /R and ∀a ∈ L:   1.  z∈C T(x, a, z) =  z∈C T(y, a, z), equivalently Ma (x, C) = Ma (y, C), 2. α(x) = α(y), equivalently a(x) = a(y), 3. β(x) = β(y), equivalently b(x) = b(y), and 4. AP(x) = AP(y) where AP(x) is the set of atomic propositions satisfied by x. The definition is a natural generalization of the definition of bisimulation that had been first defined for finite automata (Park 1981) and later been extended to probabilistic (Larsen and Skou 1991) and stochastic systems (Buchholz 1994; Hillston 1994). Intuitively, a bisimulation defines a set of equivalence classes such that for all states in an equivalence class, the same atomic propositions hold, the initial and final weights are identical and the sums of transition weights of outgoing transitions into any equivalence class are identical. We define the union of two bisimulations R1 and R2 via the union of their equivalence classes. Thus, R0 = R1 ∪ R2 is characterized by the equivalence classes CR0 [x] = CR1 [x] ∪ CR2 [x] for all x ∈ S . With this definition the union of bisimulation relations yields a bisimulation relation. Theorem 5.1 Let R1 and R2 be two bisimulations for automaton A, then R = R1 ∪ R2 is also a bisimulation. Proof The proof is a simple extension of the proof in Buchholz (2008), one needs to consider the additional condition AP(x) = AP(y) of Definition 5.1, which is straightforward. Additionally, R is an equivalence relation since it results from the union of equivalence classes.   Thus, the largest bisimulation for an automaton can be defined as the union of all bisimulations. We use the notation x ∼ y for x, y ∈ S , if a bisimulation R with (x, y) ∈ R exists. The bisimulation can be extended to compare automata instead of states. This is commonly done for untimed automata as in Milner (1989) but requires slight extensions if applied to the general automata model presented here. Functions α and β require an additional condition. We define the union of automata in the usual sense and bisimulation of automata by means of a bisimulation relation on the union. Definition 5.2 Let A1 = (S1 , α1 , T1 , β1 ) and A2 = (S2 , α2 , T2 , β2 ) be two weighted automata defined over the same semiring IK, identical alphabets L, and S1 ∩ S2 = ∅. The union A1 ∪ A2 is defined as an automaton A0 = (S0 , α0 , T0 , β0 ) with • • • •

S0 = S1 ∪ S2 ,⎧ ⎨ T1 (x, a, y) if x, y ∈ S1 , T0 (x, a, y) = T2 (x, a, y) if x, y ∈ S2 , ⎩ 0 otherwise. α0 (x) = α1 (x) if x ∈ S1 and α2 (x) for x ∈ S2 , and β0 (x) = β1 (x) if x ∈ S1 and β2 (x) for x ∈ S2 .

Discrete Event Dyn Syst (2010) 20:103–137

121

Definition 5.3 Automata A1 and A2 are bisimulation equivalent, if a bisimulation relation R exists for A0 = A1 ∪ A2 and for all C ∈ S /R: 

x∈C∩S1

α(x) =



x∈C∩S2

α(x) and



x∈C∩S1

β(x) =



x∈C∩S2

β(x)

In terms of matrices, A0 = A1 ∪ A2 yields Ma (0) =



Ma (1) 0 0 Ma (2)



  , a(0) = a(1) , a(2) , b(0) =

b(1) b(2)

.

where automaton Ai is characterized by the matrices Ma(i) and the vectors a(i) and b(i) . Example 5.1 Driving test, continued. Figure 2 shows a model which is bisimilar to the one in Fig. 1 provided a semiring is given and functions T, α and β and sets AP are appropriately defined. Let AP = {ok, learn} and AP(x) = {learn}∀x ∈ {A, B, C, D, E, F, G, G , L, L , ABC, DEF} and AP(x) = {ok} for all x ∈ {H, H  }. So by definition of α, β, and AP, we have 3 candidates for equivalence classes {H, H  }, {G, G , L, L } and S \{G, G , L, L , H, H  } to fulfill conditions 2-4 of the definition. By assuming T(x, a, y)  =  0 for all arcs in Figs. 1 and 2 and  0 otherwise,   we need to partition S \{L, L , H, H } into sets {A, B, C, ABC} and {D, E, F, DEF} and to partition {L, L , G, G } into {L, L } and {G, G }. For the Boolean semiring, addition is ∨ in Definition 5.1, condition 1, so it is straightforward to verify that this partition gives a bisimulation, i.e., L ∼ L , G ∼ G , H ∼ H  , A ∼ ABC, B ∼

Fig. 2 Possible bisimilar model of the driving test example

f

d ABC l l

f e

L’

d DEF

l

f G’

H’

122

Discrete Event Dyn Syst (2010) 20:103–137

ABC, C ∼ ABC, D ∼ DEF, E ∼ DEF, and F ∼ DEF. If we choose the semiring (IR≥0 , +, ·, 0, 1), we achieve the same bisimulation if we define M0 for example as follows:

The entries give the arc weights, while the index indicates the associated label, e.g., M0 (L, A) =2l−1 indicates T0 (L, l, A) = 1/2, which corresponds to a transition in the first automaton. Additional lines have been added to the upper left block that corresponds to M(1) to highlight blocks whose row and column sets correspond to sets of bisimilar states. To see if a partition is a bisimulation, we need to check elements of each class with respect to Definition 5.1. For example, for A ∼ ABC, we need to consider all classes and labels, e.g., class DEF and label e, −1  −1   1  M0 (A, E) +  M0 (A, F) = 6−1 M0 (A, D) + e + 6e + 0 = 3 = 3e = M0 (ABC, DEF). Matrix entries that are  0 are omitted for clarity. The following theorem introduces the relation between bisimulation equivalence for weighted automata and CTL$ formulas, which is similar to the relation between bisimulation and CTL in untimed automata. Theorem 5.2 If x ∼ y, then 1. 2. 3. 4. 5.

x |=  ⇔ y |=  for all  which are logical combinations of atomic propositions, x |= [a] p . ⇔ y |= [a] p . and x |= [∗] p . ⇔ y |= [∗] p ., t t x |= 1 U  p 2 ⇔ y |= 1 U  p 2 , t t x |= 1 AU  p 2 ⇔ y |= 1 AU  p 2 and x |= ¬ ⇔ y |= ¬

where , 1 and 2 are CTL$ formulas. Proof 1. holds since AP(x) = AP(y) for x ∼ y such that also all logical combinations of atomic propositions yield identical results.

Discrete Event Dyn Syst (2010) 20:103–137

123

2. is proved inductively for the [a] p . by assuming that for x ∼ y: x |=  ⇔ y |= . Then x |= [a] p . ⇔ y |= [a] p . since Ma (x, C) = Ma (y, C) and all states in an equivalence class either fulfill  or do not fulfill . We use the notation C |=  if the states of class C fulfill . This implies that the weight of transitions ending in a state where  holds equals 

C,C|=

Ma (x, C) =



C,C|=

Ma (y, C)

Initially we know that AP(z) is the same for all z ∈ C such that the relation holds for all  which are logical combinations of atomic propositions. By induction the relation also holds for  containing an arbitrary number of constructs of the form [a] p .. For more general formulas we combine the induction used in this step with the induction presented for 3. and 4. below. The proof for the second statement [∗] p . is analogous. 3. and 4. have to be proved inductively over the number of occurrences of t t 1 U  p 2 and 1 AU  p 2 in the formula and over the length t of the required paths. First assume for x ∼ y: x |= 1 ⇔ y |= 1 and x |= 2 ⇔ y |= 2 t which is proved for formulas 1 and 2 that do not contain 1 U  p 2 t t t or 1 AU   . Now we prove x |=  U  ⇔ y |=  U 2 1 2 1 p  p  p 2 inductively over t. For t = 0 we have:

a(x)b(x) = a(y)b(y) such that the formula holds for x ∼ y. Define for C ∈ S / ∼: ξ(C) = b(z) for some (all) z ∈ C and let δ(C, ) =  1 if for some (all) z ∈ C: z |=  and  0 otherwise. Due to our assumptions about bisimulations we have for all z ∈ C b(z) = ξ(C) and δ(C, ) = 1 ⇔ z |= . For t = 1, the following relation holds for x ∼ y and all C ∈ S / ∼: a(x)



z∈C

M[1 ∧ ¬2 , 2 ](x, z)b[2 ](z)

= a(x)M[1 ∧ ¬2 , 2 ](x, C)ξ(C)δ(C, 2 ) = a(y)M[1 ∧ ¬2 , 2 ](y, C)ξ(C)δ(C, 2 ) 

M[1 ∧ ¬2 , 2 ](y, z)b[2 ](z) = a(y) z∈C

such that the required property is given for t = 1.  Let bC (i) =  z∈C M[1 ∧ ¬2 , 2 ](i, z)b[2 ](z) for i ∈ S . So, the afore  mentioned argumentation ensures that bC (x) = bC (y) if x ∼ y. For the induction step, we assume that the relation has been proved for t ≥ 1 and we show that it holds for t + 1. To simplify the notation, let P = M[1 ∧ ¬2 , 1 ∧ ¬   2 ], Q = M[1 ∧ ¬2 , 2 ], and Rt =   t (M[1 ∧ ¬2 , 1 ∧ ¬2 ])k M[1 ∧ ¬2 , 2 ]. We have to prove k=0 that  



Rt (x, z)b[2 ](z) = a(y) Rt (y, z)b[2 ](z) . a(x) z∈C

z∈C

124

Discrete Event Dyn Syst (2010) 20:103–137

Since a(x) = a(y) for x ∼ y, we only need to show that 

z∈C

Rt (x, z)b[2 ](z) =



z∈C

Rt (y, z)b[2 ](z) .

Starting from the left side, we obtain by the induction assumption, 

z∈C

= = =

Rt (x, z)b[2 ](z)



z∈C



z∈C



z∈C

 Rt−1 (x, z)b[2 ](z) +  Rt−1 (y, z)b[2 ](z) +



 z∈C



z∈C

 Pt Q (x, z)b[2 ](z)

 t  P Q (x, z)b[2 ](z)

  ex Pt bC Rt−1 (y, z)b[2 ](z) +

At this point, we are done if ex Pt = e y Pt . Obviously, x ∼ y implies only P(x, C ) = P(y, C ) for all x, y ∈ C and all C, C ∈ S / ∼. However, we can show by induction that P(x, C ) = P(y, C ) for all x, y ∈ C and all C, C ∈ S / ∼ implies Pk (x, C) = Pk (y, C) for k > 0. Define ψk (C, C ) = Pk (x, C) for some x ∈ C which is independent of the choice of x. By definition, the statement is true for k = 1. So for an inductive argument, we can assume that the result holds for k − 1, then we have for an arbitrary C ∈ S / ∼ and all x, y ∈ C: Pk (x, C ) = = = = = = =



z∈S

P(x, z)Pk−1 (z, C ) 



C ∈S /∼

z∈C





C ∈S /∼



C ∈S /∼

z∈C

C ∈S /∼

z∈C





C ∈S /∼



z∈S

P(x, z)ψk−1 (C , C )

ψ1 (C, C )ψk−1 (C , C ) 



P(x, z)Pk−1 (z, C )

z∈C

P(y, z)ψk−1 (C , C ) P(y, z)Pk−1 (z, C )

P(y, z)Pk−1 (z, C )

= Pk (y, C )

Discrete Event Dyn Syst (2010) 20:103–137

125

So in summary, we obtain 

z∈C

= = =

Rt (x, z)b[2 ](z)







z∈C

  ex Pt bC Rt−1 (y, z)b[2 ](z) +

z∈C

  e y Pt bC Rt−1 (y, z)b[2 ](z) +

z∈C

Rt (y, z)b[2 ](z)

and the induction step is complete. This finishes considerations of t 1 U  p 2 . t For 1 AU  p 2 , we have already proved that x ∼ y implies x |= t t 1 U  p 2 ⇔ y |= 1 U  p 2 . Thus, it remains to prove the second t condition for 1 AU   2 which indicates that on all paths of length t p 1 holds until 2 holds and 2 has to hold in at most t steps. Observe that for the proof we only have to distinguish between zero and nonzero transition weights. x ∼ y implies Ma (x, C)  =  0 ⇔ Ma (y, C)  =  0 and we can prove by induction over the length of the path: x |= 2 ⇔ y |= 2 which implies that for paths of length t = 0 the second condition is identical for bisimilar states, ii) assume that it has been proved for paths of length t − 1 (t > 0) that the second condition holds or does not hold for bisimilar states. We have to prove that the same is true for paths of length t. Obviously x |= 1 ⇔ y |= 1 . Furthermore Ma (x, z)  =  0 for some z where the second condition does hold (not hold) for paths of length t − 1, then there exists some z ∼ z with Ma (y, z )  =  0 and since z ∼ z the second condition holds (does not hold) for paths of length t − 1. By our induction assumption this proves that the second condition of t 1 AU  p 2 holds (does not hold) for x ∼ y and paths of arbitrary length t. i)

t t Finally, to prove 1 U  p 2 and 1 AU  p 2 for general 1 and 2 , we again use induction, namely over the number of occurrences of t t 1 U  p 2 or 1 AU  p 2 in a formula. Note that in the aforementioned argumentation, we did not use any assumption for 1 and 2 other than that x |= 1 ⇔ y |= 1 and x |= 2 ⇔ y |= 2 . Since this assumption holds here again by the induction assumption we can simply repeat the t t argumentation for 1 U  p 2 and 1 AU  p 2 above for the induction step. 5. is easy since we have proved x |=  ⇔ y |=  and x |=  or x |= ¬ has to hold, we also have x |= ¬ ⇔ y |= ¬.  

The above theorem shows that one cannot distinguish between bisimilar states or automata by model checking CTL$ formulas. Thus, an automaton can be first

126

Discrete Event Dyn Syst (2010) 20:103–137

reduced according to bisimulation equivalence to gain efficiency in subsequent model checking algorithms. For this purpose, first relation ∼ is computed, which can be done by a partition refinement algorithm (see e.g., Buchholz 2000 for such an algorithm for stochastic systems), and then each equivalence class of ∼ is substituted by a single state, which yields an aggregated or reduced automaton (Buchholz 2008). Afterwards, formulas are checked with the aggregated instead of the original automaton. In Buchholz and Kemper (2001), it is shown that bisimulation is a congruence with respect to the composition operators of the process algebra GPA, which allows compositional analysis by interleaving reduction of components due to bisimulation equivalence and composition of components. In this way, a reduced automaton is generated to which model checking is applied.

6 Examples of automata with specific semirings The model checking approach presented in this paper is based on the length and weight of paths. Thus, time can only be considered if it is described by counting transitions or transition weights as in RTCTL (Emerson et al. 1992) and in PCTL (Hansson and Jonsson 1994). Other logics such as CSL (Baier et al. 2003), TCTL (Alur et al. 1993) or WCTL (Bouyer 2006) consider a timing model which is not only defined by the length and weight of a path. Thus, CTL$ cannot be directly applied to these models. Nevertheless, it is often possible to extend the approach. E.g., in CSL which is defined over CTMCs, the state at time t is defined as weighted sum of path lengths where the additional weight depends on the length of a paths and the value of t. The extension of the logic and the automata model to more general timing models is beyond the scope of this paper and will be considered in future research. We present six examples in the following subsections. Two of the examples describe known types of automata which are presented in the proposed framework. In these cases we show that CTL$ model checking is related to logics presented specifically for these automata types. Afterwards we present new approaches for model checking. The section ends with a brief summary of the complexity of model checking formulas in different semirings.

6.1 Finite automata Finite automata are defined over the semiring (IB, ∨, ∧, 0, 1). For these automata α(x) = 1 for initial states and α(x) = 0 for the remaining states. Similarly, β(x) = 1 for terminating states and 0 for the remaining states. T(x, a, y) = 1 describes the existence of an a-labeled transition between x and y. The Boolean semiring is ordered (0 < 1), the order is preserved by the operations and 0 is the infimum. Therefore the conditions we proposed for model checking are observed. In the Boolean case all paths have the same weights, namely 1. For finite automata, CTL is a logic which is often used for model checking. We now show how the path formulas of CTL can be expressed by CTL$. State formulas

Discrete Event Dyn Syst (2010) 20:103–137

127

defined via atomic propositions are obviously identical in both cases. Negation is also identical since x |= ¬ ⇔ x  |=  in both logics. CTL EX AX A[1 U 2 ] E[1 U 2 ] AF  EF  AG  EG 

CTL$ [∗]>0 . [∗]>0 . ∧ [∗]=0 .¬ ∞ 1 AU >0 2 ∞ 1 U >0 2 ∞ AF>0  ∞ U F>0  ∞ ¬U F>0 ¬ ∞ ¬AF>0 ¬

For the detailed description of the CTL-formulas see Clarke et al. (1986). It is easy to show that for the Boolean case the model checking algorithms proposed above all t t have a finite runtime because for 1 AU  p 2 and 1 U  p 2 are identical for all t ≥ n. The reason for this behavior is that for an automaton with n states between two states, a path of length ≤ n or no path exists. Additionally, since all paths have the same weights and addition is idempotent, it is sufficient to consider paths up to length n if no longer paths have been defined explicitly via concatenation of [a] in the formulas. Consequently, the following relation holds for the Boolean semiring. 

∞ N[1 ∧ ¬2 , 1 ∧ ¬2 ] = (M[1 ∧ ¬2 , 1 ∧ ¬2 ])k k=0

=



n

k=0

(M[1 ∧ ¬2 , 1 ∧ ¬2 ])k

For the representation of CTL formulas using CTL$, paths of arbitrary length are considered. However, by considering paths of finite length and assuming that each transition of the automaton has a duration of one time unit, real time properties can be proved by CTL$ model checking. In this case CTL$ can be used to mimic formulas of the real time logic RTCTL (Emerson et al. 1992). RTCTL contains all formulas of CTL plus two path formulas which indicate that on a path (all paths) observe that condition 1 holds until 2 holds and this happens to be true within at most t steps. The following table shows the correspondence to CTL$. RTCTL A[1 U ≤t 2 ] E[1 U ≤t 2 ]

CTL$ t 1 AU >0 2 t 1 U >0 2

Example 6.1 We consider the driving test example shown in Fig. 1 over the Boolean semiring. In this case, each arc in the graph describes a transition with weight 1. Since for the Boolean case bisimilar automata cannot be distinguished by CTL$, model checking can be performed using the aggregated automaton shown in Fig. 2. Since L is the only initial state of the automaton, we have to prove whether ∞ a formula holds for L . Formula (true U >0 ok) states that it is possible to pass

128

Discrete Event Dyn Syst (2010) 20:103–137

the driving examination in an arbitrary number of steps. This formula is obviously satisfied by L . The shortest path satisfying the formula starts in L , passes ABC, t and then enters H  . Thus, also, the formula (true U >0 ok) is satisfied by L for all t > 1 which means that the driving examination can be passed in 2 steps. The ∞ formula (true AU >0 ok) states that the examination is always passed. This formula is not satisfied by L because paths of infinite length exist which do not reach H  . t Consequently, formula (true AU >0 ok) also does not hold for L . In the Boolean semiring it is not possible to determine more detailed results about reaching state H  . We can only state that there exists a path that reaches H  and that not all paths reach H  . CTL$ allows us to derive results about the length of the path reaching H  but not about the quantification of paths because the U operator equals EU in the Boolean semiring. This is different in the other semirings which we consider in the subsequent subsections. 6.2 Probabilistic automata Probabilistic automata are defined over the semiring (IR≥0 , +, ·, 0, 1) with the additional restrictions  x∈S α(x) = 1 , 

a∈L



y∈S

T(x, a, y) = 1 for all x ∈ S .

A probability distribution is defined as the initial distribution and the sum of transition probabilities leaving a state is 1. These restrictions define a generative probabilistic model in the sense of van Glabbek et al. (1990) because the automaton decides probabilistically which transition occurs next. Additionally, the automata model is similar to the model presented in Hansson and Jonsson (1994) with the additional possibility of labeling transitions. Probabilistic automata are ordered, the order is preserved by the operations and 0 is the infimum which implies that model checking can be applied for this automata type. For probabilistic automata the logic PCTL has been proposed in Hansson and Jonsson (1994). This logic contains, apart from state propositions and logical combinations of state propositions, the path quantifiers 1 U ≥≤tp 2 and 1 U >≤tp 2 which correspond to 1 U ≥t p 2 and 1 U >t p 2 , respectively, in CTL$. For finite t, the following relation between the path formulas U and AU holds in probabilistic systems. t t 2 ⇔ x |= 1 AU ≥1 2 x |= 1 U ≥1

The relation holds since probability 1 implies that the condition holds on all paths. I.e., there exists no path of length ≤ t that contradicts the condition since otherwise this finite path would have some weight > 0 such that the remaining paths together cannot have weight 1. Interestingly, the above relation does not necessarily hold for t = ∞ as shown in the example below. Now we consider CTL$ model checking for probabilistic automata. Of particular ∞ interest are formulas of the type 1 U  p 2 . For the remaining cases, the algorithms presented in Section 4 can be used because they require in these cases a finite number of steps. For the formulas with t = ∞, matrix N[1 ∧ ¬2 , 1 ∧ ¬2 ] has to be computed first which can be done with the general algorithm from Section 4. For

Discrete Event Dyn Syst (2010) 20:103–137

129

probabilistic automata, the matrix has an alternative representation that results from an inverse matrix as shown in the following theorem. ∞ Theorem 6.1 State x ∈ S satisfies formula 1 U  p 2 if M[1 ∧ ¬2 , 1 ∧ ¬2 ] is a substochastic matrix where rows and columns cannot be reordered by a symmetric permutation such that a stochastic submatrix appears along the diagonal3 and ∞   k (M[1 ∧ ¬2 , 1 ∧ ¬2 ]) M[1 ∧ ¬2 , 2 ]b[2 ] a(x)ex k=0

= a(x)ex (I − M[1 ∧ ¬2 , 1 ∧ ¬2 ])−1 M[1 ∧ ¬2 , 2 ]b[2 ]  p Proof The matrix representation of the formula has already been introduced. The relation ∞ 

(M[1 ∧ ¬2 , 1 ∧ ¬2 ])k = (I − M[1 ∧ ¬2 , 1 ∧ ¬2 ])−1

k=0

is well known for absorbing Markov chains (Kemeny and Snell 1976). If M[1 ∧ ¬2 , 1 ∧ ¬2 ] contains no stochastic submatrix, then the spectral radius of the matrix is less than 1 and the infinite matrix sum converges. Thus, it is easy to show that  ∞  k (I − M[1 ∧ ¬2 , 1 ∧ ¬2 ]) (M[1 ∧ ¬2 , 1 ∧ ¬2 ]) = I . k=0

The existence of the inverse matrix for substochastic matrices without traps has been proved in (Lal and Bhat 1987, Lemma 3.2, 3.3).   ∞ The theorem contains a method to decide for which states 1 U  p 2 holds. The inverse matrix used in the theorem contains in position (x, y) the average number of visits in state y starting in state x before a state is reached where 1 ∧ ¬2 is false. Multiplication with the row vector from the left and the column vector of the final weights from the right gives the required weight. If M[1 ∧ ¬2 , 1 ∧ ¬2 ] contains a stochastic submatrix, then there exists a subset of states where 1 but not 2 holds and this subset of states forms a trap with respect to the formula, i.e., the ∞ automaton can never leave the subset after entering it. Obviously 1 U  p 2 cannot be satisfied in these states and each path entering the subset does not count when path weights are summed. Thus, for subsets of states forming a stochastic submatrix, the rows in M[1 ∧ ¬2 , 1 ∧ ¬2 ] might be set to 0 to compute the result. After ∞ this modification the inverse matrix exists and the set of states satisfying 1 U  p 2 can be computed in a finite number of steps.

Example 6.2 For the probabilistic case, we consider the driving test example with probabilities given in Example 5.1, where also a bisimilar automaton with fewer states is presented. We can check the smaller aggregated automaton and consider

3 This

is sometimes denoted as a substochastic matrix without traps.

130

Discrete Event Dyn Syst (2010) 20:103–137

the formula (true U ≥∞p ok) which is true if the test is passed with probability of at least p in an arbitrary number of steps. State L satisfies the formula if a

∞ 

(M[¬ok, ¬ok])k · M[¬ok, ok] · (b[ok]) ≥ p

k=0

holds. Using the ordering of states (L , ABC, DEF, G , H  ) as given in 5.2 we obtain the following matrices and vectors. a = (1, 0, 0, 0, 0) , b[ok] = (0, 0, 0, 0, 1)T ⎛

1/2 ⎜ 0 ⎜ M[¬ok, ¬ok] = ⎜ ⎜ 0 ⎝ 1 0

1/2 1/3 0 0 0

0 1/3 1/2 0 0

0 0 1/2 0 0 ⎛

⎞ ⎛ 0 0 ⎜0 0⎟ ⎟ ⎜ ⎜ 0⎟ ⎟ , M[¬ok, ok] = ⎜ 0 ⎝0 0⎠ 0 0

4 ⎜2 ⎜ (I − M[¬ok, ¬ok])−1 M[¬ok, ok] = ⎜ ⎜4 ⎝4 0

3 3 3 3 0

2 2 4 2 0

1 1 2 2 0

0 0 0 0 0

0 0 0 0 0

0 0 0 0 0

⎞ ⎛ 0 0 ⎜0 0⎟ ⎟ ⎜ ⎜ 0⎟ ⎟ · M[¬ok, ok] = ⎜ 0 ⎠ ⎝0 0 0 1

⎞ 0 1/3 ⎟ ⎟ 0 ⎟ ⎟ 0 ⎠ 0 0 0 0 0 0

0 0 0 0 0

0 0 0 0 0

⎞ 1 1⎟ ⎟ 1⎟ ⎟ 1⎠ 0

and a (I − M[¬ok, ¬ok])−1 M[¬ok, ok] (b[ok]) = 1 which implies that the formula is observed for all p ≤ 1. This means that after an infinite number of steps the driving test will be passed with probability 1. Thus, L |= true U >∞p ok for all p ∈ [0, 1) but L  |= true AU >∞p ok for all p. This example nicely shows that probability 1 does not mean that the result holds for all paths. This result is, of course, well known from probability theory. 6.3 Max/plus automata Max/plus automata are defined over the completed semiring (IR≥0 ∪ {−∞, ∞},  − ∞ = max(a, −∞) = a and a max, +, −∞, 0) with the computation a + · 0=a+ 0 = a. The weights of a path in max/plus correspond to the sum of weights of each transition on the path because multiplication is represented by the usual addition. If we consider several paths, then the maximum operator computes the weights of the path with the highest weights. Max/plus automata can be applied for various analysis purposes including the analysis of real time systems or communications networks and have become very popular in the recent years. The max/plus semiring is ordered with respect to the usual ordering a ≤ b ⇔ max(a, b ) = b . Furthermore, the order is preserved by the operations and  0, in this case −∞, is the infimum of the semiring. In the definition of the transition function T, −∞ is used to denote that an arc does not exist, which is the common usage of element  0. We can directly apply our model checking approach.

Discrete Event Dyn Syst (2010) 20:103–137

131

The analysis of max/plus and also min/plus automata is presented in detail in Gaubert (1995). The model class used there is identical to our weighted automata over the same semirings. However, Gaubert (1995) presents the analysis but does not consider a logic to specify properties and it also does not consider the relation to bisimulation. In some sense the relation between this paper and Gaubert (1995) is like the relation between the analysis of Markov chains (Stewart 1994) and the use of model checking approaches for Markov models (Baier et al. 2003; Hansson and Jonsson 1994). Both approaches are commonly considered as being different. For the computation of N[1 ∧ ¬2 , 1 ∧ ¬2 ], the algorithm we presented above can be used since a∗ = ∞ for all a > −∞ in the max/+ semiring. Example 6.3 For this semiring, we need a different selection of T(x, a, y) to achieve bisimilar automata in Figs. 1 and 2, since the maximal values of outgoing arcs of bisimilar states leading to the same class of states need to be equal. We select the following values which may be interpreted as distances the student has to drive or a quantification of the amount of stress he/she has to suffer. Matrix elements that are  0 and transition labels are omitted for clarity.

For instance, A ∼ ABC since T(A, d, B) = 3 = T(ABC, d, ABC), max(T(A, e, D), T(A, e, E)) = 9 = T(ABC, e, DEF), and T(A, f, H) = 3 = T(ABC, f, H  ) and further conditions of Definition 5.1 with respect to α, β and AP hold as well. In this semiring, CTL$ considers the most costly (or stressful) ways to a driver’s li9 cense. E.g., one can compute by the algorithm given in Section 4 that L |= trueU ≥21 ok holds due to path π through states L, A, E, G, L, A, B, H with ce(π ) = 21. For model checking we can use the bisimilar automaton given above, which contains 9 fewer states and fewer arcs. So we check L |= trueU ≥21 ok which holds due to path π  through states L , ABC, EFG, G , L , ABC, ABC, H. Both paths are of the same length and have the same weights.

132

Discrete Event Dyn Syst (2010) 20:103–137

6.4 Min/plus automata The min/plus approach is very similar to the max/plus approach. It is applied if one is interested in minimal weights instead of maximal weights. It is defined on the semiring (IR≥0 ∪ {∞}, min, +, ∞, 0) with an inverse order, i.e. addition becomes  y = min(x, y), multiplication becomes addition x minimum x + · y = x + y, and x, y are ordered x ≥ y iff x = min(x, y). The semiring preserves the order and  0 = ∞ is the infimum. Working with an inverse order is formally correct but rather contrary to intuition. Note that the inverse order of min/plus is the reason to use the notion of infimum and supremum rather than minimum and maximum in this paper. This avoids reformulation of the algorithms. Model checking algorithms can be applied analogously as for max/plus automata. Computation of the matrix N[1 ∧ ¬2 , 1 ∧ ¬2 ] is easier for min/plus than for max/plus. The reason is that minimal weights count. Since a cycle cannot reduce the weight of a path, we have, as in the Boolean semiring N[1 ∧ ¬2 , 1 ∧ ¬2 ] = =



∞ k=0



n

k=0

(M[1 ∧ ¬2 , 1 ∧ ¬2 ])k (M[1 ∧ ¬2 , 1 ∧ ¬2 ])k .

This identity can also be exploited if finite sums with t > n have to be computed. 6.5 Max/min automata The semiring (IR≥0 ∪ {∞}, max, min, 0, ∞) is useful to identify paths with respect to bottlenecks, since the weight of a path gives the minimum value observed through all of its arcs. We consider a communication network as an example. A weighted automaton models the network by using nodes for hubs and arcs for links between hubs. Each hub shows a certain utilization and each link has a bandwidth as a nonnegative real number assigned to it. If there is no link between two nodes, we assume an arc with weight 0. In order to establish a point-to-point communication, we are interested in the existence of a connection between two nodes xstart and xend that has a minimum bandwidth μ, uses less than λ intermediate nodes and the employed nodes should have a utilization less than γ to avoid saturated or overloaded nodes. Utilization < γ is defined as an atomic proposition of the nodes. To express this in CTL$, we first define atomic propositions 1 and 2 as follows. A node x |= 1 if and only if its utilization is less than γ . A node x |= 2 if and only if it is node xend . The following formula describes the property we are interested in  = 1 U ≥t p 2 with p = μ, t = λ. Model checking the automata using the algorithm t for 1 U  p 2 given in Section 4 provides us with information whether xstarts |=  or not. Note that the semiring is ordered, the operations preserve the order and  0 = 0 is the infimum. Computation of the matrix N[1 ∧ ¬2 , 1 ∧ ¬2 ] is easy in the max/min semiring because the weight of a path is determined by minimum weight of an arc on this path such that cycles cannot increase the weight of a path and N[1 ∧ ¬2 , 1 ∧ ¬2 ] can be computed by finite summation as for the Boolean semiring or the min/plus semiring.

Discrete Event Dyn Syst (2010) 20:103–137

133

6.6 The expectation semiring In this subsection, we consider a semiring which is more complex than the previous and outline how our model checking approach can be extended to analyze this system as well. The proposed semiring has been defined in Eisner (2001) and is used in combination with the expectation maximization algorithm to learn finite grammars (Eisner 2002). A value in the expectation semiring consists of two components ( p, v) with p ∈ [0, 1] and v ∈ IR≥0 . The operations are defined as  ( p2 , v2 ) = ( p1 + p2 , v1 +v2 ) ( p1 , v1 ) · ( p2 , v2 ) = ( p1 · p2 , p1 · v2 +v1 · p2 ) and ( p1 , v1 ) + We have  0 = (0, 0) and  1 = (1, 0). Furthermore, we define the ordering ≥ with ( p1 , v1 ) ≥ ( p2 , v2 ) if p1 ≥ p2 and v1 ≥ v2 . Observe that this defines only a partial order since elements exist where neither ( p1 , v1 ) ≥ ( p2 , v2 ) nor ( p1 , v1 ) ≤ ( p2 , v2 ) holds. The semiring is commutative because multiplication is commutative, it is not idempotent, but  0 is the infimum and the order is preserved. For a given formula  let P be a matrix containing in position (x, y) the first component of the weight between states x and y if x |=  ∧ y |= , otherwise it contains a 0. Let V be a matrix containing in position (x, y) the second component of the weight between states x and y if x |=  ∧ y |= , otherwise it contains a 0. P[k] and V[k] are matrices containing the values for paths of length k. E.g., matrix (M[, ])k (x, y) = (P[k](x, y), V[k](x, y)) if P and V are chosen as follows: The values in P[k] are computed independently of the values in V such that P[k] = Pk . The elements in V[k] are computed as V[k](x, y) =

n−1 

P[k − 1](x, z)V(z, y) +

z=0

n−1 

V[k − 1](x, z)P(z, y) .

z=0

This yields the following recursion at matrix level. V[k] = Pk−1 V + V[k − 1]P = Pk−1 V + Pk−2 VP + V[k − 2]P2 =

k−1 

Pl VPk−l−1

l=0

This implies for the infinite case that limk→∞ V[k] = 0 if limk→∞ Pk = 0 and ∞  ∞    

∞ k V[k] = P V Pl k=0

k=0

l=0

This computation depends on the computation of the infinite sum of matrix powers of P. If matrix P is a substochastic matrix without traps, then the results for the probabilistic case apply and the sum can be computed as (I − P)−1 . 6.7 Complexity of model checking We briefly consider the complexity of model checking. Obviously, the complexity is linear in the length of a formula. Atomic propositions are checked in constant time and [a] p . requires a computational effort proportional to the number of non-zero elements in one row of Ma , if the formula is checked for one state and it equals the number of non-zero elements in Ma if it is checked for all states. Model

134

Discrete Event Dyn Syst (2010) 20:103–137

t t checking 1 AU  p 2 has the same complexity as model checking 1 U  p 2 . t Thus, the complexity of checking 1 U  p 2 is the major aspect. The following t ∞ table includes the complexity of model checking 1 U  p 2 and 1 U  p 2 for the presented semirings and for the general case. nz is the number of non-zero elements t in the matrix M[1 ∧ ¬2 , 1 ∧ ¬2 ] which is required for checking 1 U  p 2 . Furthermore mm is the computational effort to multiply two matrices of order n.

Semiring Boolean Probabilistic Max/plus Min/plus Min/max Expectation General

t 1 U  p 2 O(min(t, n) · nz) O(t · nz) O(min(log t · mm, t · nz) O(min(t, n) · nz) O(min(t, n) · nz) O(t · nz) O(t · nz)

∞ 1 U  p 2 O(n · nz) O(n3 ) O(n3 ) O(n · nz) O(n · nz) O(n3 ) O(n3 )

t ∞ The computation of the set of states fulfilling formula 1 U  p 2 and 1 U  p 2 is done with the algorithms presented in Section 4. Without any further assumptions t about the semiring, model checking of 1 U  p 2 requires t vector matrix multiplications with matrix M[1 ∧ ¬2 , 1 ∧ ¬2 ] such that the computational complexity is in O(t · nz). The algorithm to compute matrix N[1 ∧ ¬2 , 1 ∧ ¬2 ] which is ∞ 3 necessary to check 1 U  p 2 requires a computational effort in O(n ). After N[1 ∧ ¬2 , 1 ∧ ¬2 ] is available, only an additional vector matrix product has ∞ 3 to be computed such that the effort to check 1 U  p 2 is in O(n ). For the Boolean semiring and the semirings min/+ and min/max we have already t n shown that 1 U  p 2 = 1 U  p 2 such that at most n vector matrix products t ∞ need to be computed to obtain the set of states fulfilling 1 U  p 2 or 1 U  p 2 . Consequently, the computational effort is in O(min(t, n) · nz). For the semiring t max/+, the case 1 U  p 2 for finite t can be either checked by repeated squaring of the matrix since the semiring is idempotent or by t vector matrix products. This requires an effort which is either in O(log t · mm) or in O(t · nz). For the remaining cases, the standard algorithms apply without any modifications. ∞ Observe, however, that 1 U  p 2 can only be checked if the semiring is closed such that the weights of infinite paths are well defined. It is interesting to note that for ∞ many semirings the computation of 1 U  p 2 is less complex than the computation t of 1 U  p 2 for a large t.

7 Conclusions We present a general approach for model checking weighted automata which covers classical types of automata such as untimed or probabilistic automata as well as new types such as max/plus and min/plus automata. The key idea is that transitions weights can be taken from a semiring which is an algebraic structure of very modest requirements. We present a modal logic CTL$ for this class of models that is built on top of CTL and allows one to specify paths with respect to their length and weights. This yields a generic approach where different semirings automatically profit from algorithms and results derived for the general case, e.g., we present a bisimulation

Discrete Event Dyn Syst (2010) 20:103–137

135

for CTL$ that is subsequently used to check an example under various weight assignments of different semirings. So far we presented analysis algorithms based on graphs assuming an explicit representation of states. This was for clarity and to limit the scope of the paper. Clearly, large state spaces are better treated by a symbolic representation. In the special case of the boolean semiring, binary decision diagrams (BDDs) and corresponding algorithms (Clarke et al. 1999; Fujita et al. 1997) are sufficient. However the general case requires the treatment of numerical values, such that corresponding extensions of BDDs are more appropriate, for instance multiterminal BDDs (Fujita et al. 1997). Furthermore, compositional representations as in Buchholz and Kemper (2001) and compositional model checking are interesting candidates for model checking CTL$. The advantages of the approach will facilitate the construction of analysis tools and the application of model checking in different areas such as realtime scheduling and performance analysis.

References Aho A, Hopcraft J, Ullman J (1974) The design and analysis of computer algorithms. AddisonWesley, Massachusetts Alur R, Courcoubetis C, Dill D (1993) Model-checking in dense real-time. Inf Comput 104:2–34 Alur R, Dill DL (1994) A theory of timed automata. Theor Comp Sci 126:183–235 Baccelli F, Cohen, G, Olsder, G, Quadrat J (1992) Synchronization and linearity. Wiley, New York Baccelli F, Gaujal, B, Simon, D (1999) Analysis of preemptive periodic real time systems using the (max,plus) algebra. Research Report 3778, INRIA Baccelli F, Hong, D (2000) TCP is (max/+) linear. In: Proc SIGCOM 2000, ACM Baier C, Haverkort B, Hermanns H, Katoen JP (2003) Model checking algorithms for continuous time markov chains. IEEE Trans Softw Eng 29(7):524–541 Baier C, Cloth L, Kuntz M, Siegle M (2007) Model checking markov chains with actions and state labels. IEEE Trans Softw Eng 33(4):209–224 Beauquier D, Slissenko A (1998) Polytime model checking for timed probabilistic computation tree logic. Acta Inform 35:645–664 Berard M et al (2001) Systems and software verification. Springer, Berlin Bouyer P (2006) Weighted timed automata: Model checking and games. ENTCS 158:3–17 Brihaye T, Bruyère V, Raskin JF (2004) Model-checking for weighted timed automata. In: Lakhnech Y, Yovine S (eds) Proc FORMATS/FTRTFT, LNCS, vol 3254. Springer, Berlin pp 277–292 Bryans J, Bowman H, Derrick J (2003) Model checking stochastic automata. ACM Trans Comput Log 4(4):452–492 Buchholz P (1994) Markovian process algebra: composition and equivalence. In: Herzog U, Rettelbach M (eds) Proc 2nd work on process algebras and performance modelling. Arbeitsberichte, des IMMD, University of Erlangen, no. 27, pp 11–30 Buchholz P (2000) Efficient computation of equivalent and reduced representations for stochastic automata. Int J Comput Syst Sci Eng 15(2):93–103 Buchholz P (2008) Bisimulation relations for weighted automata. Theor Comp Sci 393(1–3):109–123 Buchholz P, Kemper P (2001) Quantifying the dynamic behavior of process algebras. In: de Alfaro L, Gilmore S (eds) Proc. process algebras and probabilistic methods, LNCS 2165. Springer, Berlin, pp 184–199 Buchholz P, Kemper P (2003a) Model checking for a class of weighted automata. Technical Report 779, TU Dortmund, Fachbereich Informatik Buchholz P, Kemper P (2003b) Weak bisimulation for (max/+) automata and related models. J Autom Lang Comb 8(2):187–218 Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142–170 Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263

136

Discrete Event Dyn Syst (2010) 20:103–137

Clarke EM, Wing JM et al (1996) Formal methods: state of the art and future directions. ACM Comput Surv 28(4):626–643 Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT, Massachusetts Clarke EM, Kurshan R (1996) Computer-aided verification. IEEE Spectrum 33(6):61–67 Dasgupta P, Chakrabarti PP, Deka JK, Sankaranarayanan S (2001) Min–max computation tree logic. Artif Intell 127(1):137–162 Donatelli S, Haddad S, Sproston J (2007) CSLT A : an expressive logic for continuous time markov chains. In: Proc QEST 2007, IEEE Dragan M (2007) Model checking für gewichtete automaten. Master’s thesis, TU Dortmund, Fakultät für Informatik (in German) Eilenberg S (1974) Automata, languages and machines part A. Pure and applied matematics : a series of monographs and textbook, vol 58. Academic, New York Eisner J (2001) Expectation semirings: flexible EM for learning finite-state transducers. In: Proc ESSLLI workshop on finite-state methods in NLP Eisner J (2002) Parameter estimation for probabilistic finite-state transducers. In: Proc 40th annual meeting of the association for computational linguistics (ACL), Philadelphia, July pp 1–8 Emerson EA, Mok A, Sistla AP, Srinivasan J (1992) Quantitative temporal reasoning. Real-time Systems, 4:331–352, Kluwer Fletcher JG (1980) A more general algorithm for computing closed semiring costs between vertices of a directed graph. Commun ACM 23(6):350–351 Fujita M, McGeer PC, Chih-Yuan Yang J (1997) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form Methods Syst Des 10(2/3):149–169 Gaubert S (1995) Performance evaluation of (max/+) automata. IEEE Trans Automat Contr 40(12):2014–2025 Golan JS (1999) Semirings and their applications. Wiley, New York Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6:512–535 Hennessy MC, Milner R (1985) Algebraic laws for non-determinism and concurrency. J ACM 32:137–161 Hillston J (1994) A compositional approach for performance modelling. PhD thesis, University of Edinburgh, Dep of Comp Sc Jiang Z, Litow B, de Vel O (2000) Similarity enrichment in image compression through weighted finite automata. In: Du DZ, et al (eds) Proc COCOON 00, LNCS 1858. Springer, pp 447–456 Kemeny JG, Snell JL (1976) Finite markov chains. Springer, Berlin Kuich W, Salomaa A (1986) Semirings, automata, languages. In: ETACS monographs on theoretical computer science, Springer, Berlin Lal R, Bhat UN (1987) Reduced systems in Markov chains and their application to queueing theory. Queueing Syst 2:147–172 Larsen K, Skou A (1991) Bisimulation through probabilistic testing. Inf Comput 94:1–28 Milner R (1989) Communication and concurrency. Prentice Hall, New Jersey Mohri M (2002) emiring frameworks and algorithms for shortest-distance problems. J Autom Lang Comb 7(3):321–350 Mohri M, Pereira F, Riley M (1996) Weighted automata in text and speech processing. In: Kornai A (ed) Proc ECAI 96 Park D (1981) Concurrency and automata on infinite sequences. In: Proc 5th GI conference on theoretical computer science, LNCS 104. Springer, Berlin, pp 167–183 Stewart WJ (1994) Introduction to the numerical solution of Markov chains. Princeton University Press, Princeton van Glabbek R, Smolka S, Steffen B, Tofts C (1990) Reactive, generative and stratified models for probabilistic processes. In: Proc LICS’90, pp 130–141

Discrete Event Dyn Syst (2010) 20:103–137

137

Peter Buchholz received the Diploma degree (1987), the Doctoral degree (1991) and the Habilitation degree (1996) all from the TU Dortmund, where he is currently a professor for modeling and simulation. His current research interests are efficient techniques for the analysis of stochastic models, formal methods for the analysis of discrete event systems, the development of modeling tools, as well as performance and dependability analysis of computer and communication systems.

Peter Kemper is an associative professor at the department of computer science of the college of William and Mary. He holds a diploma degree in computer science (Dipl.-Inform., 1992) and a doctoral degree (Dr.rer.nat, 1996), both from TU Dortmund, Germany. His main interests are in the quantitative evaluation of systems and formal aspects of software engineering. In addition to developing modelling techniques and tools for performance and dependability assessment of computer and communication systems, he also works on model-based evaluation of manufacturing systems, logistic networks and biological systems. He has contributed to several tools for functional and quantitative analysis of discrete event systems, including the QPN tool, the APNN toolbox, and the ProC/B toolset.