key: cord-0043268-xus3wo5m
authors: Donatelli, Susanna; Haddad, Serge
title: Expressiveness and Conciseness of Timed Automata for the Verification of Stochastic Models
date: 2020-01-07
journal: Language and Automata Theory and Applications
DOI: 10.1007/978-3-030-40608-0_11
sha: 1c3656c81c6750d6cddec5715f0ccba5361d66c6
doc_id: 43268
cord_uid: xus3wo5m

Timed Automata are a well-known formalism for specifying timed behaviours. In this paper we are concerned with Timed Automata for the specification of timed behaviour of Continuous Time Markov Chains (CTMC), as used in the stochastic temporal logic CSL[Formula: see text]. A timed path formula of CSL[Formula: see text] is specified by a Deterministic Timed Automaton (DTA) that features two kinds of transitions: synchronizing transitions (triggered by CTMC transitions) and autonomous transitions (triggered when a clock reaches a given threshold). Other definitions of CSL[Formula: see text] are based on DTAs that do not include autonomous transitions. This raises the natural question: do autonomous transitions enhance expressiveness and/or conciseness of DTAs? We prove that this is the case and we provide a syntactical characterization of DTAs for which autonomous transitions do not add expressive power, but allow one to define exponentially more concise DTAs.

Stochastic logics like CSL [5] allow one to express assertions about the probability of timed executions of Continuous Time Markov Chains (CTMC). In CSL, model executions (typically called "paths") are specified by two operators: timed neXt and timed Until. CSL has been extended in several ways to include action names (name of the events in the paths) and path properties specified using regular expressions leading to asCSL [6] , or rewards, leading to CSRL [7] . Note that asCSL can specify rather complex path behaviour, expressed by regular expressions, but the timing requirements cannot be mixed within these expressions. GCSRL [14] is an extension of CSRL for model checking of CTMC generated by Generalized Stochastic Petri nets (GSPN) [1] taking into account both stochastic and immediate events.

Automata with time constraints have been used to specify path-based performance indices [16] for Stochastic Activity Networks [15] , while hybrid automata have been used to define rather complex forms of passage of time [2] for GSPN, as well as generic performance properties [9] that are estimated using simulation. The use of a Deterministic Timed Automaton (DTA) in the stochastic logic CSL TA [12] allows to specify paths in terms of state propositions and action names associated to CTMC states and transitions (respectively) and in terms of the timed behaviour of portions of the paths. The CTMC actions are the input symbols for the DTA, and two types of transitions are distinguished: synchronizing transitions that read the input symbols of the CTMC, and autonomous transitions, that are taken by the DTA when the clock reaches some threshold, with priority over synchronizing ones. The determinism requirement ensures that the synchronized product of the DTA and the CTMC is still a stochastic process as all sources of non-determinism are eliminated. CSL TA strictly includes [12] CSL and asCSL. Various extensions of CSL TA have been presented in the literature. DTA with multiple clocks have been used for defining an extension of CSL TA [10, 13] but autonomous transitions are not allowed. In this paper we concentrate on single-clock CSL TA with autonomous transitions, as in the original definition of CSL TA . Indeed the single-clock limitation is a necessary requirement to reduce the CSL TA model-checking problem to the (steady-state) solution of a Markov Regenerative Process, which is the largest class of stochastic processes for which we can compute an exact numerical solution, supported by efficient solution tools [3, 4] . The single-clock setting allows also to investigate whether the definition of CSL TA in [10, 13] , once limited to a single clock, is equivalent to the original definition of CSL TA (introduced in [12] ). Paper Contributions. This paper addresses two research questions. The first one (Sect. 3) is whether the presence of autonomous transitions enhances the expressiveness of DTAs both in terms of timed languages (qualitative comparison) and in terms of probability of accepting the random path of a CTMC (quantitative comparison). We establish that autonomous transitions do enhance expressiveness. Given that eliminating autonomous transitions from a DTA is not always feasible, the second question (Sect. 4) is which are the uses of autonomous transitions that can be emulated by DTA w/o autonomous transitions. We have identified a hierarchy of subclasses of DTA in which the presence of autonomous transitions does not extend expressiveness (and autonomous transitions can therefore be eliminated), but that exponentially improves the DTA size. Only the most interesting proofs and properties have been included in this paper. Missing proofs and the full set of properties can be found in [11] .

Although our motivations rely on the acceptance of paths of CTMCs featuring atomic propositions that label states and actions that label transitions, we set our work in the general context of acceptance of timed paths, where the i`1-th state of a timed path is identified by v i (we count indices from 0), the boolean evaluation of the atomic propositions in that state. δ i indicates a delay, or a sojourn time in state i, and τ i indicates the time elapsed until exiting state i. A timed path leaves state v i with action a i after a sojourn time in the state equal to δ i . The elapsed time can be computed as: τ i " δ i`τi−1 , with τ −1 " 0.

Example 1 (Timed Path). In writing timed paths we indicate functions v i as the set of elements in AP that evaluate to J. Given AP " {p, q} and Act "

is interpreted as the system staying in a state that satisfies p^q in the time interval [0, 0.5[, at time 0.5 action a takes place and the system moves to a state that satisfies ¬p^q, stays there for 1.3 time units and then action b takes place (at the global time τ " 1.8).

DTA definition includes a clock x and two types of constraints: boundary ones, BoundC = {x " α, α P N} and inner ones, InC = {α x β}, with , P {ă, , }, α P N, and β P N Y {8}. In the sequel, C is the largest time constant occurring in a DTA. Before formally defining the syntax and semantic of a DTA (Definitions 2, 3 and 4), let us introduce its main ingredients. During the execution of a stochastic discrete event system (e.g. a Markov chain) that can be represented by a timed path, one manages (1) an index i of the timed path (2) a location, say , is matched with the current state of the path indexed by i, and (3) a delay δ δ i until the next state change from i to i`1. The function Λ mapping the set of locations to the set of boolean expressions over atomic propositions, B AP , restricts the possible matchings since the valuation v i must satisfy the formula Λ( ). This matching evolves in three ways depending on the delay δ, elapsed until the next transition (v i , δ i ) ai − → (v i`1 , δ i`1 ) of the path.

-Either after some delay δ δ, there is an outgoing autonomous transition from whose boundary condition (say x " α) is satisfied and such that v i fulfills Λ( ) where is the target location of the transition. Then is matched with i, delay δ becomes δ − δ , the clock x is increased by δ and the index i is unchanged. -Else if there is a synchronizing transition outgoing from such that (1) after time δ has elapsed its inner condition (say α x β) is satisfied, (2) the action a i belongs to the subset of actions associated with the synchronizing transition, and (3) v i`1 satisfies Λ( ) where is the target location of the transition. Then is matched with i`1, the new delay δ is set to δ i`1 , the clock x is either increased by δ or reset depending on the transition, and the index becomes i`1. -Otherwise there is no possible matching and the timed path is rejected by the DTA.

In the first two cases above, when " f , the final location, the timed path is accepted by the DTA whatever its future. This is ensured due to Λ( f ) " J and the existence of the unique (looping) synchronizing transition from f with no timing and action conditions. Observe that the synchronization may last forever without visiting f : in this case the timed path is rejected.

Furthermore the synchronization of the stochastic system with the DTA should not introduce non determinism. So (1) the formulas associated with the initial locations are mutually exclusive, (2) synchronizing transitions outgoing from the same location are never simultaneously enabled, (3) autonomous transitions outgoing from the same location are never simultaneously enabled, and (4) autonomous transitions have priority over synchronizing transitions.

A single-clock Deterministic Timed Automaton with autonomous transitions is defined by a tuple A " L, Λ, L 0 , f , AP , Synch, Aut where L is a finite set of locations, L 0 Ď L is the set of initial locations, f P L is the final location, Λ : L → B AP is a function that assigns to each location a boolean expression over the set of propositions AP , Synch Ď LˆInCˆ2 Actˆ ∅, ↓ ˆL is the set of synchronizing transitions, and Aut Ď LˆBoundCˆ7ˆ ∅, ↓ ˆL is

Given a clock constraint γ and a clock valuationx,x |" γ denotes the satisfaction of γ byx. Similarly given a boolean formula ϕ and a valuation of atomic propositions v, v |" ϕ denotes the satisfaction of ϕ by v. Example 2 (DTA). Figure 1 , left, shows a DTA with five locations: 0 , 1 , 2 , 3 and f . There is a single initial location, 0 . Autonomous transitions are depicted as dotted arcs, while synchronizing are depicted as solid arcs. For readability we omit: (1) the symbol 7 on autonomous transitions; (2) the set r when there is no reset; (3) Act if a transition accepts all actions; (4) trivially true guards (like x 0) and boolean conditions; (5) the name x of the clock in x " α guards.

As a result an autonomous transition is depicted as either l α,↓ − − → l , as between 1 and 0 , or as l α − → l , as between 0 and 2 . We informally write "a transition with reset" or "a transition without reset" to indicate the condition r " ↓ and r " ∅ respectively. The arc from 0 to 1 represents a synchronizing transition with a clock reset. The arc from 0 to 2 represents an autonomous transition to be taken when the clock is equal to 1, with no clock reset. Boolean expression of locations are: p, associated with 0 , 1 , 2 and (¬p^q), associated with 3 .

Let us describe a possible run of this DTA. At time 0.5, it goes from 0 to 1 by performing action a and resets x. Then at time 1.5, it autonomously comes back to location 0 and clock x is again reset. Then it autonomously goes to 2 at time 2.5 and later to f at time 3.5. While irrelevant, x has current value 2.

To enforce priority of autonomous transitions,

A run is therefore a path in the DTA where the visited locations are coupled with a valuation of propositions, a clock value and a delay in a consistent way w.r.t. the DTA.

Given that v is described in terms of the subset of AP that evaluate to J, a run for the DTA of Fig. 1 , left, is: 0

A timed path σ is recognized by a run ρ of A such that the occurrences of the actions in σ are matched by the synchronizing transitions in ρ. This requires to define a mapping to match the points in the paths in which synchronizing transitions take place. This can be done by identifying a strictly increasing mapping for the indices of the timed path σ to the subset of the indices of the run ρ that correspond to a synchronizing transition. Note that, due to determinism, if such a run exists, it is unique.

σ " (v 0 , δ 0 ) a0 − → (v 1 , δ 1 ) a1 − → · · · (v i , δ i ) ai − → · · · be a timed path and ρ " ( 0 , v 0 ,x 0 , δ 0 ) γ0,B0,r0 −−−−−→ · · · ( i , v i ,x i , δ i ) γi,Bi,ri − −−−− → · · · be a run of a DTA A. Then σ is recognized by ρ if there is a strictly increasing mapping κ : N → N (extended to κ(−1) " −1), such that for all i P N -a i P B κ(i) and δ i " κ(i−1)ăh κ(i) δ h -∀h, κ(i − 1) ă h κ(i) ⇒ v h " v i and h P κ(N) ⇒ B h " 7 A timed path σ is accepted by A if σ is recognized by a run ρ and ρ visits f . The language L(A) of A is the set of the timed paths σ accepted by A.

:(p, δ) · · · is recognized by the run of Example 3 with mapping κ:

The run visits f and the path is accepted.

We consider timed paths generated by a CTMC with state properties and actions. We assume that each state has at least one successor: for all s P S, exists a P Act, s P S such that R(s, a, s ) > 0. CTMC executions lead to timed paths, and a CTMC is a generator of a random path. We define by Pr M (A) the probability that the random path of M is accepted by A (probability measure of all paths accepted by A as in [8] ).

M " S, s 0 , Act , AP , lab, R , where S is a finite set of states, s 0 P S the initial state,

We indicate with A the whole family of automata of Definition 2 and with A na the subclass of automata with no autonomous transitions: A na " {A P A | Aut(A) " ∅} The comparison of the expressive power of A and A na is both qualitative (based on the timed path language) and quantitative (based on accepting probabilities). As usual, we derive other relations between such families. A 1 and A 2 are equally expressive w.r.t. language (resp. Markov chains), denoted

Observe that by definition Observe the difference between sc i , defined at the syntactical level, which maps a location to its i th successor and sc, defined at the semantical level, which maps a pair consisting in a location and a clock valuation to the new clock valuation obtained by firing the single transition enabled w.r.t. the clock valuation.

We also define the region (multi-)graph G A " (V, E) of such a DTA A as follows.

-V , the set of vertices, is defined by V " {( , i) | P L^0 i C`1}; -Let ( , i) be a vertex, then for all j s.t. max(i, 1) j C`1, there is a transition from ( , i) to (sc j ( ), j ) labelled by j with j " 0 if r j "↓ and j " j otherwise. 

The above formula represents the probability of acceptance when the Markov chain starts in s and the DTA starts in with clock valuation t, with i − 1 t i C, therefore within the region (l, i). This probability is computed in terms of the probability of having the next CTMC transition within the region (l, i) itself, or any later region (l, j), multiplied by the probability of acceptance from the state reached by accepting the CTMC transition.

Proof. Define p n (s, , t) as the probability that the run associated with a random timed path of M starting in s when the DTA starts in with clock valuation t reaches location f after performing n actions. Then for " f , p 0 (s, , t) " 0 and p 0 (s, f , t) " 1. Assume that p n (s, , t) is continuous (and so measurable) for all s and . Then the following equation holds for i − 1 t i C:

Observe that for τ > C, p n (sc(s), sc C`1 ( ), sc( , τ )) is constant since if there is a reset then sc( , τ ) " 0 and if there is no reset then sc( , τ ) " τ > C and so the valuation of the clock is irrelevant. Thus the equation can be rewritten as follows.

Observe that max(1, λ s )e −λsτ is uniformly continuous. So pick η > 0 such that

. Then for all t ă t t`η, one bounds |p n`1 (s, , t) − p n`1 (s, , t )| by the sum of three terms using the above equation to establish that |p n`1 (s, , t) − p n`1 (s, , t )| ε. Thus p n`1 (s, , t) is continuous. When t > C, p n`1 (s, , t) is constant and so continuous. Observe that p(s, , t) " lim n→8 p n (s, , t). So the mapping p(s, , t) is measurable as a limit of continuous mappings. Thus Eq. 1 holds for i − 1 t i C: Repeating the same argument as the one for the inductive case yields the result. When t > C, p(s, , t) is constant and so continuous. Proof. We will even prove this result when restricting the quantification to Markov chains with a single action and a single valuation of propositions for all states and a single successor for all states. Thus we can omit propositions and actions in the DTA and only consider simple chains.

Let A be an automaton that satisfies the hypothesis. We want to establish that for all configurations ( , t) in some region of G A reachable from ( 0 , 0), and for all states s of a simple Markov chain, p(s, , t) " z. We do this by induction on the distance from the initial region in the region graph and then we prove that z is either 0 or 1. The basis case of the induction corresponds to the assumption Pr M (A) " z, for all M. For the inductive step we assume that for a given ( , t), and for all states s of a simple chain, p(s, , t) " z and we prove that the p(s , , t ) " z, for all (s , , t ) reachable in one step from (s, , t). Let M be an arbitrary simple chain and define M λ as the simple chain with a single transition outgoing from its initial state to the initial state of M whose rate is λ. Let s be the initial state of M λ . By assumption, p(s, , t) " z. Define f (τ ) by p(sc(s), sc j ( ), sc( , t`τ )) when j − 1 ă t`τ j C and by p(sc(s), sc C`1 ( ), sc( , t`τ )) when t`τ > C. Equation 1 can be rewitten as p(s, , t) " τ 0 λe −λτ f (τ )dτ . Since for all λ, Pr M λ (A) " z, the Laplace transform of f (τ ) is equal to z λ , i.e. the Laplace transform of the constant function z. By the theorem of unicity of Laplace transforms, this entails that f (τ ) " z except for a set of null measure. However, consider a successor region ( , i) of location with clock valuation t .

• Either i " 0 (meaning that there has been a reset) and the region has a single point reached with non null probability. So p(sc(s), , 0) " z. • Or i > 0, so by Lemma 1, p(sc(s), , t ) is continuous inside the region w.r.t.

t and thus everywhere equal to z.

So the induction is established. So if a region of f is reachable in the region graph, then z " 1. Otherwise f is not reachable implying that no run is accepting, and thus z " 0.

We can now prove Theorem 1 (A na ň M A). Proof of Theorem 1. The DTA A in Fig. 1 (lower right) has an action set reduced to a singleton {a} (omitted in the figure) and an empty set of propositions. The language of A is the set of timed paths whose first action occurs at time τ P [2i, 2i`1[ for some i P N. Assume by contradiction that there exists A P A na such that for all Markov chain M, Pr M (A ) " Pr M (A). Pick an arbitrary Markov chain M and define M λ as the Markov chain which has a single transition from its initial state to the initial state of M with rate λ. It is routine to check that Pr M λ (A) " 1−e −λ 1−e −2λ (as only the first transition of M λ is relevant) and, consequently, lim λ→0 Pr M λ (A) " 1 2 and, given the hypothesis, also lim λ→0 Pr M λ (A ) " 1 2 . Pr M λ (A ) can be decomposed as p 1,λ`p2,λ where p 1,λ is the probability to accept the random timed path and that the first action takes place at most at time C and p 2,λ is the probability to accept the random timed path and that the first action takes place after C, where C is the maximal constant of A . But lim λ→0 p 1,λ " 0 and therefore lim λ→0 p 2,λ " 1 2 . On the other hand, let 1 be the location of A reached from its initial location when the value of the clock is greater than C, its maximal constant. There must be one, if not lim λ→0 p 2,λ " 0, which contradicts what derived above. We want to design an automaton A equivalent to A when reaching 1 with clock value greater than C: any timed path is accepted by A iff it is accepted by A when starting in 1 with clock valuation greater than C. For the construction we duplicate the automaton and merge the final location, the initial location is location 1 of the first copy, and in the first copy we add to the guard of all transitions the formula x > C and redirect the transitions that reset the clock to the corresponding location of the second copy.

But then lim λ→0 p 2,λ " Pr M (A ). Since lim λ→0 p 2,λ " 1 2 and M is arbitrary, this contradicts Proposition 1 applied to A .

The DTA in Fig. 1 (upper right) shows that the above counter-example is of practical interest. Consider a periodic system that cycles over phases of duration 2, each split in two sub-phases of duration 1 (for example a running and a reset phase) and that can experience good (G), bad (B), and neutral (N) actions, generated from a CTMC of arbitrary complexity. The depicted DTA allows one to compute the probability of the CTMC behaviours characterized by a good action in the running sub-phase, given that in the preceding phases no bad action has happened in the running phase. Any action is instead allowed during the reset phase.

We have established that there exists DTAs that cannot be translated into DTAs without autonomous transitions (A na ň M A). We now investigate whether restricted forms of use of autonomous transitions are as expressive as A na . To this goal we identify two additional subclasses of A, namely A nra and A rc , characterized by a limited presence of autonomous transitions and that are in the following subset relationship:

A rc is the subclass of automata A P A in which all cycles of A including an autonomous transition with a reset also include a synchronizing transition ( , γ, B, r, ) with r "↓ or γ " (x > C).

A rc in which there is no autonomous transition that resets the clock:

The DTA on the left of Fig. 1 belongs to A rc \A nra : indeed there is an autonomous transition with reset (from 1 to 0 ), therefore it is not in A nra , but although the transition is part of a cycle, that cycle also includes a synchronizing transition with reset (from 0 to 1 ). Any DTA with no reset on autonomous transitions is an example of A nra . The family A rc has been introduced to provide an accurate syntactical characterization of DTA for which the autonomous transitions do not add expressive power. In some sense, the DTA of Theorem 1 emphasizes the interest of A rc since the cycle performed by the autonomous resetting transition points out what increases the expressive power. A nra , which forbids clock resets on autonomous transitions, removes from CSL TA the capacity of combining time constants depending on the time elapsed during (a portion of) an execution. As observed in [12] (section 4), clock resets on autonomous transitions are what makes CSL TA more expressive than asCSL [6] .

The following frame summarizes the results for A subclasses.

A na " L A nra " L A rc ň M A with A rc (A nra ) exponentially more concise than A nra (A na , respectively)

We first establish that in A rc the autonomous resetting transitions can be mimicked in A nra using additional finite memory, but with exponential cost.

There exists an algorithm operating in exponential time that takes as input A P A rc and outputs A P A nra with L(A ) " L(A).

Sketch of Proof. The construction (1) duplicates locations by memorizing in the location an integer value, (2) take into account this value for modifying the guard and the destination of the outgoing transitions, and (3) deletes the reset of autonomous transitions. This value corresponds to the accumulated value of constants in the guards of resetting autonomous transitions since the last visit of a synchronizing transition with a reset or a guard x > C. The restriction over A rc ensures that this value is bounded by some finite integer K. However K may be exponential in the size of A and thus this transformation is exponential.

The exponential blowup due to the duplication of locations is unavoidable:

There exists a family {A n } nPN in A rc such that the size of A n is O(n 2 ) and for all A P A nra with L(A) " L(A n ), (|Aut|`1)|Synch| 2 n .

We now prove that autonomous transitions in A nra can be eliminated, also at an exponential cost.

Sketch of Proof. The construction proceeds in two steps: at first, cycles of autonomous transitions are eliminated, then all (linear) paths of autonomous transitions are eliminated. The first construction is quadratic, as we duplicate each location to store in the location the information on the number of autonomous transitions visited since the last visit of a synchronized transition. The idea of this construction is that if a path exceeds the number of autonomous transitions it must visit twice the same autonomous transition without visiting a synchronized transition and so diverges. In words: in the resulting DTA, divergence has been transformed into deadlock. This finite memory has a linear size w.r.t. the size of the original DTA.

The second step consists in eliminating autonomous transitions when there are no such cycles. The key point is to select a location which is the source of the last autonomous transition of a maximal path of such transitions. Thus every autonomous transition outgoing from reaches some location u where only synchronized transitions are possible. Roughly speaking, the construction builds a synchronized transition corresponding to a sequence of an autonomous transition followed by a synchronized transition. However the construction is more involved since has to be duplicated in order to check which autonomous transition can be triggered (or if no autonomous transition can be triggered). This duplication also has an impact on the incoming transitions of . Repeating (at most |L| times) this transformation eliminates all autonomous transitions. The exponential blowup due to the repetition of duplication of locations is unavoidable:

There exists a family of automata {A n } nPN in A nra such that the size of A n belongs to O(n log(n)) and for all A P A na with L(A) " L(A n ) the number of its locations is at least 2 n .

We have established that autonomous transitions do enhance expressiveness of single clock DTAs, and more precisely for the less discriminating case of the probability of the random paths of a CTMC accepted by the DTA. This is the most relevant one for comparing some variations of (1-clock) CSL TA defined in the literature. This enhanced expressiveness is due to the possibility of associating clock resets with autonomous transitions that occur in a cycle. The small counterexample of Proposition 1 can be seen as the basic construct to study systems with periodic behaviours or periodic phases, with clear practical implications. Even in DTA subclasses for which the autonomous transitions do not enhance expressiveness, they do play a role in defining concise DTAs: removing autonomous transitions may lead to an exponential blow up of the DTA.

We plan to investigate whether the precise identification of the characteristics that enhance expressiveness and conciseness can help the identification of the best algorithms for CSL TA model-checking, in particular for the componentbased method [4] . Moreover, following the suggestion by an anonymous reviewer, we intend to investigate further consequences of Proposition 1, for example to study systems that include probabilistic choices of autonomous transitions.

Modelling with Generalized Stochastic Petri Nets

Expressing and computing passage time measures of GSPN models with HASL

MC4CSL TA : an efficient model checking tool for CSL TA

Efficient model checking of the stochastic logic CSLTA

Model-checking continuous-time Markov chains

Model checking Markov chains with actions and state labels

On the logical characterisation of performability properties

Model-checking algorithms for continuous-time Markov chains

HASL: a new approach for performance evaluation and model checking from concepts to experimentation

Model checking of continuoustime Markov chains against timed automata specifications

Autonomous Transitions Enhance CSA TA Expressiveness and Conciseness

Model checking timed and stochastic properties with CSL TA

Monitoring CTMCs by multiclock timed automata

GCSRL-a logic for stochastic reward models with timed and untimed behaviour

Stochastic activity networks: structure, behavior, and application

State-space support for path-based reward variables