Data Structure Choices for On-the-Fly Model Checking of Real-Time Systems

Abstract

-This paper studies the performance of sparse- checking based on proof search: a formula correspondmatrix-based data structures to represent clock zones (con- ing to the assertion that a timed automaton satisfies a vex sets of clock values) in an on-the-fly predicate equation mu-calculus property can be checked in a goal-driven system model checker for timed automata. We analyze the fashion to determine its truth. Zhang and Cleaveland [6] impact of replacing the dense difference bound matrix demonstrated the efficiency of this approach vis a` vis (CDRBDMA)rrwaiythdbatoathsttrhuectluinrkee.dF-rliosmtCaRnDalZyosinseoanndthaerpraayir-elidst- other real-time model-checking approaches. example-by-example differences in time performance, we In this paper we consider the special model checkinfer the DBM is either competitive with or slightly faster ing case of timed automata and timed modal equation than the CRDZone, and both perform faster than the systems representing safety properties (also studied in CRDArray. Using similar analysis on space performance, [6]), for which there are still many opportunities for we infer the CRDZone takes the least space, and the DBM performance improvements. One component of such a takes less space than the CRDArray. model checker that has a noticeable influence on performance is the data structure for the sets of clock values. I. INTRODUCTION When analyzing safety properties, each desired set of Automatic verification of real-time systems is under- clock values forms a convex set of clock values, or clock taken using notations for verifiable programs and check- zone (see Definition 3). The conventional way to store able specifications (see [1]-[6]). One common program a clock zone is as a difference bound matrix (DBM) notation is timed automata [7]. There are specification (see Definition 4) [15], which stores the constraints as notations such as timed computation tree logic (TCTL) a matrix. This approach is used by UPPAAL [16] and [1], [8] and timed extensions of a modal mu-calculus, described in [17]. To potentially save space and time, including one in [3] and another given in [5]. Specifica- instead of representing the set of constraints as a matrix, tions in a timed modal mu-calculus can be written as lists one can represent the set as an ordered linked path of of equations, known as timed modal equation systems constraints where any clock difference not on the path [5], [6], [9]. For information on the untimed modal-mu has the implicit constraint < 1. If we generalize this calculi, see [10]-[12], and see [10], [11] for information to allow for a union of zones to be represented by a on modal equation systems. directed graph of constraints (representing a tree of paths One approach to model checking timed automata as opposed to a single path), we get a clock restriction with timed modal mu-calculus specifications is to use diagram (CRD) [18]. If we compress the nodes to have predicate equation systems (PES), which were invented them represent upper and lower bound constraints as well independently by Groote and Willemse (as parameter- as explicitly encoding both valid and invalid paths, we ized boolean equation systems) [13] and by Zhang and get a clock difference diagram (CDD) [2]. These two Cleaveland [6], [9]. Predicate equation systems provide structures are extensions of binary decision diagrams a general framework for program models including para- (BDDs) (see [19] for information). metric timed automata [6] and Presburger systems [14]. To improve performance, we take the above idea of They also admit a natural on-the-fly approach to model a linked implementation and incorporate the sparseness of the implementation of CRDs while simplifying (or Research supported by NSF Grant CCF-0820072. shrinking) the structure to only support a single clock

-

zone (CRDs and CDDs in general can encode unions of clock zones). This simplified structure is a sparse sorted linked-list implementation of a DBM, the CRDZone (see Definition 5). We also implement an array-list version of the CRDZone, the CRDArray (see Definition 6). A CRDZone may be seen as a sparse sorted linked-list implementation of a DBM, and the CRDArray a sparse array-list implementation of the CRDZone. We examine the time and space performance of all three clock zone implementations: the matrix DBM, linked-list CRDZone and array-list CRDArray.

The contributions of this paper are:

We run experiments comparing time and space performance of a model checker (on safety (reachability) properties) with the DBM, CRDZone and CRDArray data structure implementations.

We formalize and extend the analysis style performed in the model checking experiments of [ 2 ], [ 6 ], [ 9 ], [ 18 ], [ 20 ], [ 21 ] by utilizing paired data (each implementation checked the same examples) and applying descriptive statistics on the paired example-by-example differences on time and space ExamRpelea1l-(ETxaimmpleeof MatiomdedealutoCmahtoen)c. kCionnsgider consumption. See Section VI for details on the the timed automaton in Figure 1, which models a train statistics and Section VI-B for the analysis. in the generalized railroad crossing (GRC) protocol.

Some sources [ 6 ], [ 23 ] and our PES checker allow clock assignments (x1 := x2) in addition to clock resets on edges, other sources [ 17 ] allow constraints on clock differences and other sources [ 1 ] allow states to be labelled with atomic propositions that each state satisfies.

Timed automata use clock valuations 2 V (V = CX ! R 0 is the set of all clock valuations), which at any moment stores a non-negative real value for each clock x 2 CX. The semantics of a timed automaton are described as an infinite-state machine, where each state is a location-valuation pair (l; ). Transitions represent either time advances or edge executions (performing an action). For a formal definition of the semantics of a timed automaton, see [ 7 ].

I : L ! (CX) gives a clock constraint for each location l. I(l) is called the invariant of l.

E L (CX) 2CX L is the set of edges.

In an edge e = (l; a; ; Y; l0) from l to l0 with action a, 2 (CX) is the guard of e, and Y represents the set of clocks to reset to 0.

After analyzing the experimental results, for time performance we infer the DBM is either competitive with or slightly faster than the CRDZone and both perform faster than the CRDArray for the examples in this experiment.

In terms of space, we infer the CRDZone takes up the least space, and the DBM and takes less space than the CRDArray for the examples in this experiment.

II. PROGRAM MODEL AND SPECIFICATIONS

A. Timed Automata

A timed automaton encodes the behavior of a real-time system [ 7 ], [ 22 ].

Definition 1 (Clock constraint 2 (CX)). Given a set of clocks CX, a clock constraint is constructed with the following grammar, where xi is a clock and c 2 Z: exit, x1 > 1 0: far

1: near approach, x1 := 0 x1 < 4 in, x1 = 4, x1 := 0 2: in x1 < 15 FigT. C1.TLTim(eIdnvauatloimd)a:tonATFA<∞1,[naemarodel oinf]a train in the generalized raiTlroCaTdLcro(ssVinagli(dG)R:CA) Gpr<o∞to[cnoela.r ! AF!TP+TDU[far]]

There are three locations—0: far (initial location), 1: near and 2: in, with one clock x1. There are the actions approach, in and exit in . Here, location 1 has the2 invariant x1 4 while 0 has no invariant. The edge (1: near; in; x1 = 4; fx1g;2: in) has the guard x1 = 4 and resets x1 to 0.

B. Modal Equation Systems (MES)

(CX) is the set of all possible clock constraints.

Definition 2 (Timed automaton). A timed automaton T A = (L; L0; ; CX; I; E) is a tuple where:

We use a modal equation system (MES) to represent ::= xi < c j xi c j xi > c j xi c j ^ real-time temporal properties that timed automata can possess. A MES is an ordered list of equations with variables on the left hand side and basic timed temporal logical formulae on the right. Each equation involves a variable X, a basic formula and a greatest fixpoint ( ) L is a finite set of locations with the initial set of or a least fixpoint ( ), and the equation is labeled with locations L0 L. the fixpoint (X = or X = ). For a formal definition is the set of actions and CX is the set of clocks. of MES syntax and semantics, see [ 6 ], [ 9 ]. Example 2 (Continuation of Example 1). Again consider the timed automaton in Figure 1. The MES

X1 = far ^ 8([ ](X1))

(1) represents the safety property “the train is always in state 0: far”, read as “the variable X1 is the greatest fixpoint of being in state 0: far and for all time advances (8), for all next actions ([ ]), X1 is true.” This is an invalid specification for the timed automaton because the execution (0: far; [xi = 0]) 2!:5 (0: far; [xi = 2:5])

appr!oach (1: near; [xi = 0]) !2 : : : (2) reaches location 1: near and thus violates the property.

III. DATA STRUCTURES FOR CLOCK VALUE SETS

A. Clock Zones

This definition of a clock zone is taken from [ 7 ], [ 19 ]. Definition 3 (Clock zone). A clock zone is a convex combination of single-clock inequalities. Each clock zone can be constructed using the following grammar, where xi and xj are arbitrary clocks and c 2 Z: Z ::= xi < c j xi c j xi > c j xi

c j xi xj < c j xi xj c j Z ^ Z (3)

Clock zones extend clock constraints with inequalities of clock differences. These inequalities are used for model checking even though clock difference inequalities are not used in timed automata. Moreover, in general, the representation of a clock zone is not unique. Example 3. Let z = 1 x1 < 3 ^ 0 x2 5. There is the implicitly encoded constraint x2 x1 4. To see this, consider the longer path of constraints (x0 is a dummy clock that always has value 0): + x2 x0 x2 x0 x1 x1 5 4

(x2 1 (1

5) x1)

To provide a standardized, or canonical, form for clock zone representations, we use shortest path closure [ 17 ]. This form makes every implicit constraint explicit. This can be implemented in O(n3) time using Floyd-Warshall all-pairs shortest path algorithm, described in [ 24 ], [ 25 ]. Other standard forms exist [ 18 ], [ 20 ].

While converting to a canonical form takes a considerable amount of time, it is needed to simplify and standardize the algorithms for the zone operations including time successor (succ(z)) computations and subset checks. For time successor, having the zone in canonical form allows the time elapse operation to simply set all single-clock upper bound constraints to < 1.

B. Clock Zone Data Structures: Difference Bound Matrix (DBM), CRDZone and CRDArray

One way to represent a clock zone is a difference bound matrix (DBM), described in Definition 4. See [ 15 ], [ 17 ] for a more thorough description.

Definition 4 (Difference bound matrix (DBM)). Let n 1 be the number of clocks. A DBM is an n n matrix where entry (i; j) is the upper bound of the clock constraint xi xj , represented as xi xj uij or xi xj < uij . The 0th index is reserved for a dummy clock x0, which is always 0, allowing bounds on single clocks to be represented by the clock differences xi x0 and x0 xj . See Figure 2 for a picture of the DBM structure and Example 4 for a concrete example.

Definition 5 (CRDZone). A CRDZone is a sparse sorted linked-list representation of a clock zone. Each constraint is encoded like a constraint in a DBM, as an upper bound constraint on xi xj , labeled as (i; j), with x0 always being 0. The CRDZone has these properties: 1) Nodes are in lexicographical order of clock constraint: (i1; j1) (i2; j2) iff i1 < i2 or (i1 = i2 and j1 < j2). 2) The (0; 0) node is always given to ensure a univer

sal head node with an initial value of x0 x0 0. 3) If a CRDZone node (i; j) is missing then the zone has an implicit constraint: (i; i) : xi xi 0 and (i; j); i 6= j : xi xj < 1.

See Figure 3 for a picture of the CRDZone structure and Example 4 for a concrete example.

This lexicographical ordering is the same ordering used in CDDs and CRDs [ 2 ], [ 18 ]. While the ordering j }| (z2: : : : : : i 4: : : : : : : : : : : : xi : : : : : : xj uij { 3 5

Definition 6 (CRDArray). The CRDArray is an array list implementation of the CRDZone. Thus, instead of using linked nodes, we use an array to store the nodes with the 0th element being the head. We statically allocate the array to hold the maximum number of elements and store a back-pointer to the back of the array list. See Figure 4 for a picture of the CRDArray structure and Example 4 for a concrete example. is conjectured to influence performance, this is the only the number of nodes looked at during a full traversal. ordering we implemented. Likewise, having different This can speed up traversal-based algorithms such as implicit constraints, such as making xi x0 0 (for intersect and subset check. However, algorithms like all i) implicit, is conjectured to influence performance. clock reset, emptiness check and canonical form use O(1) access of middle nodes in DBMs (the CRDZone and CRDArray do not have O(1) access for all nodes), resulting in a performance slowdown for those CRDZone and CRDArray methods. For space, the CRDZone and CRDArray can store fewer nodes but must store the explicit indices, resulting in more space per node.

IV. ON-THE-FLY MODEL CHECKING: CONVERTING

TO A PES AND PROOF SEARCH

Using a dynamic allocation instead of our static allocation for the CRDArray array list is conjectured to save space at the expense of time.

Example 4 (Clock zone in various representations).

Consider the clock zone from Example 3, which is z = 1 x1 < 3 ^ 0 x2 5 ^ x2 x1 4.

DBM representation of z: 2x0 4x1 x2 x0 0 x0 x0 < 3 x1 x0 5 x2 x1 x1 x1

Our model checker takes in a predicate equation system (PES) (taken from [ 9 ], [ 13 ]), which is a general framework representing logical expressions that involve fixpoints and first order quantifiers. We take a timed automaton and a MES and convert it to a PES. Currently the PES model checker can only check safety properties, which involve only greatest fixpoints in both the PES and the input MES. For more information on a PES, including its syntax, semantics and how to convert a timed automaton and a MES to a PES, see [ 6 ], [ 9 ].

The model checker takes the conclusion sequent (the sequent we wish to prove) and applies proof rules in a recursive goal-driven tree-like fashion on the premise sequents, trying to prove each premise sequent until it reaches a proof rule with no premise (called a leaf) or a circularity (a previously seen premise sequent). When 4 checking a proof, we will often encounter circularity.

In general, when the circularity reached is a greatest fixpoint, we can stop and declare the proof branch valid.

For the formal conditions for circularity and the proof rules, see [ 6 ], [ 9 ].

V. EXPERIMENTS: VARIOUS DATA STRUCTURE

IMPLEMENTATIONS

We compare the DBM implementation to the CRDZone and CRDArray implementations. Each implementation uses shortest path closure to compute canonical form. The only difference in the DBM, CRDZone and CRDArray versions is the data structure implementation.

Remark 2 (On our analysis approach). We ask: what does Remark 1 (On DBM vs. CRDZone and CRDArray methods). Due to the sparse implementation and removal of implicit nodes, the CRDZone and CRDArray can improve time by reducing the number of nodes, and thus ! : : : ! xi xj uij !

: : : Fig. 3. CRDZone: A linked list with nodes in lexicographical order it mean for an implementation to perform better than of constraint xi xj uij. another? We consider consider better to be measured in the number (or percentage) of examples that one [ j j : : : jxi xj uij j : : :] system outperforms another in. The larger aim is for any implementation, if we were to know all the examples Fig. 4. CRDArray: An array list with nodes in lexicographical order that it would run (including and beyond the experiment of constraint xi xj uij. examples), we would like one implementation to perform (strictly) better for at least 51% of this hypothetical set.

This influences our analysis.

Given our meaning of better in Remark 2, we consider the median, 25% and 75% percentile values as insights into typical examples and use the histograms to get a bigger picture of the sample distribution of the performance differences for the experiment, and weigh these more heavily than the mean and standard deviation values. The mean and the standard deviation provide us with an alternative picture of the overall performance and give hints of either a unusual sample distribution (since in a symmetric distribution the mean equals the median) or the presence of potential outliers.

The benchmark choice was modeled off of [ 6 ], with the addition of a model of the generalized railroad crossing (GRC) protocol [ 26 ]. We also used all the protocols in [ 6 ], which are the Carrier Sense, Multiple Access with Collision Detection (CSMA/CD), the Fiber Distributed Data Interface (FDDI), Fischer’s Mutual Exclusion (FISCHER), the Leader Election protocol (LEADER and LBOUND) and the PATHO Operating System (PATHOS) protocol, where each of these protocols is described some in [ 6 ]. There are 53 benchmarks that ran on each implementation.

Experiments were run on a Linux machine with a 3.4 GHz Intel Pentium 4 Dual Processor (each a single core) with 4 GB RAM. Time and space measurements (maximum space used) were made using the memtime (http://www.update.uu.se/ johanb/memtime/) tool (using time elapsed and Max VSize). The data tables are in the Appendix. the DBM, CRDZone and CRDArray. Figures 5, 6 and A. Histograms and Descriptive Statistics 7 have histograms that plot the overall time and space

Running the different data structure implementations differences between the DBM, CRDZone and CRDArray with the same examples yields paired data. Hence, implementations. Bin colors and are changed to help we can take the two implementations and pair them more easily find the -0.001 to 0.001 (equal performance, example-by-example on their time and space differences since our measurement precision is 0.01 units), and -0.25 to analyze their performance. When we pair the DBM to -0.001 and 0.001 to 0.25 bins (slight differences). CRDZone samples, we take the DBM measurement and We do not use 95% confidence intervals, paired twosubtract the CRDZone measurement for the same exam- sample hypothesis (z) tests or ANOVA (Analysis of ple to get a DBM CRDZone paired data point. For Variance) because the independence assumption of the instance, the MUX-5-a paired point is -0.92s, 1.94MB, samples (the example benchmarks) does not hold. Fursince the DBM point is 1.22s, 14.67MB, and the CRD- thermore, we do not use a Wilcoxon signed-rank test Zone point is 2.14s, 12.73MB. Pairings are likewise done for the median because the symmetry assumption of the to obtain the paired samples for DBM CRDArray and distribution is not believed to hold, and thus we cannot CRDZone CRDArray. For more information, see a analyze the hypothetical benchmark distribution referred Statistics text such as [ 27 ]. to in Remark 2. We do use paired sampling since we have

Tables I, II and III contain descriptive statistics on the its only requirement—perfect correlation of the samples. paired difference in example-by-example performance of More information is in [ 27 ]. 0.25MB less space for 28 such examples and more than 0.25MB space for only 11 examples. Thus (even though 57% is not a large majority), we infer the CRDZone takes less space overall for this benchmark.

2) DBM vs. CRDArray: The CRDArray performs slower for 64% of the tested examples (at least as slow for 89%) with a median difference of 0.29s slower and a mean difference of 112.95s slower. Thus we infer the CRDArray performs slower overall for this benchmark.

The CRDArray takes more space for 77% (at least as much space for 77%) of the examples with a median amount of 2.81MB more space and mean amount of 47.75MB more. Thus we infer the CRDArray takes more space overall for this benchmark.

3) CRDZone vs. CRDArray: The CRDArray performs

slower for 77% of the tested examples (at least as slow for 100%) with a median difference of 0.21s slower and a mean difference of 45.40s slower. Thus we infer the CRDArray is slower overall for this benchmark.

The CRDArray takes more space for 100% of the examples with a median amount of 19.35MB more space and a mean amount of 82.71MB more. Thus we infer the CRDArray takes more space overall for this benchmark.

B. Analysis of Results

1) DBM vs. CRDZone: The CRDZone performs slower for 45% of the tested examples (at least as slow for 74%) with a median difference of 0.00s slower, while the CRDZone has a mean difference of 67.55s slower.

Thus, we infer the CRDZone is either slightly slower or competitive to the DBM for this benchmark, but due C. Discussion of Results to insufficient evidence (45% of the examples is not The CRDZone and CRDArray method that converts enough) do not infer that the DBM performs strictly zones to canonical form was implemented using arrayfaster than the CRDZone. based algorithms, where it temporarily converts the clock

The CRDZone takes less space for 57% of the tested zone to and from a matrix (the algorithm is similar to examples (at most as much space for 57%) with a median a DBM algorithm for those methods). It is possible that amount of 1.85MB less space and a mean amount of 34.96MB less space. The CRDZone takes at least performance can be improved by trying an algorithm that does not require copying to and from a matrix. All time [ 21 ], but this experiment compares data structures for vs. space tradeoffs were taken to save time. non-convex sets of clock valuations (unions of clock

Furthermore, we ran a CRDZone execution twice (first zones), and the comparison is across different tools with execution reported) and compared the distribution of different model checking approaches, and not the same their differences to get an idea of noise and/or mea- tool with different data structures. surement error. The differences in the histograms are larger than the differences of the noisy implementation, VII. CONCLUSIONS AND FUTURE WORK so thus we suspect the differences in performances are Here are our conclusions from the experiment: due to more than just uncertain measurement/noisy data. 1) Time: (DBM t CRDZone) <t CRDArray). For However, slight differences ( 0.25s or 0.25MB) this benchmark, we infer that the DBM is either may be due to execution noise or examples that require competitive with or slightly faster than the CRDvery little time and/or space. The PATHOS-7-b is one Zone and both perform faster than the CRDArray. such resource-light example, taking at most 0.10s and There is insufficient evidence to conclude that the 2.89MB for each implementation. In contrast, the MUX- DBM is strictly faster. 7-a example is resource-heavy, being the only example 2) Space: (CRDZone <s DBM) <s CRDArray. For to takes more than 2000s for each implementation. this benchmark, we infer that the CRDZone takes

When profiling the implementations using gprof the least amount of space and the DBM takes less (http://www.gnu.org/s/binutils/), CRDZones take more space than the CRDArray for this experiment. time than DBMs for clock resets and emptiness checks, For potential reasons for performance differences and but the invariant checking method (mostly clock zone analysis of some theoretical differences, see Remark 1. intersections) takes less time for CRDZones than DBMs. Future work is to model check least fixpoint ( )

From the data (see the Appendix), we notice that the equations, to implement all of the proof rules given in data structure implementation choice has a noticeable [ 6 ], [ 9 ] and to model check any PES. Comparing lists of influence on model checking performance for specific DBMs to a CRD or CDD to improve the performance of examples. To see this, consider the examples MUX-7-a, the expanded implementation is future work, as well as where the DBM finished 3118.94 seconds earlier than the comparing different kinds of standard forms and different CRDZone, and LEADER-100-c, where the CRDZone CRDZone node orderings. checked the example in 55% of the time required for the DBM. There are also noticeable differences relative ACKNOWLEDGEMENTS to the CRDArray.

We thank Dezhuang Zhang for providing the code base [ 6 ] and for his insights.

D. Related Work

A different way of modeling programs using discretetime is discussed in [ 4 ]. PES are in [ 9 ], and they have been used to model check various systems in [ 6 ], [ 9 ], [ 14 ]. Difference bound matrices originated from [ 15 ] and are used in various studies such as in those in [ 17 ], [ 23 ]. Other tools that can model check timed automata (safety and liveness properties) include KRONOS [ 23 ], UPPAAL [ 16 ], RED [ 18 ] and Rabbit [ 28 ]. We built upon Zhang’s implementation using predicate equation systems in [ 6 ], [ 9 ], which supports safety properties. A similar experiment involving using a reduced canonical form is in [ 20 ], which focuses on the influence of different standard clock zone forms instead of comparing list vs. array implementations.

A remark on a sparse DBM representation saving space, with neither a mention on time nor experimental data, is given in [ 17 ]. There is an experiment comparing CDDs to another BDD-like structure used by Rabbit in

Example CSMACD-3-a CSMACD-4-a FDDI-20-a FDDI-40-a FDDI-50-a MUX-5-a MUX-6-a MUX-7-a LEADER-6-a LEADER-7-a LBOUND-6-a LBOUND-7-a PATHOS-4-a GRC-3-a GRC-4-a Example CSMACD-3-a CSMACD-4-a FDDI-20-a FDDI-40-a FDDI-50-a MUX-5-a MUX-6-a MUX-7-a LEADER-6-a LEADER-7-a LBOUND-6-a LBOUND-7-a PATHOS-4-a GRC-3-a GRC-4-a For the experiments, we use three kinds of examples: Valid A Examples (in Tables IV and V): Correct system implementations with valid safety specifications.

Invalid B Examples (in Tables VI and VII): A examples with invalid specifications.

Invalid C Examples (in Tables VIII and IX): A examples with buggy implementations of the systems that do not satisfy the A specifications. 258.32 (186%)

References

[1] R. Alur , C. Courcoubetis , and D. Dill , “ Model-Checking in Dense Real-Time,” Inf. Comput. , vol. 104 , pp. 2 - 34 , 1993 .

[2] G. Behrmann , K. G. Larsen , J. Pearson , C. Weise , and W. Yi, “ Efficient Timed Reachability Analysis Using Clock Difference Diagrams ,” in CAV ' 99 , vol. 1633 . Springer Berlin / Heidelberg, 1999 .

[3] T. Henzinger , X. Nicollin , J. Sifakis , and S. Yovine , “ Symbolic Model Checking for Real-time Systems,” Inf. Comput. , vol. 111 , pp. 193 - 244 , 1994 .

[4] L. Lamport , “ Real-Time Model Checking Is Really Simple,” Correct Hardware Design and Verification Methods, pp. 162 - 175 , 2005 .

[5] O. V. Sokolsky and S. A. Smolka , “ Local model checking for real-time systems ,” in CAV '95. Springer-Verlag, 1995 , pp. 211 - 224 .

[6] D. Zhang and R. Cleaveland , “ Fast Generic Model-Checking for Data-Based Systems ,” in FORTE, F. Wang, Ed., vol. 3731 . Springer, 2005 , pp. 83 - 97 .

[7] R. Alur , “Timed Automata,” in CAV '99. London, UK: Springer-Verlag, 1999 , pp. 8 - 22 .

[8] C. Baier and J.-P. Katoen , Principles of Model Checking. Cambridge, MA: The MIT Press, 2008 .

[9] D. Zhang and R. Cleaveland , “ Fast On-the- Fly Parametric RealTime Model Checking ,” in RTSS '05. Washington, DC, USA: IEEE Computer Society, 2005 , pp. 157 - 166 .

[10] J. Bradfield and C. Stirling , “ Local Model Checking for Infinite State Spaces,” Theor. Comput. Sci. , vol. 96 , no. 1 , pp. 157 - 174 , 1992 .

[11] R. Cleaveland and B. Steffen , “ A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus,” Form. Methods Syst . Des., vol. 2 , no. 2 , pp. 121 - 147 , 1993 .

[12] E. A. Emerson and C. L. Lei , “ Efficient Model Checking in Fragments of the Propositional Mu-Calculus,” in LICS '86 . IEEE Computer Society Press, 1986 , pp. 267 - 278 .

[13] J. F. Groote and T. A. Willemse , “ Parameterised Boolean Equation Systems,” Theoretical Computer Science , vol. 343 , no. 3 , pp. 332 - 369 , 2005 .

[14] D. Zhang and R. Cleaveland , “ Efficient Temporal-Logic Query Checking for Presburger Systems ,” in ASE '05. New York, NY, USA: ACM, 2005 , pp. 24 - 33 .

[15] D. L. Dill , “ Timing Assumptions and Verification of FiniteState Concurrent Systems ,” in Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems . London, UK: Springer-Verlag, 1990 , pp. 197 - 212 .

[16] G. Behrmann , A. David , and K. G. Larsen , “ A Tutorial on Uppaal,” in Formal Methods for the Design of Real-Time Systems , vol. 3185 . Springer Berlin / Heidelberg, 2004 , pp. 200 - 236 .

[17] J. Bengtsson and W. Yi , “Timed Automata: Semantics, Algorithms,” in Lecture Notes in Computer Science, vol. 3098 . Springer, 2004 , pp. 87 - 124 .

[18] F. Wang , “ Efficient Verification of Timed Automata with BDDLike Data-Structures,” in VMCAI 2003 . London, UK: SpringerVerlag, 2003 , pp. 189 - 205 .

[19] E. M. Clarke , O. Grumberg , and D. A. Peled , Model Checking . The MIT Press, 1999 .

[20] K. Larsen , F. Larsson , P. Pettersson , and W. Yi, “ Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction,” in RTSS 1997 . IEEE Computer Society , December 1997 , pp. 14 - 24 .

[21] D. Beyer and A. Noack , “ Can decision diagrams overcome state space explosion in real-time verification? ” in FORTE 2003 . Springer Berlin / Heidelberg, 2003 , vol. 2767 , pp. 193 - 208 .

[22] E.-R. Olderog and H. Dierks , Real-Time Systems : Formal Specification and Automatic Verification . Cambridge University Press, 2008 .

[23] S. Yovine , “Model Checking Timed Automata,” in Lectures on Embedded Systems, European Educational Forum, School on Embedded Systems . London, UK: Springer-Verlag, 1998 , pp. 114 - 152 .

[24] R. K. Ahuja , T. L. Magnanti , and J. B. Orlin , Network Flows: Theory, Algorithms and Applications . Prentice-Hall, 1993 .

[25] T. H. Cormen , C. E. Leiserson , R. L. Rivest , and C. Stein , Introduction to Algorithms, 2nd ed. MIT Press, 2001 .

[26] C. L. Heitmeyer , B. G. Labaw , and R. D. Jeffords, “ A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems ,” Naval Research Laboratory, Tech. Rep. ADA462244 , 1993 .

[27] J. L. Devore , Probability and Statistics for Engineering and the Sciences, 6th ed. Duxbury Press, 2003 .

[28] D. Beyer , C. Lewerentz , and A. Noack , “ Rabbit: A tool for bddbased verification of real-time systems ,” in CAV '03. Springer Berlin / Heidelberg, 2003 , vol. 2725 , pp. 122 - 125 . in parenthesis. Time data is given to the nearest 0.01s The experimental data for the 53 example benchmarks (second) and space data is given to the nearest 0.01MB is provided in Tables IV, V, VI, VII, VIII and IX, (Megabyte). Given the percentage rounding, sometimes with the best entry(ies) in each row bolded and per- an example with slightly different performance may still centage change relative to the DBM, to the nearest %, have a 100% value .