Parameter Synthesis for Timed Kripke Structures Extended Abstract Michal Knapik1 and Wojciech Penczek1,2 1 Institute of Computer Science, PAS, Warsaw, Poland 2 University of Natural Sciences and Humanities, II, Siedlce, Poland {knapik,penczek}@ipipan.waw.pl Abstract. We show how to synthesise parameter values under which a given property, expressed in a certain extension of CTL called RTCTLP , holds in a parametric timed Kripke structure. Similarly as in fixed-point symbolic model checking approach, we introduce special operators which stabilise on the solution. The process of stabilisation is essentially a trans- lation from RTCTLP parameter synthesis problem to a discrete opti- mization task. We argue that this leads to new opportunities in model checking, including the use of integer programming and related tools. 1 Introduction Complex systems, both hardware and software, present in critical areas need to be verified. The best moment for the verification is the design phase, perhaps even before any prototype is developed. This helps to reduce errors and costs; the found flaws can also provide valuable pointers to a designer. Model checking is one of the established methods for verification of complex, timed, and reactive systems. In this approach, a model for a verified system is built (e.g. a Kripke structure or a Petri net), and a property to be checked is specified in a version of a modal logic (e.g. CTL or TCTL). The pair consisting of a model and a formula is the input for a model checking tool. The output is simply the property holds or property does not hold answer. However, such an approach has its drawbacks. In the beginning phases of a system design some of the features required in a model might be unknown (e.g. timing constraints), which forces the designer to substitute them with some guessed or standard values. Even if it is possible to present a full model of the system, there is no guarantee that this specification will not be subject to some changes. Often the minimal alteration of the original model may lead to violation of a checked property, therefore the process of verification has to be repeated. A system designer using model checking methods would substantially benefit from a tool that is able to accept an underspecified model with some values abstracted as parameters. In this case the expected output consists of a set of parameter valuations under which a given property holds. This approach is called parametric model checking or parameter synthesis. Parametric model checking 260 M. Knapik, W. Penczek eliminates the needs for guessing and for performing batches of tests for ranges of values. In this paper we show how to perform parameter synthesis for timed Kripke structures, i.e., Kripke structures where transition is augmented with an addi- tional label specifying how long it takes to traverse it. The input logic is a certain extension of Computation Tree Logic, which allows for expressing properties over the restricted fragments of paths. 1.1 Related Work and Paper Outline The logic considered in this paper and its models are based on the Real Time Computation Tree Logic (RTCTL) and timed Kripke structures introduced in [1]. As we show, the problem of parameter synthesis is decidable for RTCTLP . It is however not decidable for even as simple properties as reachability for many other models, e.g. parametric timed automata (PTA) [2, 3] and bounded para- metric time Petri nets [4]. Difference bound matrix - based semi-algorithms for reachability were extended to the PTA case in [5] and implemented in UPPAAL- PMC. In [6] we showed how to synthesise by means of bounded model checking a part of the set of valuations for PTA reachability. The problem of synthesis of bounded integer valuations for PTA is analysed in [7] and shown to be in PSPACE. In [8] the authors show how to synthesise the constraints on valu- ations under which a PTA is time-abstract equivalent to some initial one; the work is implemented in IMITATOR prototype tool. Parametric analysis is also possible with HyTech [9] by means of hybrid automata. In the next section we introduce the RTCTLP logic and its models. In Section 3 we show how to solve the synthesis problem via a translation to sets of linear inequalities over natural numbers. We conclude the work with a comment on the possible benefits and downsides of our approach and future plans. 2 Parameterized Temporal Logics Let N denote the set of all natural numbers (including 0), and let P (D) denote the power set of a set D. For any sequence x = (x1 , . . . , xn ) and 0 ≤ i ≤ n, let x|i = xi be the projection of x on the i–th variable. 2.1 The Syntax of RTCTLP The Real Time CTL [1] allows to express branching-time temporal properties involving the integer time-step depth of considered paths. Definition 1 (Syntax of RTCTLP ). Let PV be a set of propositional variables containing the symbol true. The formulae of RTCTLP are defined as follows: 1. every member of PV is a formula, 2. if α and β are formulae, then so are ¬α, α ∧ β, Parameter Synthesis for Timed Kripke Structures 261 3. if α and β are formulae, then so are EX ≤k α, EG≤k α, EαU ≤k β for k ∈ N. As to give an example of the meaning of an RTCTLP formula, EG≤5 p states that “there exists a path such that p holds in each state reached from the beginning in time not greater than 5.” 2.2 The Semantics of RTCTLP We evaluate the truth of the formulae in the parametric timed Kripke struc- tures. These are standard Kripke structures with the transitions decorated by additional labels interpreted as time variables. Definition 2. A parametric timed Kripke structure (a model) is a 5-tuple M = (S, s0 , T, →, L) where: – S is a finite set of states, – s0 ∈ S is the initial state, – T is a set of time step parameters (variables), – → ⊆ S × T × S is a transition relation such that for every s ∈ S there exists s0 ∈ S and t ∈ T with (s, t, s0 ) ∈ → (i.e., the relation is total), – L : S −→ 2PV is a valuation function satisfying true ∈ L(s) for each s ∈ S. Let s, s0 be two states of a model, and let t be a time step parameter. By t t s → s0 we denote that (s, t, s0 ) ∈ →. The intuitive meaning of s → s0 is that it takes t time units to reach s from s. We define in(s), out(s), link(s, s0 ) as 0 the sets of the labels of the transitions entering s, leaving s, and connecting t s with s0 , respectively. More formally, in(s) = {t ∈ T | s0 → s for s0 ∈ S}, t t out(s) = {t ∈ T | s → s0 for s0 ∈ S}, and link(s, s0 ) = {t ∈ T | s → s0 }. A function ω : T → N is called a parameter valuation. The set of all the parameter valuations is denoted by Ω. Consider an infinite sequence π = ti (s0 , t0 , s1 , t1 , . . .) such that si ∈ S and si → si+1 for i ∈ N. By πi = si we denote the i–th state of π. We define the time Pj−1 distance function between the positions π0 and πj on a sequence π as δπj = i=0 ti , and we assume that δπ0 = 0. If ω is Pj−1 a parameter valuation, then let δπj (ω) = i=0 ω(ti ). A sequence π is called an ω–path if limj→∞ δπj (ω) = ∞, or simply a path if ω is evident from the context. Definition 3 (Semantics of RTCTLP ). Let M = (S, s0 , T, →, L) be a model and s ∈ S. Let α, β ∈ RTCTLP , let ω ∈ Ω be a parameter valuation, and k ∈ N. M, s |=ω α denotes that α is true at the state s of M under the valuation ω. (In what follows we omit M where it is implicitly understood.) The relation |=ω is defined inductively as follows: 1. s |=ω p iff p ∈ L(s), 2. s |=ω ¬α iff s 6|=ω α, 3. s |=ω α ∧ β iff s |=ω α and s |=ω β, 4. s |=ω EX ≤k α iff there exists a path π s.t. π0 = s, δπ1 (ω) ≤ k, and π1 |=ω α, 262 M. Knapik, W. Penczek 5. s |=ω EG≤k α iff there exists a path π such that π0 = s, and for all i ≥ 0 if δπi (ω) ≤ k, then πi |=ω α, 6. s |=ω EαU ≤k β iff there exists a path π such that π0 = s and for some i ∈ N it holds that δπi (ω) ≤ k and πi |=ω β, and πj |=ω α for all 0 ≤ j < i. The RTCTLP logic slightly differs from RTCTL presented in [1]. Firstly, we have omitted the non-superscripted modalities. It is straightforward to extend the logic with these, and to see that the standard fixpoint algorithms for EG and EU verification can be applied with no changes. Secondly, we define the semantics on ω–paths, explicitly requiring the total traversal time to grow to the infinity with the depth of the path. This is consistent with the usual requirement of progressiveness of timed systems. 3 Translation to Linear Algebra In what follows we fix a model M = (S, s0 , T, →, L). We need several simple notions concerning the sets of statements (called linear statements) of the form c1 t1 + . . . + cn tn , where ti ∈ T are time step parameters, ci ∈ N, and ti 6= tj for all 1 ≤ i, j ≤ n, i 6= j. The set of all linear statements over T is denoted by LS T ; we omit the T subscript if it is implicitly understood. In this paper we consider only finite subsets of LS T . Let η = c1 t1 + . . . + cn tn , and let ω ∈ Ω. We define the application of ω to η as η[ω] = c1 ω(t1 ) + . . . + cn ω(tn ). We also define the k-bounding operation for k ∈ N as follows: [η]k := min(c1 , k + 1)t1 + . . . + min(cn , k + 1)tn . To show an example, consider the statement η = 6t1 + 9t2 and 5-bounding [η]5 = min(6, 6)t1 + min(9, 6)t2 = 6t1 + 6t2 . The operation of k-bounding has a property such that if ≈ ∈ {≤, <, >, ≥}, then for any k ∈ N the inequalities η ≈ k and [η]k ≈ k have the same sets of solutions. This can be easily verified on a case-by-case basis, by noticing that if a given coefficient ci of η exceeds k + 1, then any nonzero value of ti makes η ≈ k true for ≈ ∈ {>, ≥}, while ≈ ∈ {≤, <} means that only zero can be substituted for ti . Previous observation is crucial to the theory, as it means that every set of linear statements over the finite parameter set T , obtained by means of k- bounding with respect to some fixed natural k, is finite. We extend the [ ]k operation to subsets A ⊆ LS as follows: [A]k = {[η]k | η ∈ A}. Let A, B ⊆ LS, then we define A + B = {η + µ | η ∈ A and µ ∈ B}. Now let us consider A ⊆ LS, k ∈ N, and ≈ ∈ {≤, <, >, ≥}. We define [A]≈k as follows: [ [A]≈k = {ω | η[ω] ≈ k}. η∈A Parameter Synthesis for Timed Kripke Structures 263 As to give an example, let A = {t1 + 2t2 , t3 }, then [A]<4 consists of all the valuations ω such that ω(t1 ) + 2ω(t2 ) < 4, or ω(t3 ) < 4. We call the set S × P (Ω) the parametric state space, and its elements are called the parametric states. As to give an example, consider A ⊆ LS such that A = {2t1 + 3t2 , 2t1 + 3t4 }. The pair of form (s0 , [A]≤10 ) is a parametric state. The last preliminary notion needed in the rest of the paper is the auxiliary operator Flatten. Let B ⊆ S × P (Ω), then we define: [ (s, A) ∈ F latten(B) iff A = {C | (s, C) ∈ B}, A 6= ∅. To make this definition clearer, consider an example where B = {(s0 , C1 ), (s0 , C2 ), (s1 , C3 ), (s1 , C4 ), (s2 , C5 )}. In this case F latten(B) = {(s0 , C1 ∪ C2 ), (s1 , C3 ∪ C4 ), (s2 , C5 )}. If F latten(B) = B, then the set B is called flat. If B is flat, then by B(s) we denote the parameter selector, that is B(s) = C iff (s, C) ∈ B. The parameter selector is a well defined partial function on S. Algorithm 1 Synthesize(M, φ) 1: if φ = p then 2: return Ap 3: end if 4: if φ = ¬α then 5: Aα = Synthesize(M, α) 6: return ıAα 7: end if 8: if φ = α ∧ β then 9: Aα = Synthesize(M, α) 10: Aβ = Synthesize(M, β) 11: return Aα ∗ Aβ 12: end if 13: if φ = EX ≤k α then 14: Aα = Synthesize(M, α) 15: return EX ≤k Aα 16: end if 17: if φ = EG≤k α then 18: Aα = Synthesize(M, α) 19: return EG ≤k Aα 20: end if 21: if φ = EαU ≤k β then 22: Aα = Synthesize(M, α) 23: Aβ = Synthesize(M, β) 24: return EAα U ≤k Aβ 25: end if 264 M. Knapik, W. Penczek 3.1 The translation Our aim is to find all the valuations under which a given formula φ ∈ RTCTLP holds in a model M . In our solution we augment each state s with the set Aφ (s) of parameter valuations such that s |=ω φ iff ω ∈ Aφ (s). This is done recursively in Algorithm 1, with respect to the formula structure. For each s the set Aφ (s) can be represented as a finite union of solution sets of a finite number of linear (integer) inequalities. This means that Aφ (s) has a finite representation for each s, and for this reason we call the method a translation from RTCTLP parametric model checking to linear algebraic problem. Let p ∈ PV, then Ap = {(s, Ω) | p ∈ L(s)} is the set of such pairs (s, Ω) that p ∈ L(s). Intuitively, Ap contains the pairs consisting of a state in which p holds, together with the full set Ω; this expresses the lack of restrictions on the parameter values. Obviously, Ap is flat. In the algorithm we use several new operators that are counterparts of propo- sitional connectives and RTCTLP modalities: 1. operator ∗ – a counterpart of ∧, 2. operator ı – related to ¬, 3. operator EX ≤k – a counterpart of EX ≤k , 4. operator EG ≤k – a counterpart of EG≤k . 5. operator EU ≤k – related to EU ≤k . The detailed description of these notions is a subject of the rest of this section, starting with the ∗ operator. Definition 4. Let A, B be two flat subsets of S × P (Ω). Define: A ∗ B = {(s, C ∩ C 0 ) | (s, C) ∈ A, and (s, C 0 ) ∈ B}. The next corollary follows immediately from the above definition. Corollary 1. Let φ, ψ be RTCTLP formulae, and Aφ , Aψ be such flat subsets of the parametric state space that s |=ω φ iff ω ∈ Aφ (s) and s |=ω ψ iff ω ∈ Aψ (s) for all s ∈ S. Then s |=ω φ ∧ ψ iff ω ∈ (Aφ ∗ Aψ )(s). It should be noted that in our applications, the ∗ operation is purely symbolic, as we deal with the sets of inequalities only. Example 1. Consider the following sets: Aφ = {(s0 , Ω), (s1 , {ω | ω(t1 ) + 3ω(t2 ) < 5})}, Aψ = {(s1 , {ω | 2ω(t1 ) + 3ω(t3 ) < 4})}, We have Aφ ∗ Aψ = {(s1 , {ω | ω(t1 ) + 3ω(t2 ) < 5 ∧ 2ω(t1 ) + 3ω(t3 ) < 4})}. In the translation of EG≤k and EU ≤k we make use of the bounded backstep operation. This operation is defined on sets of triples (s, A, C), where s is a state, A is a set of linear statements used to track possible constraints on parameters, and C is a set of parameter valuations used to track the allowed values of time step parameters. Parameter Synthesis for Timed Kripke Structures 265 Definition 5. Let D ⊆ S × P (LS) × P (Ω), k ∈ N, and Init be a flat subset of S × P (Ω) such that for each e ∈ D there is f ∈ Init satisfying e|1 = f |1 . Now, (s, A, C) ∈ BackStepk (D, Init) iff: 1. there exists e ∈ D such that e|1 = s, 2. for some A0 ⊆ LS, C 0 ⊆ Ω, and s0 ∈ S there exists (s0 , A0 , C 0 ) ∈ D, such that: (a) the set link(s, s0 ) of time step parameters (treated as linear statements) is nonempty (i.e. there is a transition from s to s0 ), (b) A = [link(s, s0 ) + A0 ]k , (c) C = C 0 ∩ Init(s). While the bounded backstep operation may seem involved, it originates from a natural idea. Let φ be some property and let Init be such a set that s |=ω φ iff ω ∈ Init(s) for each state s. Let D ⊆ S × P (LS) × P (Ω) and (s0 , A0 , C 0 ) ∈ D. A = {[δπn+1 ]k | π0 = s and π1 = s0 } A0 = {[δπn ]k | π0 = s0 } s s0 t1 s |=ω φ iff ω ∈ Init(s) s0 |=ω φ iff ω ∈ Init(s0 ) Assume that C 0 = Init(s0 ), let n ∈ N, and A0 be the set of k–bounded time distance functions for all paths leaving s0 and measuring the distance up to the n–th position. It is easy to see, that BackStepk (D, Init) contains a tuple (s, A, Init(s) ∩ Init(s0 )), where A = [link(s, s0 ) + A0 ]k . The set A consists of k–bounded time distance functions for all paths leaving s, entering s0 in the next step, and measuring the distance up to the (n + 1)–th position. The set Init(s)∩Init(s0 ) contains such parameter valuations ω that s |=ω φ and s0 |=ω φ. Example 2. Consider the sets: C1 = {ω | ω(t1 ) > 2}, C2 = {ω | ω(t2 ) + ω(t3 ) ≤ 4}, D = {(s1 , {6t1 + 8t2 }, C1 ), (s2 , {4t2 + 7t3 , t4 }, C2 )}, and assume that the only transitions involving s1 and s2 are (s1 , t1 , s2 ), (s1 , t2 , s2 ), and let Init = {(s1 , C1 ), (s2 , C2 )}. Let us compute BackStep5 (D, Init). We can see that link(s1 , s2 ) = {t1 , t2 }, link(s1 , s1 ) = link(s2 , s2 ) = link(s2 , s1 ) = ∅. Let A = [{t1 , t2 } + {4t2 + 7t3 , t4 }]5 = {t1 + 4t2 + 6t3 , 5t2 + 6t3 , t1 + t4 , t2 + t4 }, and C = C2 ∩ Init(s1 ) = C2 ∩ C1 = {ω | ω(t1 ) > 2 and ω(t2 ) + ω(t3 ) ≤ 4}. In this case BackStep5 (D, Init) = {(s1 , A, C)}. We say that a sequence of sets H0 , H1 , . . . stabilizes if there exists i ≥ 0 such that Hj = Hi for all j > i, and denote this as limj→∞ Hj = Hi . Let D be a finite subset of S × P (LS) × P (Ω). Notice that if we fix some k ∈ N and Init, then the sequence defined by H0 = D, and Hi+1 = Hi ∪ BackStepk (Hi , Init) stabilizes. This is due to the fact that there is a finite 266 M. Knapik, W. Penczek number of time parameters in a model (therefore a finite number of k-bounded expressions built with respect to [ ]k ), and a finite number of parameter valuation sets in D. Let (s, A, C) ∈ S × P (LS) × P (Ω), ≈ ∈ {≤, <, >, ≥}, and k ∈ N. Denote [(s, A, C)]≈k = (s, [A]≈k ∩C). Intuitively, this encodes a state together with those parameter valuations which satisfy constraints present in [A]≈k (the path length constraints), and in C (the initial constraints). We extend this notion to the space on which BackStep operates, by putting [D]≈k = {[(s, A, C)]≈k | (s, A, C) ∈ D} for any D ⊆ S × P (LS) × P (Ω). Let us move to the first application of BackStepk operation, i.e., the trans- lation of EG≤k . The following example provides some intuitions behind the parametric counterpart of this modality. Example 3. Consider model shown in Fig. 1, where L(s0 ) = L(s1 ) = {p}, and formula EG≤2 p. For the simplicity, the loops on states s2 , s3 are unlabeled. p p t1 s2 s0 s1 t1 s3 t2 Fig. 1: A simple model It is easy to see that s1 |=ω EG≤2 p iff ω(t1 ) > 2 or ω(t2 ) > 2, i.e., using the newly introduced notation, ω ∈ [out(s1 )]>2 . It also holds that s0 |=ω EG≤2 p if ω ∈ [out(s0 )]>2 , but this is not an exhaustive description of all such parameter valuations. Indeed, s0 |=ω EG≤2 p also if 2ω(t1 ) > 2 or ω(t1 ) + ω(t2 ) > 2, i.e., ω ∈ [t1 + out(s1 )]>2 . By a straightforward case-by-case analysis we can check that s0 |=ω EG≤2 p iff ω ∈ [out(s0 )]>2 ∪ [t1 + out(s1 )]>2 . Definition 6. Let A be a flat subset of S × P (Ω) and k ∈ N. Define: G0 (A) = {(s, out(s), A(s)) | there exists e ∈ A such that e|1 = s}, Gj+1 (A) = BackStepk (Gj (A), A). S∞ We define EG ≤k A = F latten( j=0 [Gj (A)]>k ). The F latten operator is used only in order to obtain the result in a less complex form, where for each state s there exists at most one e ∈ EG ≤k A such that e|1 = s. Theorem 1. Let φ be a formula of RTCTLP , and Aφ be such a flat subset of S ×P (Ω) that s |=ω φ iff ω ∈ Aφ (s). For any state s ∈ S, k ∈ N, and a parameter valuation ω we have s |=ω EG≤k φ iff ω ∈ (EG ≤k Aφ )(s). Proof. If s |=ω EG≤k φ, then there exists a path π = (s0 , t0 , s1 , t1 , . . .), such that for some n ∈ N it holds that π0 = s, δπn+1 (ω) > k and δπi (ω) ≤ k for all Parameter Synthesis for Timed Kripke Structures 267 0 ≤ i ≤ n, and πi |=ω φ for all 0 ≤ i ≤ n. n+1 δπ (ω)>k z }| { t0 t1 t2 tn−1 tn tn+1 π = s0 → s1 → s2 → . . . → sn → sn+1 → . . . | {z } n (ω)≤k δπ For each 0 ≤ i ≤ n weThave that πi |=ω φ, therefore Aφ (si ) is well defined for each n 0 ≤ i ≤ n, and ω ∈ i=0 Aφ (si ). It is easy to see that (sn , out(sn ), Aφ (sn )) ∈ tn−1 G0 (Aφ ), and tn ∈ out(sn ). Notice that sn−1 → sn , thus (sn−1 , [link(sn−1 , sn )+ out(sn )]k , Aφ (sn−1 ) ∩ Aφ (sn )) ∈ BackStepk (G0 (Aφ ), Aφ ) = G1 (Aφ ). Again, we have that [tn−1 + tn ]k ∈ [link(sn−1 , sn ) + out(sTnn )]k . After n + 1 such inductive steps we obtain that there is a tupleTn (s0 , A, i=0 Aφ (si )) ∈ Gn (Aφ ) such that [t0 + t1 + . . . + tn ]k ∈ A, and ω ∈ i=0 Aφ (si ). Recall that δπn = t0 + t1 + . . . + tn , and as δπn (ω) > k, we have that [t0T+ t1 + . . . + tn ]k (ω) > k, therefore ω ∈ n [A]>k . TThis means that ω ∈ [A]>k ∩ i=0 Aφ (si ), which in view of the fact that n [(s, A, i=0 Aφ (si ))]>k ∈ [Gn (Aφ )]>k concludes this part of the proof. Now let ω ∈ (EG ≤k Aφ )(s). This means that for some m ∈ N, and em = (sm , Bm ), where sm = s we have that em ∈ [Gm (Aφ )]>k , and ω ∈ Bm . This in turn means that there is a sequence (s0 , A0 , C0 ), (s1 , A1 , C1 ), . . . , (sm , Am , Cm ) such that: 1. Ai = [link(si , si−1 ) + Ai−1 ]k for all 0 < i ≤ m, and A0 = out(s0 ), Ti 2. Ci = j=0 Aφ (sj ) and ω ∈ Ci for all 0 ≤ i ≤ m, 3. (si , Ai , Ci ) ∈ Gi (Aφ ) for all 0 ≤ i ≤ m, 4. [An ]>k ∩ Cm = Bm . From the above points it follows that there exists such a finite sequence π 0 = (sm , tm , sm−1 , tm−1 . . . , s0 , t0 ) that [δπm0 ]k = [tm + tm−1 + . . . + t0 ]k ∈ Am , and [δπm0 ]k (ω) > k. Notice that the latter is equivalent to δπm0 (ω) > k, and that the second point implies that si |=ω φ for all 0 ≤ i ≤ m. The sequence π 0 is a prefix of some infinite path π (due to the totality of the transition relation), such that πi |=ω φ for all 0 ≤ i ≤ m, and δπm (ω) > k. This means that s |=ω EG≤k φ, which concludes the proof. t u Definition 7. Let A, B be two flat subsets of S × P (Ω) and k ∈ N. Denote: H0 (A, B) = {(s, link(s, s0 ), A(s) ∩ B(s0 )) | there exists e ∈ B, e|1 = s0 , and link(s, s0 ) 6= ∅}, Hi+1 (A, B) = BackStepk (Hi (A, B), A). S∞ We define EAU ≤k B = F latten(( i=0 [Hi (A, B)]≤k ) ∪ B). Again, Sj the F latten operator is used only for the convenience, and the sequence ( i=0 Hi )j≥0 is guaranteed to stabilize. 268 M. Knapik, W. Penczek Theorem 2. Let φ, ψ be RTCTLP formulae, and Aφ , Aψ be such flat subsets of parametric state space that s |=ω φ iff ω ∈ Aφ (s) and s |=ω ψ iff ω ∈ Aψ (s), for each state s. For any state s, any k ∈ N, and parameter valuation ω it holds that s |=ω EφU ≤k ψ iff ω ∈ (EAφ U ≤k Aψ )(s). Proof. Assume that s |=ω EφU ≤k ψ. This means that there exists a sequence π = (s0 , t0 , s1 , t1 , . . . , sn , tn , . . .) such that π0 = s, for some n ≥ 0 we have δπn (ω) ≤ k, πn |=ω ψ, and πi |=ω φ for all 0 ≤ i < n. If n = 0, then s |=ω ψ, therefore ω ∈ Aψ (s); now it suffices to notice that Aψ is a (flattened) subset of EAφ U ≤k Aψ . We can therefore assume that n > 0, which means that sn−1 |=ω φ, and sn |=ω ψ, thus ω ∈ Aφ (sn−1 ) ∩ Aψ (sn ). As tn−1 ∈ link(sn−1 , sn ), we obtain that sn−1 , link(sn−1 , sn ), (Aφ (sn−1 )∩Aψ (sn )) ∈ H0 (Aφ , Aψ ). Similarly as in a first part of the proof of Theorem 1 we can now create a sequence (s0 , A0 , C0 ), (s1 , A1 , C1 ), . . . , (sn−1 , An−1 , Cn−1 ) such that for all 0 ≤ i ≤ n − 1: 1. Ai = [link(si , si+1 ) + link(si+1 , si+2 ) + . . . + link(sn−1 , sn )]k , Tn−1 2. Ci = j=i Aφ (sj ) ∩ Aψ (sn ) and ω ∈ Ci , 3. (si , Ai , Ci ) ∈ Hn−i−1 (Aφ , Aψ ). Now let us notice that [t0 + t1 + . . . + tn−1 ]k ∈ A0 , and as δπn (ω) ≤ k, also [t0 + t1 + . . . + tn−1 ]k (ω) ≤ k. This means that ω ∈ [A0 ]≤k ∩ C0 , therefore there is e ∈ [H0 (Aφ , Aψ )]≤k such that e|1 = s0 = s, and ω ∈ e|2 , which concludes the case. Now let us assume that ω ∈ (EAφ U ≤k Aψ )(s). If ω ∈ Aψ (s), then obviously s |=ω ψ and s |=ω EφU ≤k ψ, therefore let us assume that for some m ∈ N we have that e = (sm , Bm ) ∈ [Hm (Aφ ), Aψ ]≤k where sm = s, and ω ∈ Bn . Again, this means that there exist a state s0 such that ω ∈ Aψ (s0 ), and a sequence (s0 , A0 , C0 ), (s1 , A1 , C1 ), . . . , (sm , Am , Cm ) such that: 1. link(si+1 , si ) 6= ∅ for all 0 ≤ i < m, and link(s0 , s0 ) 6= ∅, 2. Ai = [link(si , si−1 ) + link(si−1 , si−2 ) + . . . + link(s0 , s0 )]k for all 0 ≤ i ≤ m, Ti 3. Ci = j=0 Aφ (sj ) ∩ Aψ (s0 ) and ω ∈ Ci for all 0 ≤ i ≤ m, 4. (si , Ai , Ci ) ∈ Hi (Aφ , Aψ ) for all 0 ≤ i ≤ m, 5. [Am ]≤k ∩ Cm = Bm . From the above points we can infer the existence of such a finite sequence π 0 = (sm , tm , sm−1 , tm−1 , . . . , s0 , t0 , s0 , t0 ) (the t0 is an arbitrary time step parameter from out(s0 )) that: 1. ti ∈ link(si , si−1 ) for all 0 < i ≤ m, and t0 ∈ link(s0 , s0 ), 2. π 0 (i) |=ω φ for all 0 ≤ i ≤ m, and π 0 (m + 1) |=ω ψ, 3. δπm0 (ω) ≤ k, as [δπm0 ]k (ω) = [t0 + t1 + . . . + tm ]k (ω) ≤ k. By the virtue of the totality of the transition relation this means that s |=ω EφU ≤k ψ, which concludes the proof. t u Definition 8. Let A be a flat subset of S × P (Ω), and k ∈ N. Denote: Ik (A) = {(s, link(s, s0 ), A(s0 )) | exists e ∈ A s. t. e|1 = s0 and link(s, s0 ) 6= ∅}. We define EX ≤k A = F latten([Ik (A)]≤k ). Parameter Synthesis for Timed Kripke Structures 269 Intuitively, in Ik (A) for each state s we gather its connections with other states s0 and constraints A(s0 ) imposed in s0 . It suffices to ensure that these constraints are consistent with conditions of transition from s to s0 in under k time units. Corollary 2. Let φ be a formula of RTCTLP , let k ∈ N, and let Aφ be such a flat subset of S × P (Ω) that s |=ω φ iff ω ∈ Aφ (s). For any state s and parameter valuation ω we have s |=ω EX ≤k φ iff ω ∈ (EX ≤k Aφ )(s). We have proved that the proposed translation is valid for all nonnegated expres- sion. To complete the theory we show how to deal with negations. Definition 9. Let A be a flat subset of S × P (Ω). We define: ıA = F latten({(s, Ω \ A(s)) | exists e ∈ A such that e|1 = s} ∪{(s, Ω) | there is no e ∈ A such that e|1 = s}). Let us present some intuitions concerning the translation of the negation. Let Aφ characterize the states augmented with parameter valuations under which the φ property holds. The ıAφ set is built by: 1. augmenting any state s represented in Aφ , by those valuations under which φ does not hold (the complement of Aφ (s)), 2. including all the states which are not represented in Aφ together with the full set of parameter valuations. This gives rise to the following corollary. Corollary 3. Let Aφ be such a flat subset of S×P (Ω) that s |=ω φ iff ω ∈ Aφ (s). For any state s and ω ∈ Ω it holds that s |=ω ¬φ iff ω ∈ (ıAφ )(s). 4 Conclusions The method presented in this paper allows for the synthesis of parameter values in timed Kripke structures for properties expressed in RTCTLP logic. To be more precise, for a given property φ the result of synthesis is the set Aφ of constraints on time step parameters. These constraints are expressed as linear inequalities over natural numbers, therefore our method is in fact a translation from the problem of RTCTLP parameter synthesis to a problem stated in the language of linear algebra. If properly implemented, this enables to take advantage of the vast work and available tools from the discrete optimization field. It is rather straightforward to show that for a given RTCTLP formula φ it suffices to consider only the parameter step values which do not exceed the greatest superscript in φ plus 1. While Ω can be limited to a finite set, an enu- merative verification of all possible valuations from this set would soon prove to be intractable. A symbolic model checking approach gives a chance of alleviating these limitations via an efficient representation of statespace and operations on its subsets. We plan to research the possibilities of implementing the presented work using various versions of decision diagrams and SMT-theories. 270 M. Knapik, W. Penczek Acknowledgements Michal Knapik is supported by the Foundation for Polish Science under International PhD Projects in Intelligent Computing. Project fi- nanced from the European Union within the Innovative Economy Operational Programme 2007-2013 and European Regional Development Fund. References 1. Emerson, E.A., Trefler, R.: Parametric quantitative temporal reasoning. In: Proc. of the 14th Symp. on Logic in Computer Science (LICS’99), IEEE Computer Society (July 1999) 336–343 2. Alur, R., Henzinger, T., Vardi, M.: Parametric real-time reasoning. In: Proc. of the 25th Ann. Symp. on Theory of Computing (STOC’93), ACM (1993) 592–601 3. Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett. 102 (May 2007) 208–213 4. Tranouez, L.M., Lime, D., Roux, O.H.: 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., Springer-Verlag (2008) 280–294 5. Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: 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., Springer-Verlag (2001) 189–203 6. Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. T. Petri Nets and Other Models of Concurrency 5 (2012) 141–159 7. Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed au- tomata. In: Proceedings of the 19th international conference on Tools and Algo- rithms for the Construction and Analysis of Systems. TACAS’13, Berlin, Heidelberg, Springer-Verlag (2013) 401–415 8. André, E., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for para- metric timed automata. International Journal of Foundations of Computer Science 20(5) (Oct 2009) 819–836 9. Henzinger, T., Ho, P., Wong-Toi, H.: HyTech: A model checker for hybrid systems. In: Proc. of the 9th Int. Conf. on Computer Aided Verification (CAV’97). Volume 1254 of LNCS., Springer-Verlag (1997) 460–463