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.