=Paper=
{{Paper
|id=Vol-1698/CS&P2016_04_Zbrzezny&Zbrzezny_Simple-Bounded-MTL-Model-Checking-for-Discrete-Timed-Automata
|storemode=property
|title=Simple Bounded MTL Model Checking for Discrete Timed Automata (extended abstract)
|pdfUrl=https://ceur-ws.org/Vol-1698/CS&P2016_04_Zbrzezny&Zbrzezny_Simple-Bounded-MTL-Model-Checking-for-Discrete-Timed-Automata.pdf
|volume=Vol-1698
|authors=Agnieszka Zbrzezny,Andrzej Zbrzezny
|dblpUrl=https://dblp.org/rec/conf/csp/ZbrzeznyZ16
}}
==Simple Bounded MTL Model Checking for Discrete Timed Automata (extended abstract)==
https://ceur-ws.org/Vol-1698/CS&P2016_04_Zbrzezny&Zbrzezny_Simple-Bounded-MTL-Model-Checking-for-Discrete-Timed-Automata.pdf
Simple Bounded MTL Model Checking for
Discrete Timed Automata
(Extended abstract) ?
Agnieszka M. Zbrzezny and Andrzej Zbrzezny
IMCS, Jan Długosz University. Al. Armii Krajowej 13/15, 42-200 Czȩstochowa, Poland.
{agnieszka.zbrzezny,a.zbrzezny}@ajd.czest.pl
Abstract. We present a new translation of Metric Temporal Logic to the Lin-
ear Temporal Logic with a new set of the atomic propositions. We investigate a
SAT-based bounded model checking method for Metric Temporal Logic that is
interpreted over linear discrete infinite time models generated by discrete timed
automata. We show how to implement the bounded model checking technique
for Linear Temporal Logic with a new set of the atomic propositions and discrete
timed automata, and as a case study we apply the technique in the analysis of the
Timed Generic Pipeline Paradigm modelled by a network of discrete timed au-
tomata. We also present a comparison of the two translations of Metric Temporal
Logic on common instances that can be scaled up to for performance evaluation.
The theoretical description is supported by the experimental results that demon-
strate the efficiency of the method.
1 Introduction
Bounded model checking [2, 3, 5] (BMC) is one of the symbolic model checking tech-
nique designed for finding witnesses for existential properties or counterexamples for
universal properties. Its main idea is to consider a model reduced to a specific depth.
The method works by mapping a bounded model checking problem to the satisfiability
problem (SAT). For metric temporal logic (MTL) [4] and discrete time automata [1]
the BMC method can by described as follows: given a model M for a discrete timed
automaton , an MTL formula ϕ, and a bound k, a model checker creates a propositional
formula [M, ϕ]k that is satisfiable if and only if the formula ϕ is true in the model M.
The novelty of our paper lies in :
1. defining a translation of the existential model checking problem for MTL to the ex-
istential model checking problem for linear temporal logic with additional propo-
sitional variables qI . This logic is denoted by LTLq ;
2. defining bounded sematics for LTLq and defining the BMC algorithm;
3. implementing the new method.
The translation from MTL to LTLq requires neither new clocks nor new transitions,
whereas the translation to HLTL [7] requires as many new clocks as there are inter-
vals in a given formula. It also requires an exponential number of resetting transitions.
?
Partly supported by National Science Centre under the grant No. 2014/15/N/ST6/05079.
Moreover, our BMC method needs only one path, whereas the BMC method from [7]
needs a number of paths depending on a given formula ϕ. Thus, one may expect that
our method is much more effective since intuition is that an encoding which results in
fewer variables and clauses is usually easier to solve.
Finally, we evaluate the BMC method experimentally by means of a timed generic
pipeline paradigm (TGPP), which we model by a network of discrete timed automata
and compare with the corresponding method [7].
The rest of the paper is structured as follows. In Section 2 we briefly recall the basic
notion used through the paper. In Section 3 we define the translation to LTLq . In Sec-
tion 4 we define the BMC method for LTLq . In Section 5 we discuss our experimental
results. In Section 6 we conclude the paper.
2 Preliminaries
2.1 Discrete Timed Automata
Let IN be a set of natural numbers. We assume a finite set X = {x0 , . . . , xn−1 } of
variables, called clocks. Each clock is a variable ranging over a set of non-negative
natural numbers.
A clock valuation is a total function v : X 7→ IN that assigns to each clock x a
non-negative integer value v(x). The set of all the clock valuations is denoted by INn .
For X ⊆ X, the valuation v 0 = v[X := 0] is defined as: ∀x ∈ X, v 0 (x) = 0 and
∀x ∈ X \ X, v 0 (x) = v(x). For δ ∈ IN, v + δ denotes the valuation v 00 such that
∀x ∈ X, v 00 (x) = v(x) + δ. Let x ∈ X, c ∈ IN, and ∼ ∈ {<, 6, =, >, >}. The set C(X)
of clock constraints over the set of clocks X is defined by the following grammar:
cc := x ∼ c | cc ∧ cc.
Let v be a clock valuation, and cc ∈ C(X). A clock valuation v satisfies a clock con-
straint cc, written as v |= cc, iff cc evaluates to true using the clock values given by the
valuation v.
Definition 1. A discrete timed automaton A is a tuple (Act, Loc, `0 , T, X, Inv, AP , V ),
where Act is a finite set of actions, Loc is a finite set of locations, `0 ∈ Loc is an initial
location, T ⊆ Loc × Act × C(X) × 2X × Loc is a transition relation, X is a finite
set of clocks, Inv : Loc 7→ C(X) is a state invariant function, AP is a set of atomic
proposition, and V : Loc 7→ 2AP is a valuation function assigning to each location
a set of atomic propositions true in this location.
σ,cc,X
Each element t ∈ T is denoted by ` −→ `0 , and it represents a transition from
location ` to location `0 on the input action σ. X ⊆ X is the set of the clocks to be reset
with this transition, and cc ∈ C(X) is the enabling condition for t.
The semantics of the discrete timed automaton is defined by associating a transition
system with it, which we call a concrete model.
Definition 2. Let A = (Act, Loc, `0 , T, X, Inv, AP , V ) be a discrete timed automa-
ton, and v 0 a clock valuation such that ∀x ∈ X, v 0 (x) = 0. A concrete model for A is
a tuple MA = (Q, q 0 , −→, V), where Q = Loc × INn is a set of the concrete states,
q 0 = (`0 , v 0 ) is the initial state, −→⊆ Q × Q is a total binary relation on Q defined by
action and time transitions as follows. For σ ∈ Act and δ ∈ IN,
σ σ,cc,X
1. Action transition: (`, v) −→ (`0 , v 0 ) iff there is a transition ` −→ `0 ∈ T such
that v |= cc ∧ Inv(`) and v 0 = v[X := 0] and v 0 |= Inv(`0 ),
δ
2. Time transition: (`, v) −→ (`, v + δ) iff v |= Inv(`) and v + δ |= Inv(`).
V : Q 7→ 2AP is a valuation function such that V((`, v)) = V (`) for all (`, v) ∈ Q.
δ0 ,σ0 δ1 ,σ1 δ2 ,σ2
A run ρ of A is an infinite sequence of concrete states: q0 −→ q1 −→ q2 −→ . . . such
that qi ∈ Q, σi ∈ Act, and δi ∈ IN+ for each i ∈ IN. Notice that our runs are strongly
monotonic. This is because the definition of the run does not permit two consecutive
actions to be performed one after the other, i.e., between each two actions some time
must pass.
2.2 Metric Temporal Logic (MTL)
Let p ∈ AP , and I be an interval in IN of the form: [a, b) or [a, ∞), for a, b ∈ IN and
a 6= b. The MTL in release positive normal form is defined by the following grammar:
α := true | false | p | ¬p | α ∧ α | α ∨ α | αUI α | GI α.
Intuitively, UI and GI are the operators for bounded until and for bounded always.
The formula αUI β is true in a computation if β is true in the interval I at least in one
state and always earlier α holds. The formula GI α is true in a computation α is true
at all states of the computation that are in the interval I. The derived basic modality is
def
defined as follows: FI α = trueUI α (bounded eventually).
Let A be a discrete timed automaton, MA = (Q, q 0 , −→, V) a concrete model for
δ0 ,σ0 δ1 ,σ1 δ2 ,σ2
A, ρ : q0 −→ q1 −→ q2 −→ . . . a run of A, and α, β formulae of MTL. In order
to define the satisfiability relation for MTL, we need to define the notion of a discrete
path λρ corresponding to run ρ [6]. This can be done in a unique way because of the as-
sumption that δi ∈ IN+ . First, define the sequence ∆0 = [b0 , b1 ), ∆1 = [b1 , b2 ), ∆2 =
[b2 , b3 ), . . . of pairwise disjoint intervals, where: b0 = 0, and bi = bi−1 + δi−1 if
i > 0. Now, for each t ∈ IN, let idxρ (t) denote the unique index i such that t ∈ ∆i .
A discrete path (or path) λρ corresponding to ρ is a mapping λρ : IN 7→ Q such that
λρ (t) = (`i , vi + t − bi ), where i = idxρ (t). Given t ∈ IN, the suffix λtρ of a path λρ at
time t is a path defined as: ∀i ∈ IN, λtρ (i) = λρ (t + i).
In order to improve readability, in the following definition we write λtρ |=MTL ϕ
instead of Mϕ , λtρ |=MTL ϕ, for any MTL formula ϕ.
Definition 3. The satisfiability relation |=MTL , which indicates truth of an MTL for-
mula in the concrete model MA along a path λρ at time t ∈ IN, is defined inductively
as follows:
– λtρ |=MTL true, λtρ 6 |=MTL false,
– λtρ |=MTL p iff p ∈ V(λρ (t)), λtρ |=MTL ¬p iff p 6∈ V(λρ (t)),
– λtρ |=MTL α ∧ β iff λtρ |=MTL α and λtρ |=MTL β,
– λtρ |=MTL α ∨ β iff λtρ |=MTL α or λtρ |=MTL β,
0 00
– λtρ |=MTL αUI β iff (∃t0 ∈ I)(λt+t
ρ |=MTL β and (∀0 6 t00 < t0 )λt+t
ρ |=MTL α),
0
– λtρ |=MTL GI β iff (∀t0 ∈ I)(λt+t
ρ |= MTL β).
As λ0ρ = λρ , we shall write MA , λρ |=MTL ϕ for MA , λ0ρ |=MTL ϕ. An MTL formula
ϕ is existentially valid in the model MA , denoted MA |=MTL Eϕ, if, and only if
MA , λρ |=MTL ϕ for some path λρ starting in the initial state of MA . Determining
whether an MTL formula ϕ is existentially valid in a given model is called an existential
model checking problem.
3 Translation from MTL to LTLq
3.1 Abstract model
Let ϕ be an MTL formula and A = (Act, Loc, `0 , T, X, Inv, AP , V ) be a discrete
timed automaton with X = {x0 , . . . , xn−1 }. For each j ∈ {0, . . . , n − 1}, let cmax
j be
the largest constant appearing in intervals of ϕ and in any enabling condition involving
the clock xj and used in the state invariants and guards of A. For two clock valuations
v and v 0 in INn , we say that v ' v 0 iff for each 0 6 j < n either v(xj ) > cmax j and
v 0 (xj ) > cmax
j or v(x) 6 c max
j and v 0
(x) 6 c max
j and v(x) = v 0
(x).
It is well known, that the relation ' is an equivalence relation, what gives rise to
construct an finite abstract model. To this end we define the set of possible values of the
clock xj in the abstract model as IDj = {0, . . . , cmaxj +1} for 0 6 j < n. Moreover, for
two clock valuations v and v 0 in ID0 × . . . × IDn−1 , we say that v 0 is the time successor
of v (denoted succ(v)) as follows: for each 0 6 j < n,
v(xj ) + 1, if v(xj ) 6 cmax
j ,
succ(v)(xj ) =
cmax
j + 1, if v(x j ) = c max
j + 1.
Definition 4. Let A = (Act, Loc, `0 , T, X, Inv, AP , V ) be a discrete timed automa-
ton, and ϕ an MTL formula build over the set AP of atomic propositions. An abstract
model for the automaton A and the formula ϕ is a tuple Mϕ = (S, b s0 , ,→, V),
b where
0 0 n+1
S = L×(ID0 ×. . .×IDn−1 ) is the set of abstract states, s = (` , {0}
b ) is the initial
b : Sb → 2AP is a valuation function such that for all p ∈ AP , p ∈ V((`,
state, V b v)) iff
p ∈ V (`), and ,→⊆ S × Act0 × S, where Act0 = Act ∪ {τ }, is a transition relation
defined by the time and action transitions:
τ
– Time transition: (`, v) ,→ (`, v 0 ) iff v |= Inv(`), v 0 = succ(v), and v 0 |= Inv(`),
σ
– Action transition: for any σ ∈ Act, (`, v) ,→ (`0 , v 0 ) iff there exists a transition
σ,cc,X
` −→ `0 ∈ T such that v |= cc ∧ Inv(`), v 0 = v[X := 0], and v 0 |= Inv(`0 ).
Definition 5. A path in Mϕ is a sequence π = (s0 , s1 , . . .) of states such that for each
τ σ
j ∈ IN, either (sj ,→ sj+1 ) or (sj ,→ sj+1 ) for some σ ∈ Act, and every action
transition is preceded by at least one time transition.
The above definition of the path ensures that the first transition is the time one, and that
between each two action transitions at least one time transition appears.
For a path π, π(j) denotes the j-th state sj of π, π[..j] = (π(0), . . . , π(j)) denotes
the j-th prefix of π ending with π(j), and π j = (sj , sj+1 , . . .) denotes the j-th suffix
of π starting with π(j).
Given a path π one can define a function ζπ : IN 7→ IN such that for each j > 0,
ζπ (j) is equal to the number of time transitions on the prefix π[..j]. Let us note that for
each j > 0, ζπ (j) gives the value of the global time in the j-th state of the path π.
3.2 The logic LTLq
Let I be the set of all intervals in IN. Let AP I = {qI | I ∈ I}. The LTLq formulae in
the negation normal form are defined by the following grammar:
ψ ::= true | false | p | ¬p | qI | ¬qI | ψ ∧ ψ | ψ ∨ ψ | ψUψ | Gψ,
where p ∈ AP and qI ∈ AP I . The temporal modalities U and G are, respectively,
named as the until and the always. The derived basic temporal modality for eventually
def
is defined in the standard way: Fψ = trueUψ.
In order to improve readability, in the following definition we write hπ, mi |=k ψ
instead of Mϕ , hπ, mi |=k ψ, for any LTLq formula ψ.
d
Definition 6. The satisfiability relation |= , which indicates truth of an LTLq formula
in the abstract model Mϕ along the path π with the starting point m and at the depth
d > m, is defined inductively as follows:
d d
– hπ, mi |= true, hπ, mi 6 |= false,
d d
– hπ, mi |= p iff p ∈ V(π(d)), hπ, mi |= ¬p iff p ∈
/ V(π(d)),
d
– hπ, mi |= qI iff ζπ (d) − ζπ (m) ∈ I,
d
– hπ, mi |= ¬qI iff ζπ (d) − ζπ (m) 6∈ I,
d d d
– hπ, mi |= α ∧ β iff hπ, mi |= α and hπ, mi |= β,
d d d
– hπ, mi |= α ∨ β iff hπ, mi |= α or hπ, mi |= β,
d j i
– hπ, mi |= αUβ iff (∃j > d)(hπ, di |= β and (∀d 6 i < j) hπ, di |= α),
d j
– hπ, mi |= Gβ iff (∀j > d) hπ, di |= β.
An LTLq formula ψ existentially holds in the model Mϕ , written Mϕ |= Eψ, if,
0
and only if Mϕ , hπ, 0i |= ψ for some path π starting at the initial state. The existential
model checking problem asks whether Mϕ |= Eψ.
3.3 Translation
Let p ∈ AP , α and β be formulae of MTL. We define the translation from MTL into
LTLq as a function tr : MTL → LTLq in the following way:
– tr(true) = true, tr(false) = false, tr(p) = p, tr(¬p) = ¬p,
– tr(α ∧ β) = tr(α) ∧ tr(β), tr(α ∨ β) = tr(α) ∨ tr(β),
– tr(αUI β) = tr(α)Utr(qI ∧ β), tr(GI β) = G(¬qI ∨ tr(β))
Observe that the translation of literals as well as logical connectives is straightforward.
The translation of the UI operator ensures that β holds somewhere in the interval I (this
is expressed by the requirement qI ∧ tr(β)), and α holds always before β. Similarly,
the translation of the GI operator ensures that β always holds in the interval I (this is
expressed by the requirement ¬qI ∨ tr(β)).
Theorem 1. Let A be a discrete timed automaton, MA the concrete model for A, ϕ
an MTL formula, and Mϕ the abstract model for the automaton A and the formula ϕ.
Then, MA |= Eϕ if, and only if Mϕ |= Etr(ϕ).
4 Bounded model checking
In this section we define a bounded semantics for LTLq in order to translate the existen-
tial model checking problem for LTLq into the satisfiability problem.
4.1 Bounded semantics
To define the bounded semantics one needs to represent infinite paths in a model in a spe-
cial way. To this aim, we recall the notions of k-paths and loops [8].
Definition 7. Let Mϕ be a model, k ∈ IN, and 0 6 l 6 k. A k-path is a pair (π, l),
also denoted by πl , where π is a finite sequence π = (s0 , . . . , sk ) of states such that
τ σ
for each 0 6 j < k, either (sj ,→ sj+1 ) or (sj ,→ sj+1 ) for some σ ∈ Act, and
every action transition is preceded by at least one time transition. A k-path πl is a loop,
written a(πl ) for short, if l < k and π(k) = π(l).
If a k-path πl is a loop it represents the infinite path of the form uv ω , where u =
(π(0), . . . , π(l)) and v = (π(l + 1), . . . , π(k)). We denote this unique path by πel . Note
that for each j ∈ IN, πel l+j = πel k+j .
In the definition of bounded semantics for variables from AP I one needs to use
only a finite prefix of the sequence (ζπel (0), ζπel (1), . . .). Namely, for a k-path πl that
is not a loop the prefix of the length k is needed, and for a k-path πl that is a loop the
prefix of the length k + k − l is needed.
In order to improve readability, in the following definition we write hπl , mi |=k ψ
instead of Mϕ , hπl , mi |=k ψ, for any LTLq formula ψ.
Definition 8 (Bounded semantics). Let Mϕ be the abstract model, πl be a k-path in
Mϕ , and 0 6 m, d 6 k. The relation |=dk is defined inductively as follows:
d d
– hπl , mi |=k true, hπl , mi 6 |=k false,
d d
– hπl , mi |=k p iff p
∈ V(πl (d)), hπl , mi |=k ¬p iff p ∈ / V(πl (d)),
ζ
πel
(d) − ζ πel (m) ∈ I, if πl is not a loop,
d
– hπl , mi |=k qI iff ζπel (d) − ζπel (m) ∈ I, if πl is a loop and d > m,
ζπel (d + k − l) − ζπel (m) ∈ I, if πl is a loop and d < m,
d d
– hπl , mi |=k ¬qI iff hπl , mi 6 |=k qI
d d d
– hπl , mi |=k α ∧ β iff hπl , mi |=k α and hπl , mi |=k β,
d d d
– hπl , mi |=k α ∨ β iff hπl , mi |=k α or hπl , mi |=k β,
– hπl , mi |=dk αUβ iff (∃d6j6k ) hπl , di |=jk β and (∀d6i min(d, l) implies hπl , di |=jk β.
An LTLq formula ψ existentially k-holds in the model Mϕ , written Mϕ |=k Eψ,
0
if, and only if Mϕ , hπ, 0i |=k ψ for some path π starting at the initial state.
Theorem 2. Let A be a discrete timed automaton, ϕ an MTL formula, and Mϕ the
abstract model for the automaton A and the formula ϕ. Moreover, let ψ = tr(ϕ). Then,
Mϕ |= Eψ if, and only if there exists k > 0 such that Mϕ |=k Eψ.
4.2 Translation to SAT
The last step of our method is the standard one (see [8, 7]). It consists in encoding the
transition relation of Mϕ and the LTL formula tr(ϕ). The only novelty lies in encoding
of the finite prefix of the sequence (ζπel (0), ζπel (1), . . .). The translation to SAT results
in the propositional formula [Mϕ , tr(ϕ)]k with the property expressed in the following
theorem.
Theorem 3. Let Mϕ be an abstract model. Then, for every k ∈ IN, Mϕ |=dk Etr(ϕ)
if, and only if, the propositional formula [Mϕ , tr(ϕ)]k is satisfiable.
5 Experimental results
In this section we experimentally evaluate the performance of our new translation.
We have conducted the experiments using the slightly modified timed generic pipeline
paradigm (TGPP) [7].
5.1 Timed Generic Pipeline Paradigm
The Timed Generic Pipeline Paradigm (TGPP) discrete timed automata model shown
in Figure 1 consists of Producer producing data within the certain time interval ([a, b])
or being inactive, Consumer receiving data within the certain time interval ([c, d]) or
being inactive within the certain time interval ([g, h]), and a chain of n intermediate
Nodes which can be ready for receiving data within the certain time interval ([c, d]),
processing data within the certain time interval ([e, f ]) or sending data. We assume that
a = c = e = g = 1 and b = d = f = h = 2 · n + 2, where n represents number of
nodes in the TGPP.
To compare our experimental results with [7], we have tested the TGPP discrete
timed automata model, scaled in the number of intermediate nodes on the following
MTL formulae that existentially hold in the model of TGPP (n is the number of nodes):
Fig. 1: The TGPP system.
– ϕ0 = F[0,2·n+3) (ConsReceived). It expresses that Consumer receives the data in
at most 2 · n + 3 time units.
– ϕ1 = G[0,2·n+2) (ConsReady). It states that the Consumer is always forced to
receive the data in 2 · n + 2 time units.
– ϕ2 = G[0,∞) (P rodReady∨ConsReady). It states that always either the Producer
has sent the data or the Consumer has received the data.
– ϕ3 = F[0,2·n+3) (G[0,∞) (P rodSend ∨ ConsReceived)). It states that eventually
in time less then 2 · n + 3 it is always the case that the Producer is ready to send the
data or the Consumer has received the data.
– ϕ4 = G[0,∞) (F[0,2·n+3) (ConsReceived)). It states that the Consumer infinitely
often is receiving the data in time less then 2 · n + 3.
– ϕ5 = G[0,∞) (F[0,2·n+3) (P rodSend) ∧ G[0,∞) (F[0,2·n+3) (ConsReceived)). It
states that the Producer infinitely often is sending the data in the time less then
2 · n + 3 and the Consumer infinitely often is receiving the data in time less then
2 · n + 3.
5.2 Performance evaluation
We have performed our experimental results on a computer equipped with I7-3770 pro-
cessor, 32 GB of RAM, and the operating system Linux with the kernel 4.6.4. Our
SAT-based BMC algorithms are implemented as standalone programs written in the
programming language C++. We used the state of the art SAT-solver CryptoMiniSat5
(http://www.msoos.org/).
All the benchmarks together with instructions on how to reproduce our experimental
results can be found at the web page http://ajd.czest.pl/~a.zbrzezny/
bmc.html.
The number of considered k-paths (fk ) for the new translation is always equal to 1
and for the old translation is respectively equal to: fk (ϕ0 ) = 2, fk (ϕ1 ) = 2, fk (ϕ2 ) =
2, fk (ϕ3 ) = 3, fk (ϕ4 ) = 8 · n + 9, fk (ϕ5 ) = 16 · n + 17. The length of the witness
for the formula ϕ0 is equal to 4 · n + 4 ; for the formula ϕ1 is equal to 8 · n + 6; for the
formula ϕ2 and is equal to 8 · n + 6; for the formula ϕ3 is equal to 8 · n + 15; for the
formula ϕ4 is equal to 8 · n + 6; for the formula ϕ5 is equal to 8 · n + 6.
Total time usage for a TGPP ϕ0 Memory usage for a TGPP ϕ0
5000 1200
New translation New translation
4500 Old translation Old translation
1000
4000
3500
Memory in MB
800
Time in sec.
3000
2500 600
2000
400
1500
1000
200
500
0 0
1 3 5 7 9 11 13 15 17 19 21 22 23 24 25 26 1 3 5 7 9 11 13 15 17 19 21 22 23 24 25 26
Number of Nodes Number of Nodes
Fig. 2: ϕ0 : TGPP with n nodes.
From Fig. 2 one can observe that the new method is able to verify the formula ϕ0
for TGPP with 27 nodes. The old method is able to verify the formula ϕ0 for TGPP
with 24 nodes. The memory usage for the old method is 1.72 times higher than for the
new method for 24 nodes.
Total time usage for a TGPP ϕ1 Memory usage for a TGPP ϕ1
4500 800
New translation New translation
4000 Old translation 700 Old translation
3500 600
Memory in MB
3000
Time in sec.
500
2500
400
2000
300
1500
1000 200
500 100
0 0
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Number of Nodes Number of Nodes
Fig. 3: ϕ1 : TGPP with n nodes.
From Fig. 3 one can observe that the new method is able to verify the formula ϕ1
for TGPP with 17 nodes. The old method is able to verify the formula ϕ1 for TGPP
with 15 nodes. The memory usage for the old method is 1.50 times higher than for the
new method for 15 nodes.
From Fig. 4 one can observe that the new method is able to verify the formula ϕ2
for TGPP with 18 nodes. The old method is able to verify the formula ϕ2 for TGPP
with 15 nodes. The memory usage for the old method is 1.55 times higher than for the
new method for 15 nodes.
From Fig. 5 one can observe that the new method is able to verify the formula ϕ3
for TGPP with 17 nodes. The old method is able to verify the formula ϕ3 for TGPP
with 13 nodes. The memory usage for the old method is 2.21 times higher than for the
new method for 13 nodes.
From Fig. 6 one can observe that the new method is able to verify the formula ϕ4
for TGPP with 13 nodes. The old method is able to verify the formula ϕ4 for TGPP
Total time usage for a TGPP ϕ2 Memory usage for a TGPP ϕ2
4500 900
New translation New translation
4000 Old translation 800 Old translation
3500 700
Memory in MB
3000 600
Time in sec.
2500 500
2000 400
1500 300
1000 200
500 100
0 0
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
Number of Nodes Number of Nodes
Fig. 4: ϕ2 : TGPP with n nodes.
Total time usage for a TGPP ϕ3 Memory usage for a TGPP ϕ3
5000 1200
New translation New translation
4500 Old translation Old translation
1000
4000
3500
Memory in MB
800
Time in sec.
3000
2500 600
2000
400
1500
1000
200
500
0 0
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Number of Nodes Number of Nodes
Fig. 5: ϕ3 : TGPP with n nodes.
Total time usage for a TGPP ϕ4 Memory usage for a TGPP ϕ4
4000 3000
New translation New translation
3500 Old translation Old translation
2500
3000
Memory in MB
2000
Time in sec.
2500
2000 1500
1500
1000
1000
500
500
0 0
1 2 3 4 5 6 7 8 9 10 11 12 1 2 3 4 5 6 7 8 9 10 11 12
Number of Nodes Number of Nodes
Fig. 6: ϕ4 : TGPP with n nodes.
with 7 nodes. The memory usage for the old method is 10.32 times higher than for the
new method for 7 nodes.
From Fig. 8 one can observe that the new method is able to verify the formula ϕ5
for TGPP with 13 nodes. The old method is able to verify the formula ϕ5 for TGPP
with 6 nodes. The memory usage for the old method is 21.39 times higher than for the
new method for 6 nodes.
For the formula ϕ4 the new method generates only 395775 variables and 1229009
clauses (Fig. 7) for 7 nodes. The time consumed by BMC to generate the set of clauses
is equal 65.35 sec. The memory consumed by BMC to generate the set of clauses is
Number of variables for a TGPP ϕ4 Number of clauses for a TGPP ϕ4
6 7
7x10 2x10
New translation New translation
Old translation 1.8x107 Old translation
6x106 7
1.6x10
Number of variables
5x106
Number of clauses
1.4x107
4x106 1.2x107
1x107
3x106 8x106
2x106 6x106
6
4x106
1x10
2x106
0 0
1 2 3 4 5 6 7 8 9 10 11 12 1 2 3 4 5 6 7 8 9 10 11 12
Number of Nodes Number of Nodes
Fig. 7: Number of variables and clauses for ϕ4 and TGPP with n nodes.
Total time usage for a TGPP ϕ5 Memory usage for a TGPP ϕ5
7000 5000
New translation New translation
Old translation 4500 Old translation
6000
4000
5000 3500
Memory in MB
Time in sec.
4000 3000
2500
3000 2000
2000 1500
1000
1000
500
0 0
1 2 3 4 5 6 7 8 9 10 11 12 1 2 3 4 5 6 7 8 9 10 11 12
Number of Nodes Number of Nodes
Fig. 8: ϕ5 : TGPP with n nodes.
equal 100.54 MB. The time and memory consumed by the state of the art SAT solver
CryptoMiniSat5, respectively is equal to 112.59 sec. and 287.41 MB.
The old method generates 6122646 variables and 18739998 clauses. The time con-
sumed by BMC to generate the set of clauses is equal 977.18 sec. The memory con-
sumed by BMC to generate the set of clauses is equal 1505.05 MB. The time and
memory consumed by the state of the art SAT solver CryptoMiniSat5, respectively is
equal to 2892.31 sec. and 2967.82 MB.
The example above shows that our new method results in reducing the overall run-
time and memory of BMC to construct a CNF formula, and of SAT solver to check
satisfiability of this formula.
6 Conclusions
We have proposed, implemented, and experimentally evaluated SAT-based
BMC method for soft real-time systems, which are modelled by discrete timed au-
tomata, and for properties expressible in MTL with the semantics over discrete timed
automata. The method is based on a translation of the existential model checking for
MTL to the existential model checking for LTLq , and then on the translation of the
existential model checking for LTLq to the propositional satisfiability problem.
In the following table we compare the new BMC method with the old one.
Simple BMC+DTA&MTL BMC+DTA&MTL[6]
no new clocks a number of new clocks equal to the number
of intervals in the given formula
no new transitions exponential number of new transitions
only one path a number of paths depending on the given
formula and the length of the k-path
smaller number of propositional substantially larger number
variables and clauses of propositonal variables and clauses
better time and memory usage worse time and memory usage
Table 1: The comparison of two methods
The experimental results show that our approach is much better than the approach
based on translation to HLTL. The reason is that the new method needs only one new
path, does not need any new clocks, and does not need any new transitions. The ex-
periments confirm that the improvement in question leads to a reduction of the size of
the CNF formulas submitted to the SAT solver, and therefore to a significant reduc-
tion both in the time and memory required by the SAT solver to return an answer. The
paper presents preliminary experimental results only, but they show that the proposed
verification method is quite efficient and worth exploring.
Therefore, in our future work we are going to define the SMT-based BMC encoding
for DTA and for LTLq and compare this encoding with the SAT-based encoding, and
we would like to develop SAT-based BMC method for timed automata and properties
expressible in TECTL.
References
1. R. Alur and D. Dill. A theory of Timed Automata. Theoretical Computer Science, 126(2):183–
235, 1994.
2. A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In
Proc. of the 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS’99), volume 1579 of LNCS, pages 193–207. Springer-Verlag, 1999.
3. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu.
Bounded model checking. Advances in Computers, 58:117–148, 2003.
4. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Sys-
tems, 2(4):255–299, 1990.
5. 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.
6. Bożena Woźna-Szcześniak and Andrzej Zbrzezny. A translation of the existential model
checking problem from MITL to HLTL. Fundamenta Informaticae, 122(4):401–420, 2013.
7. Bożena Woźna-Szcześniak and Andrzej Zbrzezny. Checking MTL properties of discrete timed
automata via bounded model checking. Fundam. Inform., 135(4):553–568, 2014.
8. A. Zbrzezny. A new translation from ECTL∗ to SAT. Fundamenta Informaticae, 120(3-
4):377–397, 2012.