The paper shows how bounded model checking can be applied to parameter synthesis for parametric timed automata with continuous 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.
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
property (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 [
Many of model checking tools acquired new capabilities of parametric
verification, e.g. UPPAAL-PMC [
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 [
In this paper we use two kinds of variables, namely parameters P = {p1, . . . , pm}
and clocks X = {x0, . . . , xn}. An expression of the form Pim=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
R≥0n). Additionally, following [
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 [
Let us recall some notions from the theory of parametric timed automata.
Nonparametric timed automata [
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 parametric 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)), – let (q, ω), (q′ , ω′ ) ∈ S. The transition relation →d is defined as follows: • if d ∈ R≥0, then (q, ω) →d (q′ , ω′ ) iff q = q′ and ω′ = ω + d, • if d ∈ A, then (q, ω) →d (q′ , ω′ ) iff q a→,g,r 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 [
Our definition of parametric timed automata slightly differs from the one
presented in [
In non-parametric timed automata theory, the region graph [
To our aims it is convenient to describe regions as sets of valuations satisfying certain guard expressions.
Lemma 1. Let X = {x0, . . . , xn} be a set of clocks, and Z – a region of valuations. There exists a guard gZ = Vi,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)⌋ ,
• 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 characteristic 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 example 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 parameters (treated as natural vectors). Let s = xi − xj ≺ e be a simple guard, and gZ = Vi,j∈{0,...,n},i6=j xi − xj ≺ij bij the characteristic guard of region Z. Then we define:
(Z, C) ;s (Z′ , C′ ) iff Z = Z′ and C′ = C ∩ {υ | bij(≺ij⇒≺)e[v]}. Let g be a guard and s a simple guard, then: (Z, C) g;∧s (Z′ , C′ ) iff for some (Z′ , C′ ) we have (Z, C) ;g (Z′ , C′ ) and (Z′ , C′ ) ;s (Z′ , C′ ).
There is a natural intuition behind the above definition – if (Z, C) ;g (Z′ , C′ )
then (Z′ , C′ ) contains all the pairs (ω, υ) ∈ Z × C such that ω |=υ g. Such an
operation is a counterpart for guard addition from [
Lemma 2. Let (Z, C) ;g (Z′ , C′ ), where g is a guard. Then, the following conditions hold: 1. if (ω, υ) ∈ (Z, C) and ω |=υ g, then (ω, υ) ∈ (Z′ , C′ ), 2. if (ω, υ) ∈ (Z′ , C′ ), then ω |=υ g. 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.
For the induction step, notice that if (Z, C) g;′∧s (Z′ , C′ ) (g′ is a guard, ′ and s a simple guard), then there exists (Z′ , C′ ) such that (Z, C) ;g (Z′ , C′ ) and (Z′ , C′ ) ;s (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 form xi−xj ≺ij bij. If (Z, C) ;g (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.
For the induction step, let us notice that if (Z, C) g;′∧s (Z′ , C′ ), then there ′ exists (Z′ , C′ ) such that (Z, C) ;g (Z′ , C′ ) and (Z′ , C′ ) ;s (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: 1. if (Z, C) ;g (Z′ , C′ ), then Z′ × C′ = Z × C ∩ {(ω, υ) | ω |=υ g}, 2. if ω ∈ Z, υ ∈ C, and ω |=υ g, then (Z, C) ;g (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 representative.
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 [
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)}, – (q, Z, C) →d (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′ ), • if d ∈ A (action transition), then there exists a transition q d→,g,r q′ in A and C′ such that (Z, C) ;g (Z, C′ ) and (Z[r], C′ ) I;(q′ ) (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 (parametric) 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.
Now, if sn−1 →d sn is an action transition (d ∈ A), then there exists a transition qn−1 d→,g,r qn in A, and a subset C′ of Nm, such that (Zn−1, Cn−1) ; g (Zn−1, C′ ), and (Zn−1[r], C′ ) I(;qn) (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}) →τ . . .
Consider a transition (q, Z, C) →d (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 infinite (finite) run in Aυ, where ti = (qi, ωi), and such that if ti →d 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.).
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.
If tn−1 →d 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′ such that (Zn, Cn−1) I(;qn) (Zn, C′ ), υ ∈ C′ , and conclude the case by placing Cn = C′ , and the inductive assumption.
If tn−1 →d tn is an action transition, then there exists a transition in A such that for some guard g and reset r we have qn−1 d→,g,r 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 have that there exist sets C′ , C′ satisfying (Zn−1, Cn−1) ;g (Zn−1, C′ ), υ ∈ C′ , and (Zn−1, C′ ) I(;qn) (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 = s0n, s1n, . . . 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 region 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 restriction of →d to S′ .
Definition 8. Let A be a parametric timed automaton, υ – a parameter valuation, 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
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 [
The non-parametric model checking tool verifies a model (system specification) against a given property (usually in form of a temporal logic formula), producing the answer of simple holds/does not hold type. Its parametric counterpart 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 property is satisfied. The automated synthesis of a complete set of desired parameter valuations is not possible in case of timed automata due to general undecidability 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 sufficient, 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.
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 [
The P REG(A) structure is infinite. In order to represent the infinite runs in a finite substructure we need a notion of loop.
Definition 9. Let ρn = s0, s1, . . . sn be a finite run in P REG(A), and si →d si+1 for all 0 ≤ i < n. If sn = (qn, Zn, Cn) and there exists si = (qi, Zi, Ci), where 0 ≤ i < n such that sn →d 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: sˆi = (qi, Zi, Cn) for i < n (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:
qˆi =
qi for i < n
qj+(n−i)mod(n−j) for i ≥ n.
The presented method can be applied to the verification of a variety of
properties. As the example, in this subsection we present the application of introduced
theory to verification of properties specified in the existential part of
Computation Tree Logic (CTL−X) without the next operator [
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.
Additionally we use the derived modalities: EF α d=ef E(trueU α), AF α = def 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 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.
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 semantics (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 properties 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 [
– 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 ([
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 [
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 implementations [?,?]. 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, respectively, the lower and the upper bound on read/write time. req := true ack := true
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 putData minIO < x1
x2 := 0 putData τ readData τ readData
return s1 [(2,0)] maxIO > 2 minIO ≤ 2
s1 s2 s1 mm[ia(nx2II,O0O.1≤≥)]12 mma[(ix1nI.I1OO,0≥)=]20 mmaix[n(I2IO,O1>)=]10 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 parameter 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.
The theory presented in this paper is to be implemented in Verics model checker
[