Bounded Model Checking for the Existential Fragment of TCTL _ {-G} and Diagonal Timed Automata

Please download to get full document.

View again

of 28
5 views
PDF
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Document Description
Bounded Model Checking for the Existential Fragment of TCTL _ {-G} and Diagonal Timed Automata
Document Share
Document Tags
Document Transcript
  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, 42-200 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 gener-ating a propositional formula that is satisfiable iff such a counterexample exists. The BMC methodis feasible for the various classes of temporal logic; in particular it is feasible for TECTL (the exis-tential fragment of Time Computation Tree Logic) and Diagonal-free 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 efficiencyof the method. 1. Introduction  Model checking is a verification technique that was srcinally developed for (untimed) temporal logics[8]. Its main idea is to represent a finite state system, often deriving from a hardware or software design,as a labelled transition system (model), to represent a specification (property) by a modal formula, andto check automatically whether the formula holds in the model.Over the past few years, the interest in automated verification has been moved towards concurrentreal-time systems, and now verification 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, 42-200 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 verified 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 PSPACE-complete in contrary to the modelchecking problem for MITL that is decidable but EXPSPACE-complete [28].The practical applicability of the model checking method is strongly restricted by so-called 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], BDD-based symbolic storage methods [7, 18], and SAT-relatedalgorithms [5, 19, 21, 30, 25, 26, 27, 35, 34].Bounded model checking (BMC) is one of the SAT-based (satisfiability checking) methods, and itwas introduced as a technique complementary to the BDD-based 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 efficiency 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 sufficient forfinding an error. Obviously, when testing large models and complex formulae the efficiency 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 efficiency 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 easy-to-usemodels. Timed automata with diagonal constraints (or Diagonal Timed Automata [31]) are sufficientlyexpressive to describe the essential aspects of time-dependent real-life problems in a variety of applica-tion 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 diagonal-free timed automata [4]. However, a construction of diagonal-free 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 briefly introduce diagonal timed au-tomata 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 definitions and notations that are used in Section 5 to define 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 , defined in Section 7. In Section 8 we provide some preliminary experimental results fora modified Fischer mutual exclusion protocol, and in Section 9 we show how to tailor the BMC tech-nique from Section 7 to a specially chosen subclass of TECTL − G formulae. The last section containsa discussion of related work and final remarks.   B. Wo´  zna and A. Zbrzezny/BMC for  TECTL − G and Diagonal Timed Automata 3 2. Diagonal Timed Automata To define diagonal time automata formally we need to say what type of clock constraints are allowed asguards and invariants. For a finite set of real variables X  , called clocks , and a set of natural numbers N = { 0 , 1 ,... } , we define 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. Definition 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 finite set of actions, L is a nonempty finite 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 finite 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 satisfied. The guard cc has to be satisfied to enable the transition. The transitionresets all clocks in the set Y  to the value 0 .The semantics of a timed automaton A is defined by associating to it a dense model as defined below. Definition 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 ) defined 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 satisfied.  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 infinite sequence of statessuch that action transitions are taken infinitely 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 suffix 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 infinitely 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  non-zeno runs.Formally, an infinite run ρ is said to be non-zeno iff  Σ i ∈ N δ  i is unbounded. An infinite 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 non-zeno. q  0 q  1 bac, x := 0 x := 0 x ≤ 2 x ≤ 2 Figure 1. An example of non-time progressive timed automaton. We say that A is time-progressive iff all its q  0 -runs are non-zeno. For easiness of presentation, weconsider only time-progressive timed automata; note that time-progressiveness 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 Compu-tation 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 defined by the followinggrammar: ϕ := p | ¬  p | ϕ ∧ ϕ | ϕ ∨ ϕ | E( ϕ U I  ϕ ) | A( ϕ U I  ϕ ) The other basic operators are defined 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 suffixes of the q  0 -runs. In order todefine a satisfaction relation for TCTL − G , we define 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 ) . Definition 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 definedinductively 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 defining the notion of validity in a dense model and defining 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 .
Similar documents
View more...
Search Related
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks