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 xed-point symbolic model checking approach, we introduce special operators which stabilise on the solution. The process of stabilisation is essentially a translation from RTCTLP parameter synthesis problem to a discrete optimization task. We argue that this leads to new opportunities in model checking, including the use of integer programming and related tools.
Introduction
be veri ed. The best moment for the veri cation is the design phase, perhaps even before any prototype is developed. This helps to reduce errors and costs; the found aws can also provide valuable pointers to a designer.
timed, and reactive systems. In this approach, a model for a veri ed system is built (e.g. a Kripke structure or a Petri net), and a property to be checked is speci ed 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 speci cation 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 veri cation has to be repeated.
from a tool that is able to accept an underspeci ed 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 eliminates the needs for guessing and for performing batches of tests for ranges of values.
structures, i.e., Kripke structures where transition is augmented with an additional 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
is however not decidable for even as simple properties as reachability for many
other models, e.g. parametric timed automata (PTA) [
a part of the set of valuations for PTA reachability. The problem of synthesis
of bounded integer valuations for PTA is analysed in [
2
Parameterized Temporal Logics
the power set of a set D. For any sequence x = (x1; : : : ; xn) and 0 i n, let xji = xi be the projection of x on the i{th variable. 2.1
The Syntax of RTCTLP
containing the symbol true. The formulae of RTCTLP are de ned as follows:
and are formulae, then so are EX k , EG k , E U k for k 2 N.
\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
De nition 2. A parametric timed Kripke structure (a model) is a 5-tuple M = (S; s0; T; !; L) where: { S is a nite set of states, { s0 2 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 2 S there exists s0 2 S and t 2 T with (s; t; s0) 2 ! (i.e., the relation is total), { L : S ! 2PV is a valuation function satisfying true 2 L(s) for each s 2 S.
s !t s0 we denote that (s; t; s0) 2 !. The intuitive meaning of s !t s0 is that it takes t time units to reach s0 from s. We de ne in(s), out(s), link(s; s0) as the sets of the labels of the transitions entering s, leaving s, and connecting s with s0, respectively. More formally, in(s) = ft 2 T j s0 !t s for s0 2 Sg, out(s) = ft 2 T j s !t s0 for s0 2 Sg, and link(s; s0) = ft 2 T j s !t s0g.
A function ! : T ! N is called a parameter valuation. The set of all the parameter valuations is denoted by . Consider an in nite sequence = (s0; t0; s1; t1; : : :) such that si 2 S and si !ti si+1 for i 2 N. By i = si we denote the i{th state of . We de ne the time distance function between the positions 0 and j on a sequence as j = Pij=01 ti, and we assume that 0 = 0. If ! is a parameter valuation, then let j (!) = Pij=01 !(ti). A sequence is called an !{path if limj!1 j (!) = 1, or simply a path if ! is evident from the context. De nition 3 (Semantics of RTCTLP). Let M = (S; s0; T; !; L) be a model and s 2 S. Let ; 2 RTCTLP, let ! 2 be a parameter valuation, and k 2 N. M; s j=! 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 j=! is de ned inductively as follows: 1. s j=! p i p 2 L(s), 2. s j=! : i s 6j=! , 3. s j=! ^ i s j=! and s j=! , 4. s j=! EX k i there exists a path s.t. 0 = s; 1 (!) k; and 1 j=! , 5. s j=! EG k i there exists a path such that 0 = s; and for all i 0 if i (!) k; then i j=! , 6. s j=! E U k i there exists a path such that 0 = s and for some i 2
N it holds that i (!) k and i j=! ; and j j=! for all 0 j < i.
The RTCTLP logic slightly di ers from RTCTL presented in [
Translation to Linear Algebra In what follows we x a model M = (S; s0; T; !; L).
linear statements ) of the form c1t1 + : : : + cntn, where ti 2 T are time step parameters, ci 2 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 LST ; we omit the T subscript if it is implicitly understood. In this paper we consider only nite subsets of LST .
Let = c1t1 + : : : + cntn, and let ! 2 . We de ne the application of ! to as [!] = c1!(t1) + : : : + cn!(tn). We also de ne the k-bounding operation for k 2 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.
then for any k 2 N the inequalities k and [ ]k k have the same sets of solutions. This can be easily veri ed on a case-by-case basis, by noticing that if a given coe cient ci of exceeds k + 1, then any nonzero value of ti makes k true for 2 f>; g, while 2 f ; <g means that only zero can be substituted for ti.
of linear statements over the nite parameter set T , obtained by means of kbounding with respect to some xed natural k, is nite. We extend the [ ]k operation to subsets A LS as follows: [A]k = f[ ]k j 2 Ag: Let A; B LS, then we de ne A + B = f + j 2 A and 2 Bg:
as follows: [A] k = [ f! j [!]
kg: As to give an example, let A = ft1 + 2t2; t3g, then [A]<4 consists of all the valuations ! such that !(t1) + 2!(t2) < 4, or !(t3) < 4.
called the parametric states. As to give an example, consider A LS such that A = f2t1 + 3t2; 2t1 + 3t4g. The pair of form (s0; [A] 10) is a parametric state.
(s; A) 2 F latten(B) i A = [fC j (s; C) 2 Bg; A 6= ;: To make this de nition clearer, consider an example where B = f(s0; C1); (s0; C2); (s1; C3); (s1; C4); (s2; C5)g. In this case F latten(B) = f(s0; C1 [ C2); (s1; C3 [ C4); (s2; C5)g.
If F latten(B) = B, then the set B is called at. If B is at, then by B(s) we denote the parameter selector, that is B(s) = C i (s; C) 2 B. The parameter selector is a well de ned partial function on S.
The translation Our aim is to nd all the valuations under which a given formula 2 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 j=! i ! 2 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 nite union of solution sets of a nite number of linear (integer) inequalities. This means that A (s) has a nite 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 2 PV, then Ap = f(s; ) j p 2 L(s)g is the set of such pairs (s; ) that p 2 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 at.
In the algorithm we use several new operators that are counterparts of propositional connectives and RTCTLP modalities:
k { a counterpart of EX k, 43.. ooppeerraattoorr EE GX k { a counterpart of EG k. 5. operator E U k { related to EU k.
De nition 4. Let A; B be two at subsets of S P ( ). De ne: A
B = f(s; C \ C0) j (s; C) 2 A; and (s; C0) 2 Bg:
^
Corollary 1. Let ; be RTCTLP formulae, and A ; A be such at subsets of the parametric state space that s j=! i ! 2 A (s) and s j=! i ! 2 A (s) for all s 2 S. Then s j=! i ! 2 (A A )(s). operation is purely symbolic,
A A = f(s0; ); (s1; f! j !(t1) + 3!(t2) < 5g)g; = f(s1; f! j 2!(t1) + 3!(t3) < 4g)g;
A
= f(s1; f! j !(t1) + 3!(t2) < 5 ^ 2!(t1) + 3!(t3) < 4g)g.
operation. This operation is de ned on sets of triples (s; A; C), where s is a state,
S P ( ) such that for each e 2 D there is f 2 Init satisfying ej1 = f j1. Now, (s; A; C) 2 BackStepk(D; Init) i : 1. there exists e 2 D such that ej1 = s, 2. for some A0 LS, C0 , and s0 2 S there exists (s0; A0; C0) 2 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 = C0 \ Init(s).
natural idea. Let be some property and let Init be such a set that s j=! i ! 2 Init(s) for each state s. Let D S P (LS) P ( ) and (s0; A0; C0) 2 D.
A = f[ n+1]k j 0 = s and 1 = s0g
A0 = f[ n]k j 0 = s0g s t1
s0 s j=! i ! 2 Init(s) s0 j=! i ! 2 Init(s0) Assume that C0 = Init(s0), let n 2 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 j=! and s0 j=! .
C1 = f! j !(t1) > 2g; C2 = f! j !(t2) + !(t3) and assume that the only transitions involving s1 and s2 are (s1; t1; s2); (s1; t2; s2), and let Init = f(s1; C1); (s2; C2)g: Let us compute BackStep5(D; Init). We can see that link(s1; s2) = ft1; t2g, link(s1; s1) = link(s2; s2) = link(s2; s1) = ;. Let A = [ft1; t2g + f4t2 + 7t3; t4g]5 = ft1 + 4t2 + 6t3; 5t2 + 6t3; t1 + t4; t2 + t4g, and C = C2 \ Init(s1) = C2 \ C1 = f! j !(t1) > 2 and !(t2) + !(t3) 4g. In this case BackStep5(D; Init) = f(s1; A; C)g.
that Hj = Hi for all j > i, and denote this as limj!1Hj = Hi.
k 2 N and Init, then the sequence de ned by H0 = D, and Hi+1 = Hi [
number of time parameters in a model (therefore a nite number of k-bounded expressions built with respect to [ ]k), and a nite number of parameter valuation sets in D.
Let (s; A; C) 2 S P (LS) P ( ), 2 f ; <; >; g, and k 2 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 = f[(s; A; C)] k j (s; A; C) 2 Dg for any D S P (LS) P ( ).
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) = fpg, and formula EG 2p. For the simplicity, the loops on states s2; s3 are unlabeled. p s0 t1 p s1 t1 t2 s2 s3 It is easy to see that s1 j=! EG 2p i !(t1) > 2 or !(t2) > 2, i.e., using the newly introduced notation, ! 2 [out(s1)]>2. It also holds that s0 j=! EG 2p if ! 2 [out(s0)]>2, but this is not an exhaustive description of all such parameter valuations. Indeed, s0 j=! EG 2p also if 2!(t1) > 2 or !(t1) + !(t2) > 2, i.e., ! 2 [t1 + out(s1)]>2. By a straightforward case-by-case analysis we can check that s0 j=! EG 2p i ! 2 [out(s0)]>2 [ [t1 + out(s1)]>2.
De nition 6. Let A be a at subset of S
P ( ) and k 2 N. De ne:
G0(A) = f(s; out(s); A(s)) j there exists e 2 A such that ej1 = sg; Gj+1(A) = BackStepk(Gj (A); A): We de ne E G
kA = F latten(Sj1=0[Gj (A)]>k):
form, where for each state s there exists at most one e 2 E G kA such that ej1 = s.
Theorem 1. Let be a formula of RTCTLP, and A be such a at subset of S P ( ) that s j=! i ! 2 A (s): For any state s 2 S, k 2 N, and a parameter valuation ! we have s j=! EG k i ! 2 (E G kA )(s).
Proof. If s j=! EG k , then there exists a path = (s0; t0; s1; t1; : : :), such that for some n 2 N it holds that 0 = s, n+1(!) > k and i (!) k for all n, and i j=! for all 0 i For each 0 i n we have that i j=! , therefore A (si) is well de ned for each 0 i n, and ! 2 Tin=0 A (si). It is easy to see that (sn; out(sn); A (sn)) 2 G0(A ), and tn 2 out(sn). Notice that sn 1 tn!1 sn, thus (sn 1; [link(sn 1; sn)+ out(sn)]k, A (sn 1) \ A (sn)) 2 BackStepk(G0(A ); A ) = G1(A ). Again, we have that [tn 1 + tn]k 2 [link(sn 1; sn) + out(sn)]k. After n + 1 such inductive steps we obtain that there is a tuple (s0; A; Tn i=0 A (si)) 2 Gn(A ) such that [t0 + t1 + : : : + tn]k 2 A, and ! 2 Tn
i=0 A (si). Recall that n = t0 + t1 + : : : + tn, [A]>k. Thni(s!m)e>anks,thwaet h!a2ve[At h]>akt \[t0T+in=0t1A+(:s:i):,+wthnic]kh(!in) v>iewk,ofthtehreeffoarcet t!ha2t and as [(s; A; Tin=0 A (si))]>k 2 [Gn(A )]>k concludes this part of the proof.
Now let ! 2 (EG kA )(s). This means that for some m 2 N, and em = (sm; Bm), where sm = s we have that em 2 [Gm(A )]>k, and ! 2 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 2. Ci = Tij=0 A (sj) and ! 2 Ci for all 0 3. (si; Ai; Ci) 2 Gi(A ) for all 0 i m, 4. [An]>k \ Cm = Bm. i m, and A0 = out(s0), m, From the above points it follows that there exists such a nite sequence 0 = (sm; tm; sm 1; tm 1 : : : ; s0; t0) that [ m0 ]k = [tm + tm 1 + : : : + t0]k 2 Am, and [ m0 ]k(!) > k. Notice that the latter is equivalent to m0 (!) > k, and that the second point implies that si j=! for all 0 i m. The sequence 0 is a pre x of some in nite path (due to the totality of the transition relation), such that i j=! for all 0 i m, and m(!) > k. This means that s j=! EG k , which concludes the proof. tu De nition 7. Let A; B be two at subsets of S P ( ) and k 2 N. Denote: H0(A; B) = f(s; link(s; s0); A(s) \ B(s0)) j there exists e 2 B; ej1 = s0; and link(s; s0) 6= ;g;
Hi+1(A; B) = BackStepk(Hi(A; B); A): We de ne EAU kB = F latten((Si1=0[Hi(A; B)] k) [ B):
(Sij=0 Hi)j 0 is guaranteed to stabilize. Theorem 2. Let ; be RTCTLP formulae, and A ; A be such at subsets of parametric state space that s j=! i ! 2 A (s) and s j=! i ! 2 A (s), for each state s. For any state s, any k 2 N, and parameter valuation ! it holds that s j=! E U k i ! 2 (EA U kA )(s).
Proof. Assume that s j=! 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 j=! , and i j=! for all 0 i < n. If n = 0, then s j=! , therefore ! 2 A (s); now it su ces to notice that A is a ( attened) subset of EA U kA . We can therefore assume that n > 0, which means that sn 1 j=! , and sn j=! , thus ! 2 A (sn 1) \ A (sn). As tn 1 2 link(sn 1; sn), we obtain that sn 1; link(sn 1; sn); (A (sn 1)\A (sn)) 2 H0(A ; A ). Similarly as in a rst 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, 2. Ci = Tn
j=i1 A (sj) \ A (sn) and ! 2 Ci, 3. (si; Ai; Ci) 2 Hn i 1(A ; A ).
Now let us notice that [t0 + t1 + : : : + tn 1]k 2 A0, and as n(!) k, also [t0 + t1 + : : : + tn 1]k(!) k. This means that ! 2 [A0] k \ C0, therefore there is e 2 [H0(A ; A )] k such that ej1 = s0 = s, and ! 2 ej2, which concludes the case.
Now let us assume that ! 2 (EA U kA )(s). If ! 2 A (s), then obviously s j=! and s j=! E U k , therefore let us assume that for some m 2 N we have that e = (sm; Bm) 2 [Hm(A ); A ] k where sm = s, and ! 2 Bn. Again, this means that there exist a state s0 such that ! 2 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 3. Ci = Tij=0 A (sj) \ A (s0) and ! 2 Ci for all 0 i m, 4. (si; Ai; Ci) 2 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 nite sequence 0 = (sm; tm; sm 1; tm 1; : : : ; s0; t0; s0; t0) (the t0 is an arbitrary time step parameter from out(s0)) that: i m, 1. ti 2 link(si; si 1) for all 0 < i m, and t0 2 link(s0; s0), 2. 0(i) j=! for all 0 i m, and 0(m + 1) j=! , 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 j=! E U k , which concludes the proof. tu De nition 8. Let A be a at subset of S P ( ), and k 2 N. Denote:
Ik(A) = f(s; link(s; s0); A(s0)) j exists e 2 A s: t: ej1 = s0 and link(s; s0) 6= ;g: We de ne EX kA = F latten([Ik(A)] k):
s0 and constraints A(s0) imposed in s0. It su ces to ensure that these constraints are consistent with conditions of transition from s to s0 in under k time units.
at subset of S P ( ) that s j=! i ! 2 A (s). For any state s and parameter valuation ! we have s j=! EX k i ! 2 (E X kA )(s).
De nition 9. Let A be a at subset of S P ( ). We de ne: {A = F latten(f(s; n A(s)) j exists e 2 A such that ej1 = sg [f(s; ) j there is no e 2 A such that ej1 = sg):
does not hold (the complement of A (s)),
Corollary 3. Let A be such a at subset of S P ( ) that s j=! For any state s and ! 2 it holds that s j=! : i ! 2 ({A )(s). i ! 2 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 eld.
It is rather straightforward to show that for a given RTCTLP formula it su ces to consider only the parameter step values which do not exceed the greatest superscript in plus 1. While can be limited to a nite set, an enumerative veri cation 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 e cient 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.
nanced from the European Union within the Innovative Economy Operational