Bounded Model Checking for Parametric Timed Automata⋆ Michal Knapik1 and Wojciech Penczek1,2 1 Institute of Computer Science, PAS, J.K. Ordona 21, 01-237 Warszawa, Poland {Michal.Knapik}@ipipan.waw.pl 2 Institute of Informatics, Podlasie Academy, Sienkiewicza 51, 08-110 Siedlce, Poland penczek@ipipan.waw.pl Abstract. The paper shows how bounded model checking can be ap- plied to parameter synthesis for parametric timed automata with con- tinuous time. While it is known that the general problem is undecidable even for reachability, we show how to synthesize a part of the set of all the parameter valuations under which the given property holds in a model. The results form a complete theory which can be easily applied to parametric verification of a wide range of temporal formulae – we present such an implementation for the existential part of CTL−X . 1 Introduction and related work The growing abundance of complex systems in real world, and their presence in critical areas fuels the research in formal specification and analysis. One of the established methods in systems verification is model checking, where the system is abstracted into the algebraic model (e.g. various versions of Kripke structures, Petri nets, timed automata), and then processed with respect to the given prop- erty (usually a formula of modal or temporal logic). Classical methods have their limits however – the model is supposed to be a complete abstraction of system behaviour, with all the timing constraints explicitely specified. This situation has several drawbacks, e.g. the need to perform a batch of tests to confirm the proper system design (or find errors) is often impossible to fullfill due to the high complexity of the problem. Introducing parameters into models changes the task of property verification to task of parameter synthesis, meaning that parametric model checking tool produces the set of parameter valuations under which the given property holds instead of simple holds/does not hold answer. Unfortunately, the problem of parameter synthesis is shown to be undecidable for some of widely used parametric models, e.g. parametric timed automata [3, 8] and bounded parametric time Petri nets [15]. Many of model checking tools acquired new capabilities of parametric verifi- cation, e.g. UPPAAL-PMC [11] – the parametric extension of UPPAAL, LPMC [14] – extending PMC. Some of the tools were built from scratch with parametric ⋆ Partly supported by the Polish Ministry of Science and Higher Education under the grant No. N N206 258035. Recent Advances in Petri Nets and Concurrency, S. Donatelli, J. Kleijn, R.J. Machado, J.M. Fernandes (eds.), CEUR Workshop Proceedings, ISSN 1613-0073, Jan/2012, pp. 419–435. 420 Petri Nets & Concurrency Knapik and Penczek model checking in mind, e.g. TREX [1] and MOBY/DC [7]. Parametric analysis is also possible with HyTech [10] by means of hybrid automata. However, due to undecidability issues, algorithms implemented in these tools need not to stop and are very time and resource consuming. Another, very interesting approach is given in a recently developed IMITATOR tool [4] – having both the parametric timed automaton and the initial parameter valuation, IMITATOR synthesizes a set of parameter constraints. Substituting the parameters with a valuation sat- isfying these constraints is guaranteed to produce the timed automaton which is time-abstract equivalent to the one obtained from substituting the parameters with the initial valuation. In this paper we present a new approach to parametric model checking, based on the observation that while we are not able to synthesize the full set of parameter constraints in general, there is no fundamental rule which forbids us from obtaining a part of this set. In Section 2 we introduce the parametric region graph – an extension of region graph used in theory of timed automata [2] and show (in Section 3) how the computation tree of a model can be unwinded up to some finite depth in order to apply bounded model checking (BMC) techniques [5]. To the best knowledge of the authors, this is the first application of BMC to parametric timed automata and seems to be a quite promising direction of research – firstly due to the unique BMC advantage which allows for verification of properties in limited part of the model, secondly due to the fact that it is quite easy to present BMC-based model checking algorithms for existential parts of many modal and temporal logics. In fact we describe how Parametric BMC can be implemented for the existential subset of CTL−X logic in Section 3, including the analysis of a simplified parametric model of the 4-phase handshake protocol. 2 Theory of Parametric Timed Automata Pm P = {p1 , . . . , pm } In this paper we use two kinds of variables, namely parameters and clocks X = {x0 , . . . , xn }. An expression of the form i=1 ti · pi + t0 , where ti ∈ Z is called a linear expression. A simple guard is an expression of the form xi − xj ≺ e, where i 6= j, ≺∈ {≤, <} and e is a linear expression. A conjunction of simple guards is called a guard and the set of all guards is denoted by G. We valuate the clocks in nonnegative reals, and parameters in naturals (including 0) that is υ : P → N is a parameter valuation and ω : X → R≥0 is a clock valuation (both υ and ω can be thought of as points in, respectively, Nm and n R≥0 ). Additionally, following [11] we assume that ω(x0 ) = 0 – the ”false clock” x0 is fixed on 0 for convenience only, for uniform presentation of guards. By e[υ] we denote the value obtained by substituting the parameters in a linear expression e according to parameter valuation υ. We denote ω |=υ xi − xj ≺ e iff ω(xi ) − ω(xj ) ≺ e[v] holds, and naturally extend this notion to guards. We also need a notion of reset that is a set of expressions of the form xi := bi where bi ∈ N, and 0 < i ≤ n. The set of all resets is denoted by R, and the action of resetting a clock valuation ω by reset r ∈ R is defined as following: ω[r] is a clock valuation such that ω[r](xi ) = bi if xi := bi ∈ r, and ω[r](xi ) = ω(xi ) 2 Model checking for timed automata Petri Nets & Concurrency – 421 otherwise. If δ ∈ R and ω is a clock valuation, then ω + δ is a clock valuation such that (ω + δ)(xi ) = ω(xi ) + δ for all 0 < i ≤ n, and ω(x0 ) = 0. An initial clock valuation ω0 is the valuation satisfying ω(xi ) = 0 for all xi ∈ X. We also adopt a convenient notation from [11], where the ≤ symbol is treated as true and the < symbol is treated as f alse. The propositional formulae built from symbols ≤ and < are evaluated in a standard way. As to give an example, ≤⇒< evaluates to <, <⇒≤ evaluates to ≤, and ¬(≤ ∨ <) evaluates to <. 2.1 Parametric Timed Automata Let us recall some notions from the theory of parametric timed automata. Non- parametric timed automata [2] are state-transition graphs augmented with a finite number of clocks, and clock constraints guarding the transitions between states. Their parametric version [3] allows for using parameters (other than clocks) in guard expressions – which may be perceived as creating the general template for system behaviour under more abstract timed constraints. Definition 1. A tuple A = hQ, q0 , A, X, P, →, Ii where: – Q is a set of locations, – q0 ∈ Q is the initial location, – A is a set of actions, – X and P are, respectively, sets of clocks and parameters, – I : Q → G is an invariant function, – →⊆ Q × A × G × R × Q is a transition relation. is called a parametric timed automaton (PTA). All the above sets are finite. We a,g,r abbreviate (q, a, g, r, q ′ ) as q → q ′ . The semantics of PTA is presented below, in form of a labeled transition system. Definition 2 (Concrete semantics). Let A = hQ, q0 , A, X, P, →, Ii be a para- metric timed automaton and υ be a parameter valuation. The labeled transition d system of A under υ is defined as a tuple [A]υ = hS, s0 , →i where: – S = {(q, ω) | q ∈ Q, and ω is a clock valuation such that ω |=υ I(q)}, – s0 = (q0 , ω0 ) (we assume that ω0 |=υ I(q0 )), d – let (q, ω), (q ′ , ω ′ ) ∈ S. The transition relation → is defined as follows: d • if d ∈ R≥0 , then (q, ω) → (q ′ , ω ′ ) iff q = q ′ and ω ′ = ω + d, d a,g,r • if d ∈ A, then (q, ω) → (q ′ , ω ′ ) iff q → q ′ , and ω |=υ g, and ω ′ = ω[r]. The elements of S are called the concrete states of Aυ . The automaton obtained by substituting parameters in the guards and the invariants of A by appropriate values of the parameter valuation υ is denoted by Aυ . The concrete semantics of Aυ is defined as [Aυ ] = [A]υ . Notice that Aυ is a timed automaton and [Aυ ] – its concrete semantics [2]. 3 422 Petri Nets & Concurrency Knapik and Penczek Our definition of parametric timed automata slightly differs from the one presented in [11], namely, we do not allow nonnegative reals as parameter values. As it was shown in [3], the choice of the parameter valuation codomain does not change the fact that the emptiness problem is undecidable. We explain the origin of this restriction in the following subsection. 2.2 Parametric Region Graph In non-parametric timed automata theory, the region graph [2] is used as a part of a convenient method of presenting the concrete state space in a uniform, finite way. The finiteness of the resulting structure is a result of presence of both the bounded and unbounded regions. Intuitively, the bounded regions are convex bounded sets in the space of clock valuations, while the unbounded regions are convex and unbounded. The latter ones are defined using the maximal values of clock constraints – this is not possible in the general case of parametric timed automata (see however the optimization techniques in [11]), therefore in this paper we consider only the bounded regions. We divide the space of all the clock valuations into the set of regions using the following equivalence relation. Definition 3. Let ω, ω ′ be valuations of clocks X = {x0 , . . . , xn }. Then, ω ≈ ω ′ iff the following conditions hold: – ⌊ω(xi )⌋ = ⌊ω ′ (xi )⌋ for all xi ∈ X, – and f rac(ω(xi )) < f rac(ω(xj )) ⇐⇒ f rac(ω ′ (xi )) < f rac(ω ′ (xj )) for all i 6= j, 1 ≤ i, j ≤ n, – and f rac(ω(xi )) = 0 ⇐⇒ f rac(ω ′ (xi )) = 0 for all xi ∈ X, where f rac(ω(xi )) denotes the fractional part of ω(xi ). The equivalence classes of ≈ are called (detailed) regions. To our aims it is convenient to describe regions as sets of valuations satisfying certain guard expressions. Lemma 1. Let X = {x0 , . . . , xn } beVa set of clocks, and Z – a region of val- uations. There exists a guard gZ = i,j∈{0,...,n},i6=j xi − xj ≺ij bij , such that ≺ij ∈ {≤, <} and bij ∈ Z satisfying: Z = {ω | ω |= gZ }. Proof. We need to specify the values of bij together with the accompanying relation ≺ij . Let Z = [ω]≈ (the following considerations are valid for any choice of ω from Z). – If f rac(ω(xi )) = 0, f rac(ω(xj )) = 0, let ≺ij =≤ and bij = ⌊ω(xi )⌋ − ⌊ω(xj )⌋, – if f rac(ω(xi )) 6= 0, f rac(ω(xj )) = 0, let ≺ij =< and bij = ⌈ω(xi )⌉ − ⌊ω(xj )⌋, – if f rac(ω(xi )) = 0, f rac(ω(xj )) 6= 0, let ≺ij =< and bij = ⌊ω(xi )⌋ − ⌊ω(xj )⌋, – for f rac(ω(xi )) 6= 0, f rac(ω(xj )) 6= 0 : • if f rac(ω(xi )) = f rac(ω(xj )), let ≺ij =≤, bij = ⌊ω(xi )⌋ − ⌊ω(xj )⌋, 4 Model checking for timed automata Petri Nets & Concurrency – 423 • if f rac(ω(xi )) < f rac(ω(xj )), put ≺ij =<, bij = ⌊ω(xi )⌋ − ⌊ω(xj )⌋, • if f rac(ω(xi )) > f rac(ω(xj )), let ≺ij =<, bij = ⌈ω(xi )⌉ − ⌊ω(xj )⌋. It is easy to see that if ω ≈ ω ′ , then for any guard g we have ω |= g iff ω ′ |= g. Therefore, as gZ was constructed in such a way that ω |= gZ , we have also ω ′ |= gZ for all ω ′ ∈ Z. On the other hand, if ω ′ |= gZ , then satisfaction of the guards of form xi − x0 ≺i0 bi0 and x0 − xi ≺0i b0i (recall that x0 is fixed) guarantees that ⌊ω ′ (xj )⌋ = ⌊ω(xj )⌋ for all xj ∈ X. Similarly, ω ′ (xi ) has nonzero fractional value iff f rac(ω(xi )) 6= 0, as ω ′ (xi ) ∈ (⌊ω(xi )⌋, ⌈ω(xi )⌉), provided that f rac(ω(xi )) 6= 0. Let us assume that 0 < f rac(ω(xi )), and f rac(ω(xi )) < f rac(ω(xj )), then from ω(xi ) − ω(xj ) < ⌊ω(xi )⌋ − ⌊ω(xj )⌋ we have ω ′ (xi ) − ω ′ (xj ) < ⌊ω ′ (xi )⌋ − ⌊ω ′ (xj )⌋. Therefore ω ′ (xi ) − ⌊ω ′ (xi )⌋ < ω ′ (xj ) − ⌊ω ′ (xj )⌋, thus f rac(ω(xi )) < f rac(ω(xj )). The guard constructed in the proof of the above lemma is called the charac- teristic guard of Z. In the above proof we used the fact that if one representative of an equivalence class satisfies a guard g, then so do all the remaining members. This is not true if we allow nonnegative reals as parameter values – for exam- ple it is easy to see that only some of representatives of class [(0, 0.3)] satisfy x1 − x0 < p under parameter valuation υ such that υ(p) = 0.5. Definition 4. Let A = hQ, q0 , A, X, P, →, Ii be a parametric timed automaton, X = {x0 , . . . , xn } and P = {p1 , . . . , pm }. We introduce a relation in the set of all the pairs (Z, C) where Z is a region, and C ⊆ Nm is a subset of the set of all the valuations of parametersV(treated as natural vectors). Let s = xi − xj ≺ e be a simple guard, and gZ = i,j∈{0,...,n},i6=j xi − xj ≺ij bij the characteristic guard of region Z. Then we define: s (Z, C) ; (Z ′ , C ′ ) iff Z = Z ′ and C ′ = C ∩ {υ | bij (≺ij ⇒≺)e[v]}. Let g be a guard and s a simple guard, then: g∧s g (Z, C) ; (Z ′ , C ′ ) iff for some (Z ′′ , C ′′ ) we have (Z, C) ; (Z ′′ , C ′′ ) s and (Z ′′ , C ′′ ) ; (Z ′ , C ′ ). g There is a natural intuition behind the above definition – if (Z, C) ; (Z ′ , C ′ ) then (Z ′ , C ′ ) contains all the pairs (ω, υ) ∈ Z × C such that ω |=υ g. Such an operation is a counterpart for guard addition from [11], notice however that we do not need a burden of costly canonicalization. Below we state some basic g properties of ; relation. g Lemma 2. Let (Z, C) ; (Z ′ , C ′ ), where g is a guard. Then, the following con- ditions hold: 1. if (ω, υ) ∈ (Z, C) and ω |=υ g, then (ω, υ) ∈ (Z ′ , C ′ ), 2. if (ω, υ) ∈ (Z ′ , C ′ ), then ω |=υ g. 5 424 Petri Nets & Concurrency Knapik and Penczek Proof. Let us start with the first part of the lemma. Let us assume that ω |=υ g. By the induction on the complexity of g we prove that υ ∈ C ′ . The base case is when g = xi − xj ≺ e (g is a simple guard). Let us assume that gZ contains a simple guard of the form xi − xj ≤ bij where bij ∈ Z. Notice that in this case the characteristic guard contains also a simple guard of the form xj − xi ≤ −bij , therefore bij = ω ′ (xi ) − ω ′ (xj ) for each ω ′ ∈ Z. As ω |=υ g, then bij = ω ′ (xi ) − ω ′ (xj ) ≺ e[υ]. Therefore bij ≺ e[υ], which in this case means that bij (≺ij ⇒≺)e[υ]. Now let us assume that gZ contains a simple guard of the form xi − xj < bij . In this case, for each ω ′ ∈ Z there exists δ ∈ (0, 1) such that ω ′ (xi ) − ω ′ (xj ) = (bij − 1) + δ. Let us notice that e[υ] ∈ Z, therefore from (bij − 1) + δ = ω ′ (xi ) − ω ′ (xj ) ≺ e[υ] we obtain bij ≤ e[υ]. The latter inequality means that in this case bij (≺ij ⇒≺)e[υ] holds. g ′ ∧s For the induction step, notice that if (Z, C) ; (Z ′ , C ′ ) (g ′ is a guard, g′ and s a simple guard), then there exists (Z ′′ , C ′′ ) such that (Z, C) ; (Z ′′ , C ′′ ) s and (Z ′′ , C ′′ ) ; (Z ′ , C ′ ). From the inductive assumption we obtain that as ω |=υ g ′ ∧ s implies ω |=υ g ′ , then υ ∈ C ′′ . Similarly, as (ω, υ) ∈ (Z ′′ , C ′′ ) and ω |=υ s, we have υ ∈ C ′ . The proof of the second part of the lemma is also by the induction on the structure of g. Assume that g = xi − xj ≺ e and gZ contains a simple guard of g form xi −xj ≺ij bij . If (Z, C) ; (Z ′ , C ′ ), then C ′ = C ∩{υ | bij (≺ij ⇒≺)e[υ]}. As ω(xi )−ω(xj ) ≺ij bij and bij (≺ij ⇒≺)e[υ] then ω(xi )−ω(xj )(≺ij ∧(≺ij ⇒≺))e[υ]. Therefore we have ω(xi ) − ω(xj ) ≺ e[υ], thus ω |=υ g. g ′ ∧s For the induction step, let us notice that if (Z, C) ; (Z ′ , C ′ ), then there g′ s exists (Z ′′ , C ′′ ) such that (Z, C) ; (Z ′′ , C ′′ ) and (Z ′′ , C ′′ ) ; (Z ′ , C ′ ). If (ω, υ) ∈ (Z ′ , C ′ ) then by the inductive assumption ω |=υ s holds. As C ′ ⊆ C ′′ ⊆ C, then υ ∈ C ′′ and (ω, υ) ∈ (Z ′′ , C ′′ ). Therefore, from the inductive assumption we obtain ω |=υ g ′ and, finally, ω |=υ g ′ ∧ s. From the above lemma we immediately obtain the following corollary. Corollary 1. Let Z be a region, and C a subset of set of all the parameter valuations. Then, the following conditions hold: g 1. if (Z, C) ; (Z ′ , C ′ ), then Z ′ × C ′ = Z × C ∩ {(ω, υ) | ω |=υ g}, g 2. if ω ∈ Z, υ ∈ C, and ω |=υ g, then (Z, C) ; (Z ′ , C ′ ) for some Z ′ , C ′ such ′ ′ that (ω, υ) ∈ Z × C . In order to develop our theory further, we need to define two additional operations on regions. Definition 5. Let Z = [ω]≈ be a region and r ∈ R be a reset. Then, resetting of Z by r is defined as: Z[r] = [ω[r]]≈ . Clearly, resetting of a region does not depend on the choice of a representa- tive. 6 Model checking for timed automata Petri Nets & Concurrency – 425 Definition 6. Let Z and Z ′ be two different regions. Region Z ′ is called a time successor of Z (denoted by τ (Z)) iff for all ω ∈ Z there exists δ ∈ R such that ω + δ ∈ Z ′ and ω + δ ′ ∈ Z ∪ Z ′ for all δ ′ ≤ δ. Now, we are in the position to present the notion of a parametric region graph, being an extension of region graph used in theory of timed automata [2]. The main idea is to augment regions with sets of parameter valuations under which the given concrete state (its equivalence class) is reachable from the initial state, and to mimick the transitions in the concrete semantics by their counterparts in parametric region graph. Definition 7. Let A = hQ, q0 , A, X, P, →, Ii be a parametric timed automaton. d Define the parametric region graph of A as the tuple P REG(A) = hS, s0 , →i where: – S = {(q, Z, C) | q ∈ Q, Z is a region, C ⊆ Nm and ∀υ∈C ∃ω∈Z ω |=υ I(q)}, – s0 = (q0 , Z0 , C0 ) where Z0 = [ω0 ]≈ and C0 = {υ | ω0 |=υ I(q0 )}, d – (q, Z, C) → (q ′ , Z ′ , C ′ ) is defined as follows: • if d = τ (time transition), then q = q ′ , Z ′ = τ (Z), and C ′ is such that I(q) (Z ′ , C) ; (Z ′ , C ′ ), d,g,r • if d ∈ A (action transition), then there exists a transition q → q ′ in A ′ g I(q ) and C ′′ such that (Z, C) ; (Z, C ′′ ) and (Z[r], C ′′ ) ; (Z ′ , C ′ ). Additionally, we call nodes of type (q, Z, ∅) dead, and assume that they have no outgoing transitions. Notice that in the above definition we could replace ∃ with ∀, due to the fact that for any guard g, fixed parameter valuation υ, and clock valuations ω, ω ′ such that ω ≈ ω ′ we have ω |=υ g iff ω ′ |=υ g. Both the concrete semantics of (parametric) timed automaton, and (para- metric) region graph are labelled transition systems. We define finite and infinite runs in a labelled transition system in a usual way. Lemma 3. Let A be a parametric timed automaton, and ρn = s0 , s1 , . . . sn a finite run in P REG(A), where si = (qi , Zi , Ci ), and Cn 6= ∅. For any (ω, υ) ∈ Zn × Cn there exists a finite run µn = t0 , t1 , . . . tn in Aυ , such that ti = (qi , ωi ), ωi ∈ Zi for i ∈ {0, . . . , n}, and ωn = ω. Proof. The base case of n = 0 is straightforward – as from the definition of P REG(A) we have ω |=υ I(q0 ) for any (ω, υ) ∈ Z0 × C0 . d Recall that Cn ⊆ Cn−1 . If sn−1 → sn is a time transition (with d = τ ), then τ (Zn−1 ) = Zn . Therefore for each ωn ∈ Zn there exist ωn−1 ∈ Zn−1 , and l ∈ R, such that ωn = ωn−1 + l. We conclude the case by noticing that (ωn−1 , υ) ∈ Zn−1 × Cn−1 , ωn |=υ I(qn ), and using the inductive assumption. d Now, if sn−1 → sn is an action transition (d ∈ A), then there exists a d,g,r g transition qn−1 → qn in A, and a subset C ′ of Nm , such that (Zn−1 , Cn−1 ) ; 7 426 Petri Nets & Concurrency Knapik and Penczek I(qn ) (Zn−1 , C ′ ), and (Zn−1 [r], C ′ ) ; (Zn−1 [r], Cn ). Therefore for each ωn ∈ Zn we have ωn |=υ I(qn ), and there exists ωn−1 ∈ Zn−1 such that ωn = ωn−1 [r], ωn−1 |=υ I(qn−1 ), and ωn−1 |=υ g (notice that υ ∈ Cn ∩C ′ ∩Cn−1 ). We conclude the case by assuming tn−1 = (qn−1 , ωn−1 ), tn = (qn , ωn ) and using the inductive assumption. Notice that the definition of the transition relation in P REG(A) implies that in ρn we have Ci+1 ⊆ Ci for all 0 ≤ i < n. In particular Cn ⊆ Ci for all 0 ≤ i ≤ n. The above lemma does not extend to infinite runs, as shown in the following example. Example 1. Consider the simple parametric timed automaton: q x1 − x0 < p The following infinite run in P REG(A) does not have a counterpart in Aυ due to the fact that p is unbounded. τ τ (q, [(0, 0)], {p | p > 0}) → (q, [(0, 0.1)], {p | p ≥ 1}) → τ τ (q, [(0, 1)], {p | p > 1}) → (q, [(0, 1.1)], {p | p ≥ 2}) → . . . d Consider a transition (q, Z, C) → (q ′ , Z ′ , C ′ ) in P REG(A). Notice that if ′ d ω ∈ Z, υ ∈ C ∩ C ′ , then (q, ω) → (q ′ , ω ′ ) in [Aυ ], where d′ = d if d is an action, and d′ is some real number if d = τ . From this observation and Lemma 3 we obtain the following corollary. Corollary 2. Let ρ = s0 , s1 , . . . be an infinite run in P REG(A), such that si = (qi , Zi , Ci ) for some Zi , Ci , and let υ ∈ Ci for all i ≥ 0. Then, there exists an infinite run µ = t0 , t1 , . . . in the concrete semantics of Aυ , such that ti = (qi , ωi ), and ωi ∈ Zi . The counterpart of Lemma 3 holds without the restriction on finiteness of runs. Lemma 4. Let A be a parametric timed automaton, and µ = t0 , t1 , . . . tn . . . an d infinite (finite) run in Aυ , where ti = (qi , ωi ), and such that if ti → ti+1 is a time transition, then [ωi+1 ] = τ ([ωi ]). Then, there exists an infinite (finite, resp.) run ρ = s0 , s1 , . . . sn . . . in P REG(A) such that si = (qi , Zi , Ci ), and (ωi , υ) ∈ Zi × Ci for each i ≥ 0 (0 ≤ i ≤ n, resp.). 8 Model checking for timed automata Petri Nets & Concurrency – 427 Proof. Let us start with the finite run case, and let Zi = [ωi ]. The base case is straightforward – just assume C0 = {u | ω0 |=u I(q0 )} and notice that υ ∈ C0 . Assume that we have already constructed a finite run ρn = s0 , s1 , . . . sn−1 . d If tn−1 → tn is a time transition, then τ (Zn−1 ) = Zn , ωn ∈ Zn , υ ∈ Cn−1 , and ωn |=υ I(qn ). Therefore, from Corollary 1 we obtain that there exists C ′ I(qn ) such that (Zn , Cn−1 ) ; (Zn , C ′ ), υ ∈ C ′ , and conclude the case by placing Cn = C ′ , and the inductive assumption. d If tn−1 → tn is an action transition, then there exists a transition in A such d,g,r that for some guard g and reset r we have qn−1 → qn . Notice that as (ωn−1 , υ) ∈ Zn−1 × Cn−1 , ωn−1 |=υ g, ωn−1 [r] = ωn , and ωn |=υ I(qn ), from Corollary 1 we g have that there exist sets C ′ , C ′′ satisfying (Zn−1 , Cn−1 ) ; (Zn−1 , C ′ ), υ ∈ C ′ , I(qn ) and (Zn−1 , C ′ ) ; (Zn , C ′′ ). We conclude the case by assuming Cn = C ′′ . Let µ = t0 , t1 , . . . be an infinite run in Aυ . We have already shown that for each finite prefix µn = t0 , t1 , . . . tn we can construct its counterpart ρn = sn0 , sn1 , . . . snn in P REG(A), where sin = (qi , Zi , Cin ). Notice that Cin = Cin+1 , so the infinite sequence ρ = s0 , s1 , . . ., where si = (qi , Zi , Cii ) is a valid infinite run in P REG(A) satisfying (ωi , υ) ∈ Zi × Cii for all i ≥ 0. The following definition formalizes the connection between parametric re- gion graph, and region graphs. In what follows, by a subgraph of P REG(A) = d d d hS, s0 , →i we mean a tuple hS ′ , s0 , ֒→i, where S ′ is a subset of S, and ֒→ is the d restriction of → to S ′ . Definition 8. Let A be a parametric timed automaton, υ – a parameter valua- tion, and F – a subgraph of P REG(A). By proj(F, υ) we define a subgraph of F whose states are tuples (q, Z, C) such that υ ∈ C. Observe that proj(P REG(A), υ) is in fact isomorphic with the region graph of Aυ – by a forgetful functor stripping C from tuple (q, Z, C). 3 Bounded Model Checking for ECTL−X The central idea of bounded model checking is to unfold the computation tree of a considered model up to some depth, and then perform the analysis of such a finite structure [5]. Such an approach limits us to verification (and in our case – parameter synthesis) of existential properties only, it should be noted however that implicit model checking methods often fail in case of large and complex systems. Bounded model checking seems to be especially effective in searching for counterexamples, i.e. in proving that some undesirable property holds in a model. This allows for detection of serious design flaws of concurrent and reactive systems. The non-parametric model checking tool verifies a model (system specifica- tion) against a given property (usually in form of a temporal logic formula), 9 428 Petri Nets & Concurrency Knapik and Penczek producing the answer of simple holds/does not hold type. Its parametric coun- terpart is supposed to work slightly differently – having a parametric model we expect the answer in form of a set of parameter values under which a given prop- erty is satisfied. The automated synthesis of a complete set of desired parameter valuations is not possible in case of timed automata due to general undecid- ability of the problem, however obtaining a part of this set still seems to be a worthy goal. Our approach allows for incremental synthesis of parameters, i.e. if the valuations obtained by analysis of a part of a computation tree are not suf- ficient, then the tree can be unfolded up to a greater depth for further analysis. Combined with an expert supervision, the synthesized parameter valuations can give rise to hypotheses specifying the whole space of desired parameters. We propose the following general flow of property verification/parameter synthesis. Fig. 1. Parametric Bounded Model Checking schema The above diagram is very general. One of the approaches in the current applications of bounded model checking to verification of system properties is to encode the limited part of the computation tree together with a property in question as a propositional formula [6, 13]. The result can be checked using an efficient SAT-solver. 3.1 From Parametric Region Graph to concrete semantics The P REG(A) structure is infinite. In order to represent the infinite runs in a finite substructure we need a notion of loop. 10 Model checking for timed automata Petri Nets & Concurrency – 429 d Definition 9. Let ρn = s0 , s1 , . . . sn be a finite run in P REG(A), and si → si+1 for all 0 ≤ i < n. If sn = (qn , Zn , Cn ) and there exists si = (qi , Zi , Ci ), where d 0 ≤ i < n such that sn → si and qn = qi , Zn = Zi , then ρn is called a loop. Let ρn = s0 , s1 , . . . sn be a loop in P REG(A), such that si = (qi , Zi , Ci ), and (qn , Zn ) = (qj , Zj ) for some j < n. We can create an infinite run ρ̂ = sˆ0 , sˆ1 , . . . by unwinding the ρn loop as follows:  (qi , Zi , Cn ) for i < n sˆi = (qj+(n−i)mod(n−j) , Zj+(n−i)mod(n−j) , Cn ) for i ≥ n. The validity of such a construction is based on the observation that Cn ⊆ Ci for all 0 ≤ i ≤ n and the fact that transitions in P REG(A) are defined in terms of gZ and guards only. Applying Corollary 2 to such an unwinding we obtain the following corollary. Corollary 3. Let ρ = s0 , s1 , . . . , sn be a loop in P REG(A), where si = (qi , Zi , Ci ), and υ ∈ Cn – a parameter valuation. There exists an infinite run µt = t0 , t1 , . . . in the concrete semantics of Aυ , where ti = (qˆi , ωi ), ωi ∈ Zi for i < n, ωi ∈ Zj+(n−i)mod(n−j) for i ≥ n, and:  qi for i < n qˆi = qj+(n−i)mod(n−j) for i ≥ n. 3.2 Parametric Bounded Model Checking for ECTL−X The presented method can be applied to the verification of a variety of proper- ties. As the example, in this subsection we present the application of introduced theory to verification of properties specified in the existential part of Compu- tation Tree Logic (CTL−X ) without the next operator [9] – namely ECTL−X . Intuitively, CTL−X uses a branching time model, where many possible paths in the future exist. The whole CTL−X contains both the universal (”for all the pos- sible paths”) and existential modalities (”there exists a path in the future”) while ECTL−X contains only the latter ones – see [13] for more thorough treatment. Definition 10 (CTL−X and ECTL−X syntax). Let PV be a set of propositions containing the true symbol, and p ∈ PV. The set of well-formed CTL−X formulae is given by the following grammar: Φ ::= p | ¬Φ | Φ ∨ Φ | Φ ∧ Φ | EGΦ | EΦU Φ. The existential subset of CTL−X , i.e. ECTL−X is defined as a restriction of CTL−X such that the negation can be applied to the propositions only. def def Additionally we use the derived modalities: EF α = E(trueU α), AF α = def ¬EG¬α, AGα = ¬EF ¬α. Each modality of CTL−X has an intuitive meaning. The path quantifier A stands for ”on every path” and E means ”there exists a 11 430 Petri Nets & Concurrency Knapik and Penczek path”. G stands for ”in all the states”, F means ”in some state”, and U has a meaning of ”until”. We augment the given parametric timed automaton A = hQ, q0 , A, X, P, → , Ii with a labelling function L : Q → 2PV . Let us present an intepretation of ECTL−X formulae for a parametric region graph. Definition 11 (ECTL−X semantics for parametric region graph). Let A = hQ, q0 , A, X, P, →, Ii be a parametric timed automaton, and F – a subgraph of its parametric region graph, such that (q0 , Z0 , C0′ ), where C0′ ⊆ C0 , is a state of F . Let s be a state of F , p ∈ PV, and α, β be ECTL−X formulae. We treat F as a model for ECTL−X formulae, defining the |= relation as follows. 1. F, (q, Z, C) |= p iff p ∈ L(q), 2. F, s |= ¬p iff F, s 6|= p, 3. F, s |= α ∨ β iff F, s |= α or F, s |= β, 4. F, s |= EαU β iff there exists a run ρn = s0 , s1 , . . ., where s0 = s, si are states of F for i ≥ 0, F, sj |= β for some j ≥ 0, and F, si |= β for all i < j, 5. F, s |= EGα iff there exists a run ρn = s0 , s1 , . . ., such that F, si |= α for all i ≥ 0. We abbreviate F, (q0 , Z0 , C0 ) |= α as F |= α. The counterpart of the above definition for the timed automaton Aυ = d hS, s0 , →i obtained from the parametric timed automaton A under the parameter valuation υ is similar – except for that it is defined over the concrete seman- tics (s ∈ S). Therefore the only difference is in the first clause which takes the following form: 1. Aυ , (q, ω) |= p iff p ∈ L(q) As previously, we abbreviate Aυ , (q0 , ω0 ) |= α as Aυ |= α. In order to apply bounded model checking to verification of temporal proper- ties in P REG(A) we need to specify the version of the above semantics for finite subgraphs of P REG(A). The only difference concerns clauses 4 and 5 which take the following form: 4. F, s |= EαU β iff there exists a finite run ρn = s0 , s1 , . . . sn , where s0 = s, si are states of F for 0 ≤ i ≤ n, F, sj |= β for some 0 ≤ j ≤ n, and F, si |= β for all i < j, 5. F, s |= EGα iff there exists a loop ρn = s0 , s1 , . . . , sn , such that F, si |= α for all 0 ≤ i ≤ n. Recall that timed automaton Aυ is strongly non-zeno (see [16]) iff for each ai ,gi ,ri sequence of states q1 , . . . , qn such that qi −→ qi+1 for all 0 ≤ i < n, and an ,gn ,rn qn −→ q1 (we call such a sequence a structural loop) there exists a clock x satisfying the following conditions: – for some 1 ≤ i ≤ n the x clock is reset in step i (i.e. x := 0 ∈ ri ), 12 Model checking for timed automata Petri Nets & Concurrency – 431 – there exists 1 ≤ j ≤ n such that for any clock valuation ω if ω |=υ gj , then ω(x) ≥ 1. Intuitively, if an automaton is strongly non-zeno, then in each its loop at least one unit of time elapses ([16]). Notice that checking if the automaton is strongly non-zeno does not require any representation of the state space. Theorem 1. Let A be a parametric timed automaton, F – a finite T subgraph of P REG(A) containing state (q0 , Z0 , C0′ ), where C0′ ⊆ C0 , and P = {C | (q, Z, C) is a state of F }. If P is nonempty, and Aυ is strongly non-zeno for each υ ∈ P , then for each formula α ∈ ECTL−X if F |= α, then Aυ |= α for all υ ∈ P . Proof. Let υ ∈ P be a parameter valuation. Denote by F̂ a (possibly infinite) subgraph of P REG(A) created in two steps: – firstly, by adding to F the new states created by unwinding of each loop along the lines presented above – obtaining F ′ , – secondly, by replacing all the states (q, Z, C) in F ′ by (q, Z, P ) – obtaining F̂ . It is easy to see that F |= α iff F̂ |= α. Recall that proj(F̂ , υ) is isomorphic to some subgraph of the region graph of Aυ . As satisfiability of ECTL−X formulae in a subgraph of the region graph implies satisfiability in the region graph, and satisfiability in region graph is equivalent to satisfiability in the concrete model (see [16]) we obtain the thesis of the theorem. 3.3 Example – four phase handshake protocol In this section we perform a first step in parametric analysis of a simplified version of four phase handshake protocol. The protocol is extensively used in practice and widely studied, having both the software and hardware implemen- tations [?,?]. The considered system consists of two communicating entities – the Producer and the Consumer. The Producer creates data packages and sends them to the Consumer. Both the components communicate using two shared boolean variables, that is: req (request) governed by the Producer and used to signal the Consumer that the data is prepared and ready to be read, and ack (acknowledge) governed by the Consumer and used to signal the Producer that the data has been read successfully and the Consumer is ready. The initial value of both the variables is false. The running system goes through the following sequence of signals (req, ack): (f alse, f alse) → (true, f alse) → (true, true) → (f alse, true) → (f alse, f alse). As we have no tool for automated analysis at our disposal yet, we analyze the simplified version of the system behaviour. We introduce two parameters, omitting the signal propagation time, namely: minIO, and maxIO being, re- spectively, the lower and the upper bound on read/write time. 13 432 Petri Nets & Concurrency Knapik and Penczek Producer Consumer wait wa for wait for send receive ack == true req == false req := false ack := false ack == false req == true wait for wait for Ack Req put Data get Data req := true ack := true Fig. 2. 4–phase handshake protocol putData minIO < x1 s0 s1 Producer Ready x2 := 0 Producer Idle Consumer Ready Consumer Ready x1 < maxIO x2 < maxIO readData minIO ≤ x2 return s2 x1 − x2 ≤ IdleSender() x1 := 0 Producer Idle Consumer Idle Fig. 3. 4–phase handshake protocol, behaviour diagram The IdleSender function guards the time that the Producer is allowed to be idle after putting data into some shared transmission vehicle (e.g. a bus). Let us put IdleSender() := maxIO − minIO and unwind the Parametric Region Graph of Figure 3 (we omit the dummy clock x0 ). Notice that the above graph contains a loop, introduced by the sequence of actions: τ, τ, putData, readData, return. This loop can be unwinded as presented in Subsection 4.1 into an infinite path in the Parametric Region Graph, and into 14 Model checking for timed automata Petri Nets & Concurrency – 433 s0 [(0, 0)] s0 τ putData s1 [(0.1, 0.1)] [(0, 0)] maxIO ≥ 1 ∅ dead τ putData s0 s1 [(1, 1)] [(0.1, 0)] maxIO > 1 maxIO ≥ 1 τ putData τ readData s0 s1 s1 s2 [(1.1, 1.1)] [(1, 0)] [(1, 0.1)] [(0.1, 0)] maxIO ≥ 2 maxIO > 1 maxIO ≥ 1 ∅ minIO = 0 dead putData readData readData τ τ τ s0 s1 s1 s2 s1 s2 [(2, 2)] [(1.1, 0)] [(1.1, 0.1)] [(1, 0)] [(1.1, 1)] [(1, 0.1)] maxIO > 2 maxIO ≥ 2 maxIO > 1 maxIO > 1 maxIO > 1 maxIO ≥ 1 minIO ≤ 1 minIO = 0 minIO = 0 minIO = 0 minIO = 0 readData τ readData readData return putData τ τ τ τ return τ s0 s1 s1 s2 s1 s2 s0 s1 s2 s0 [(2.1, 2.1)] [(2, 0)] [(2, 0.1)] [(1.1, 0)] [(2, 1)] [(1.1, 0.1)] [(0, 0)] [(2, 1.1)] [(1.1, 1)] [(0, 0.1)] maxIO ≥ 3 maxIO > 2 maxIO ≥ 2 maxIO ≥ 2 maxIO > 1 maxIO > 1 maxIO > 1 maxIO ≥ 2 maxIO > 1 maxIO ≥ 1 minIO ≤ 2 minIO ≤ 1 minIO = 0 minIO = 0 minIO = 0 minIO = 0 minIO = 0 minIO = 0 minIO = 0 Fig. 4. The 4–phase handshake protocol, Parametric Region Graph of depth 5 loops in concrete semantics of non-parametric timed automata with minIO = 0, and maxIO instantiated by any value greater that 1. The graph of Figure 4, treated as a subgraph of the Parametric Region Graph of Figure 3 allows us to observe that in the considered system the property EGEF (P roducerIdle ∧ ConsumerReady) holds for minIO = 0, and maxIO > 1, with the previously mentioned loop as a witness. The intuition behind the considered formula is that the Producer will put data into the transmission infinitely often in the running system. Of course, this is only the first, hand-made, step of synthesis of the param- eter valuations under which the considered property is satisfied. The complete analysis of non-simplified versions with more parameters and components has to wait until we develop the planned tool. 4 Future work The theory presented in this paper is to be implemented in Verics model checker [12]. There is a growing evidence [14, ?] of success of model checking in verifica- tion of safety critical industrial applications, and the idea of parameter synthesis for a complex model or protocol seems to be promising in analysis and design of real-world systems. Also, as the method is quite general, we expect that it may be applied to many known temporal, modal and epistemic logics. 15 434 Petri Nets & Concurrency Knapik and Penczek References 1. R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994. 2. R. Alur, T. Henzinger, and M. Vardi. Parametric real-time reasoning. In Proc. of the 25th Ann. Symp. on Theory of Computing (STOC’93), pages 592–601. ACM, 1993. 3. É. André, T. Chatain, E. Encrenaz, and L. Fribourg. An inverse method for parametric timed automata. International Journal of Foundations of Computer Science, 20(5):819–836, October 2009. 4. A. Annichini, A. Bouajjani, and M. Sighireanu. Trex: A tool for reachability analysis of complex systems. In Proc. of CAV, pages 368–372, 2001. 5. A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. In Highly Dependable Software, volume 58 of Advances in Computers. Academic Press, 2003. Pre-print. 6. I. Blunno, J. Cortadella, A. Kondratyev, L. Lavagno, K. Lwin, and C. Sotiriou. Handshake protocols for de-synchronization. In International Symposium on Ad- vanced Research in Asynchronous Circuits and Systems, pages 149–158. IEEE Computer Society Press, 2004. 7. E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfi- ability solving. Formal Methods in System Design, 19(1):7–34, 2001. 8. H. Dierks and J. Tapken. Moby/DC - a tool for model-checking parametric real- time specifications. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03), volume 2619 of LNCS, pages 271–277. Springer-Verlag, 2003. 9. L. Doyen. Robust parametric reachability for timed automata. Information Pro- cessing Letters, 102:208–213, 2007. 10. E. A. Emerson and E. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241–266, 1982. 11. S.B. Furber and P. Day. Four-phase micropipeline latch control circuits. In IEEE Transactions on VLSI Systems, volume 4, pages 247–253, 1996. 12. T. Henzinger, P. Ho, and H. Wong-Toi. HyTech: A model checker for hybrid systems. In Proc. of the 9th Int. Conf. on Computer Aided Verification (CAV’97), volume 1254 of LNCS, pages 460–463. Springer-Verlag, 1997. 13. T. Hune, J. Romijn, M. Stoelinga, and F. Vaandrager. Linear parametric model checking of timed automata. In Proc. of the 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), volume 2031 of LNCS, pages 189–203. Springer-Verlag, 2001. 14. M. Kacprzak, W. Nabialek, A. Niewiadomski, W. Penczek, A. Pólrola, M. Szreter, B. Woźna, and A. Zbrzezny. VerICS 2008 - a model checker for time Petri nets and high-level languages. In Proc. of Int. Workshop on Petri Nets and Software Engineering (PNSE’09), pages 119–132. University of Hamburg, 2009. 15. Spelberg R. L., De Rooij R. C. H., , and Toetenel W. J. Application of parametric model checking – the root contention protocol using lpmc. In Proc. of the 7th ASCI Conference, pages 73–85, February 2000. 16. W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135–156, 2002. 17. M. Stoelinga. Fun with firewire: A comparative study of formal verification meth- ods applied to the ieee 1394 root contention protocol. In Formal Asp. Comput., volume 14, pages 328–337, 2003. 16 Model checking for timed automata Petri Nets & Concurrency – 435 18. L-M. Tranouez, D. Lime, and O. H. Roux. Parametric model checking of time Petri nets with stopwatches using the state-class graph. In Proc. of the 6th Int. Workshop on Formal Analysis and Modeling of Timed Systems (FORMATS’08), volume 5215 of LNCS, pages 280–294. Springer-Verlag, 2008. 19. S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisim- ulations. Formal Methods in System Design, 18(1):25–68, 2001. 17