=Paper=
{{Paper
|id=None
|storemode=property
|title=Bounded Model Checking for Parametric Timed Automata
|pdfUrl=https://ceur-ws.org/Vol-827/32_MichalKnapik_article.pdf
|volume=Vol-827
|dblpUrl=https://dblp.org/rec/conf/acsd/KnapikP10
}}
==Bounded Model Checking for Parametric Timed Automata==
https://ceur-ws.org/Vol-827/32_MichalKnapik_article.pdf
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