Fundamenta Informaticae XX (2007) 1–28
1
IOS Press
Bounded Model Checking for the ExistentialFragment of TCTL
−
G
and Diagonal Timed Automata
∗
Bo˙zena Wo´zna
†‡
and Andrzej Zbrzezny
Institute of Mathematics and Computer Science, Jan Długosz University Al. Armii Krajowej 13/15, 42200 Cze¸stochowa, Poland
{
b.wozna,a.zbrzezny
}
@ajd.czest.pl
Abstract.
Bounded Model Checking (BMC) is one of the well known SAT based symbolic modelchecking techniques. It consists in searching for a counterexample of a particular length, and generating a propositional formula that is satisﬁable iff such a counterexample exists. The BMC methodis feasible for the various classes of temporal logic; in particular it is feasible for TECTL (the existential fragment of Time Computation Tree Logic) and Diagonalfree Timed Automata. The maincontribution of the paper is to show that the concept of Bounded Model Checking can be extendedto deal with TECTL
−
G
properties of Diagonal Timed Automata. We have implemented our newBMC algorithm, and we present preliminary experimental results, which demonstrate the efﬁciencyof the method.
1. Introduction
Model checking
is a veriﬁcation technique that was srcinally developed for (untimed) temporal logics[8]. Its main idea is to represent a ﬁnite state system, often deriving from a hardware or software design,as a labelled transition system (model), to represent a speciﬁcation (property) by a modal formula, andto check automatically whether the formula holds in the model.Over the past few years, the interest in automated veriﬁcation has been moved towards concurrentrealtime systems, and now veriﬁcation of such systems is an active area of research. Various classes of models for real time systems have been proposed in the literature, but Timed Automata [2] and Timed
∗
The authors acknowledge support from the research grant No. 3T11C01128
†
The research presented here was mainly conducted while B. Wo´zna was supported by EPSRC (grant GR/S49353).
‡
Address for correspondence: Institute of Mathematics and Computer Science, Jan Długosz University, Al. Armii Krajowej13/15, 42200 Cze¸stochowa, Poland
2
B. Wo´ zna and A. Zbrzezny/BMC for
TECTL
−
G
and Diagonal Timed Automata
Petri Nets [20] are the best known ones. The properties to be veriﬁed are usually expressed eitherin standard temporal logics like LTL [8] and CTL [13], or in their timed versions like MITL [3] andTCTL [1]. In the paper we have decided to consider a restricted version of TCTL, since the modelchecking problem for branching time logics is decidable and PSPACEcomplete in contrary to the modelchecking problem for MITL that is decidable but EXPSPACEcomplete [28].The practical applicability of the model checking method is strongly restricted by socalled the
stateexplosion problem
. Therefore, different reduction techniques were proposed to minimise models. Themajor methods include application of partial order reductions [9, 17, 22, 23, 32], symmetry reductions[14], abstraction techniques [10, 11], BDDbased symbolic storage methods [7, 18], and SATrelatedalgorithms [5, 19, 21, 30, 25, 26, 27, 35, 34].Bounded model checking (BMC) is one of the SATbased (satisﬁability checking) methods, and itwas introduced as a technique complementary to the BDDbased symbolic model checking for LTL[5]. The main idea of BMC is to search for an execution (or a set of executions) of the system of somelength
k
that constitutes a counterexample for a tested property. If no counterexample of length
k
canbe found, then
k
is increased by one. The efﬁciency of this method is based upon the observation thatif a system is faulty, then often examining only a (small) fragment of its state space is sufﬁcient forﬁnding an error. Obviously, when testing large models and complex formulae the efﬁciency of the BMCmethod is dependent on the speed of the chosen SAT solver, with which the test is carried out. As SATcheckers have progressively become more effective, the efﬁciency of BMC has improved, an observationexperimentally demonstrated in, among others, [5, 26, 27].In order to represent and verify real time systems it is convenient to have expressive and easytousemodels. Timed automata with diagonal constraints (or Diagonal Timed Automata [31]) are sufﬁcientlyexpressive to describe the essential aspects of timedependent reallife problems in a variety of application domains; in particular, they are very useful for modelling scheduling problems [15]. It is known thatdiagonal constraints can be eliminated from diagonal timed automata, and that they do not add expressivepower to diagonalfree timed automata [4]. However, a construction of diagonalfree timed automatonfor a given diagonal timed automaton leads to an exponential (in the number of diagonal constraints)blowup of the number of states of the automaton, and this blowup is unavoidable. Therefore, in thepresent paper we deal with diagonal timed automata.The main contribution of the paper consists in showing that the concept of Bounded Model Checkingcan be extended to deal with TECTL
−
G
(the existential fragment ofTCTLwithout the modality standingfor “
always in the future within an interval
”) properties of Diagonal Timed Automata. In particular, weshow that the discretisation method [37] can be applied to model check an arbitrary TECTL
−
G
formulaover Diagonal Timed Automata. Moreover, we have implemented the new BMC algorithm, and weprovide some preliminary experimental results that seem to be promising.The rest of the paper is organised as follows. In Section 2 we brieﬂy introduce diagonal timed automata and a model for them. In Section 3 we give a syntax and semantics for TCTL
−
G
and its subsets.Section 4 contains the basic deﬁnitions and notations that are used in Section 5 to deﬁne a translationof the model checking problem for TCTL
−
G
to the model checking problem of CTL
y
−
G
. In Section6 we present a discretisation technique that is a base for our implementation of the BMC method forTECTL
−
G
, deﬁned in Section 7. In Section 8 we provide some preliminary experimental results fora modiﬁed Fischer mutual exclusion protocol, and in Section 9 we show how to tailor the BMC technique from Section 7 to a specially chosen subclass of TECTL
−
G
formulae. The last section containsa discussion of related work and ﬁnal remarks.
B. Wo´ zna and A. Zbrzezny/BMC for
TECTL
−
G
and Diagonal Timed Automata
3
2. Diagonal Timed Automata
To deﬁne diagonal time automata formally we need to say what type of clock constraints are allowed asguards and invariants. For a ﬁnite set of real variables
X
, called
clocks
, and a set of natural numbers
N
=
{
0
,
1
,...
}
, we deﬁne the set
C
(
X
)
of
clock constraints
over
X
by the following grammar:
cc
::=
true

x
∼
c

x
−
y
∼
c

cc
∧
cc
where
x, y
∈
X
,
c
∈
N
and
∼∈ {
<,
≤
,
=
, >,
≥}
.A
clock valuation
v
is atotal function from
X
into the set of nonnegative real numbers
R
.
R
X
denotesthe set of all clock valuations. For a clock constraint
cc
∈
C
(
X
)
,
cc
denotes the set of all clock valuations that satisfy
cc
. The clock valuation assigning the value
0
to all clocks in
X
is denoted by
v
0
.For
v
∈
R
X
and
δ
∈
R
, the clock valuation
v
+
δ
assigns the value
v
(
x
) +
δ
to each clock
x
∈
X
. For
v
∈
R
X
and
Y
⊆
X
,
v
[
Y
]
denotes the clock valuation that assigns the value
0
to each clock in
Y
andleaves the values of the other clocks unchanged.
Deﬁnition 2.1. (Diagonal Timed Automaton)
Let
PV
be a set of propositional variables. A
diagonal timed automaton
(for short a
timed automaton
) isa tuple
A
= (Σ
,L,l
0
,X,
I
,R,
V
)
, where
Σ
is a nonempty ﬁnite set of actions,
L
is a nonempty ﬁnite setof locations,
l
0
∈
L
is an initial location,
V
:
L
→
2
PV
is a valuation function assigning to each locationa set of atomic propositions true in that location,
X
is a ﬁnite set of clocks,
I
:
L
→
C
(
X
)
is a stateinvariant function, and
R
⊆
L
×
Σ
×
C
(
X
)
×
2
X
×
L
is a transition relation.An element
(
l, σ,
cc
, Y, l
)
∈
R
represents a transition from the location
l
to the location
l
labelledwith the action
σ
. The invariant condition allows the automaton to stay at the location
l
as long only asthe constraint
I
(
l
)
is satisﬁed. The guard
cc
has to be satisﬁed to enable the transition. The transitionresets all clocks in the set
Y
to the value
0
.The semantics of a timed automaton
A
is deﬁned by associating to it a
dense model
as deﬁned below.
Deﬁnition 2.2. (Dense Model)
Let
A
= (Σ
,L,l
0
,X,
I
,R,
V
)
be a timed automaton. A
dense model
for
A
is a tuple
G
(
A
) = (Σ
∪
R
,Q,q
0
,
V
,
→
)
, where
Σ
∪
R
is a set of labels,
Q
=
L
×
R
X
is a set of states,
q
0
= (
l
0
,v
0
)
is an initialstate,
V
:
Q
→
2
PV
is a valuation function such that
V
((
l,v
)) =
V
(
l
)
, and
→ ⊆
Q
×
(Σ
∪
R
)
×
Q
is atransition relation of
G
(
A
)
deﬁned by:
•
Time transitions:
(
l,v
)
δ
→
(
l,v
+
δ
)
iff
(
∀
0
≤
δ
≤
δ
)
v
+
δ
∈
I
(
l
)
•
Action transitions:
(
l,v
)
σ
→
(
l
,v
)
iff
(
∃
cc
∈
C
(
X
))(
∃
Y
⊆
X
)
such that
v
=
v
[
Y
]
,
(
l, σ,
cc
,
Y, l
)
∈
R
,
v
∈
cc
, and
v
∈
I
(
l
)
.Intuitively, a time transition does not change a location, but describes an equal increase in the value of all the clocks, provided that the new clock valuations still satisfy all the location invariants. An actiontransition corresponds to an action performed by the automaton under consideration. Following this, itslocation changes accordingly, and all the clocks that are associated with the action are set to zero (i.e.,the ones which belong to the set
Y
⊆
X
). Obviously, the action can be performed only if the underlingenabling condition is satisﬁed.
4
B. Wo´ zna and A. Zbrzezny/BMC for
TECTL
−
G
and Diagonal Timed Automata
The below lemma shows that for the considered set of clock constraints
C
(
X
)
, in the semantics of timed automata the condition of a time transition
(
l,v
)
δ
→
(
l,v
+
δ
)
can be replaced by the following:
v
∈
I
(
l
)
and
v
+
δ
∈
I
(
l
)
.
Lemma 2.1.
Let
cc
∈
C
(
X
)
,
v
∈
R
X
, and
δ
∈
R
. If
v
∈
cc
and
v
+
δ
∈
cc
, then for each
(0
≤
δ
≤
δ
)
v
+
δ
∈
cc
.
Proof:
Straightforward by induction on clock constraints.
For
(
l,v
)
∈
Q
, let
(
l,v
) +
δ
denote
(
l,v
+
δ
)
. A
q
0
run
ρ
of
A
is a sequence of states:
q
0
δ
0
→
q
0
+
δ
0
σ
0
→
q
1
δ
1
→
q
1
+
δ
1
σ
1
→
q
2
δ
2
→
...
,where
q
i
∈
Q
,
σ
i
∈
Σ
and
δ
i
∈
R
+
for each
i
∈
N
. In other words, a run is an inﬁnite sequence of statessuch that action transitions are taken inﬁnitely often and time transitions are aggregated. Notice that thesemantics does not permit to perform two consecutive action transitions, that is, between each two actiontransitions some time must pass. This is a convenient way of representing a series of events to be takenin a continuous time.Given a run
ρ
=
q
0
δ
0
→
q
0
+
δ
0
σ
0
→
q
1
δ
1
→
q
1
+
δ
1
σ
1
→
q
2
δ
2
→
...
, we say that a run
ρ
=
q
0
δ
0
→
q
0
+
δ
0
σ
0
→
q
1
δ
1
→
q
1
+
δ
1
σ
1
→
q
2
δ
2
→
...
is a
sufﬁx
of
ρ
if there exists
i
∈
N
such that
q
0
=
q
i
and
σ
j
=
σ
i
+
j
and
δ
j
=
δ
i
+
j
for each
j
∈
N
.In line with much of the literature of the real life systems we make the assumption that a systemunder consideration runs continuously without termination. This requirement is normally expressed bydistinguishing between
discrete progress
and
time progress
. Under discrete progress we allow for actiontransitions to happen inﬁnitely often, that is, no state occurs without action successors. Under timeprogress one assumes that time may pass without an upper bound; this is usually formalised by thenotion of
nonzeno
runs.Formally, an inﬁnite run
ρ
is said to be
nonzeno
iff
Σ
i
∈
N
δ
i
is unbounded. An inﬁnite run
ρ
issaid to be
zeno
iff
Σ
i
∈
N
δ
i
is bounded by some real value. As an example, consider the automatonshown in Figure 1. Its
q
0
run
(
q
0
,
0)
1
→
(
q
0
,
1)
a
→
(
q
0
,
1)
0
.
5
→
(
q
0
,
1
.
5)
a
→
(
q
0
,
1
.
5)
0
.
25
→
(
q
0
,
1
.
75)
a
→
(
q
0
,
1
.
75)
0
.
125
→
(
q
0
,
1
.
875)
a
→
(
q
0
,
1
.
875)
0
.
0625
→
...
is zeno. On the other hand the following
q
0
run
(
q
0
,
0)
1
→
(
q
0
,
1)
b
→
(
q
1
,
1)
1
→
(
q
1
,
2)
c
→
(
q
1
,
0)
1
→
(
q
1
,
1)
c
→
(
q
1
,
0)
1
→
(
q
1
,
1)
c
→
...
is nonzeno.
q
0
q
1
bac,
x
:= 0
x
:= 0
x
≤
2
x
≤
2
Figure 1. An example of nontime progressive timed automaton.
We say that
A
is
timeprogressive
iff all its
q
0
runs are nonzeno. For easiness of presentation, weconsider only timeprogressive timed automata; note that timeprogressiveness can be checked as in[31].
B. Wo´ zna and A. Zbrzezny/BMC for
TECTL
−
G
and Diagonal Timed Automata
5
3. Time Computation Tree Logic without
G
In this section, we formally present a syntax and semantics of TCTL
−
G
, a fragment of Time Computation Tree Logic (TCTL) [1] that does not include the modality for “always in the future within someinterval”.
Syntax.
Let
PV
be a set of propositional variables containing the symbol
(denoting the constant“true”), and
I
an interval in
R
with integer bounds of the form
[
n,n
]
,
[
n,n
)
,
(
n,n
]
,
(
n,n
)
,
(
n,
∞
)
,and
[
n,
∞
)
, for
n,n
∈
N
. For
p
∈ PV
, the set of TCTL
−
G
formulae is deﬁned by the followinggrammar:
ϕ
:=
p
 ¬
p

ϕ
∧
ϕ

ϕ
∨
ϕ

E(
ϕ
U
I
ϕ
)

A(
ϕ
U
I
ϕ
)
The other basic operators are deﬁned as usual:
⊥
def
=
¬
,
α
⇒
β
def
=
¬
α
∨
β
,
α
⇔
β
def
= (
α
⇒
β
)
∧
(
β
⇒
α
)
,
EF
I
α
def
= E(
U
I
α
)
,
AF
I
α
def
= A(
U
I
α
)
.TECTL
−
G
is a fragment of TCTL
−
G
such that the temporal formulae are restricted to the Booleancombination of
E(
α
U
I
β
)
only. Similarly, TACTL
−
G
is a fragment of TCTL
−
G
such that the temporalformulae are restricted to the Boolean combination of
A(
α
U
I
β
)
only.
Semantics.
Let
A
= (Σ
,L,l
0
,X,
I
,R,
V
)
be a timed automaton,
G
(
A
) = (Σ
∪
R
,Q,q
0
,
V
,
→
)
a densemodel for
A
,
ρ
=
q
0
δ
0
→
q
0
+
δ
0
σ
0
→
q
1
δ
1
→
q
1
+
δ
1
σ
1
→
q
2
δ
2
→
...
a run of
A
such that
q
i
∈
Q
and
δ
i
∈
R
+
for all
i
∈
N
, and
f
A
(
q
0
)
denote the set of all such
q
0
runs that are sufﬁxes of the
q
0
runs. In order todeﬁne a satisfaction relation for TCTL
−
G
, we deﬁne the notion of a
dense path
π
ρ
corresponding to run
ρ
. This can be done in an unique way because of the assumption that
δ
i
∈
R
+
. First, let
idx
(
ρ,r
)
bethe greatest
i
∈
N
such that
Σ
i
−
1
j
=0
δ
j
≤
r
. Notice that for
i
= 0
we let
Σ
i
−
1
j
=0
δ
j
= 0
. So, for
r
≤
δ
0
,
idx
(
ρ,r
) = 0
. Now,
a dense path
π
ρ
corresponding to
ρ
is a mapping from
R
to the set of states
Q
suchthat
π
ρ
(
r
) =
q
i
+
r
−
Σ
i
−
1
j
=0
δ
j
where
i
=
idx
(
ρ,r
)
.
Deﬁnition 3.1. (Satisfaction)
Let
G
(
A
) = (Σ
∪
R
,Q,q
0
,
V
,
→
)
be a
dense model
,
q
a state, and
α
,
β
TCTL
−
G
formulae. Thesatisfaction relation

=
, which indicates truth of a formula in the dense model
G
(
A
)
at state
q
, is deﬁnedinductively as follows:
G
(
A
)
,q

=
p
iff
p
∈
V
(
q
)
,
G
(
A
)
,q

=
α
∨
β
iff
G
(
A
)
,q

=
α
or
G
(
A
)
,q

=
β,
G
(
A
)
,q

=
¬
p
iff
p
∈
V
(
q
)
,
G
(
A
)
,q

=
α
∧
β
iff
G
(
A
)
,q

=
α
and
G
(
A
)
,q

=
β,
G
(
A
)
,q

= E(
α
U
I
β
)
iff
(
∃
ρ
∈
f
A
(
q
))(
∃
r
∈
I
)[
G
(
A
)
,π
ρ
(
r
)

=
β
and (
∀
r
< r
)
G
(
A
)
,π
ρ
(
r
)

=
α
]
,
G
(
A
)
,q

= A(
α
U
I
β
)
iff
(
∀
ρ
∈
f
A
(
q
))(
∃
r
∈
I
)[
G
(
A
)
,π
ρ
(
r
)

=
β
and (
∀
r
< r
)
G
(
A
)
,π
ρ
(
r
)

=
α
]
.
We end the section by deﬁning the notion of validity in a dense model and deﬁning formally themodel checking problem.A TCTL
−
G
formula
ϕ
is
valid in a dense model
G
(
A
)
(denoted by
G
(
A
)

=
ϕ
) iff
G
(
A
)
,q
0

=
ϕ
,i.e.
ϕ
is true at the initial state of the dense model
G
(
A
)
; checking validity for given
G
(
A
)
and
ϕ
is calledthe
model checking problem
.