zbMATH — the first resource for mathematics

Bounded model checking for timed automata. (English) Zbl 1270.68177
Vogler, Walter (ed.) et al., MTCS ’02. Proceedings of the 3rd international workshop on models for time-critical systems (CONCUR 2002 satellite workshop), Brno, Czech Republic, August 24, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 68, No. 5, 116-134 (2003).
Summary: Given a timed automaton \(M\), a linear temporal logic formula \(\varphi\), and a bound \(k\), bounded model checking for timed automata determines if there is a falsifying path of length \(k\) to the hypothesis that \(M\) satisfies the specification \(\varphi\). This problem can be reduced to the satisfiability problem for Boolean constraint formulas over linear arithmetic constraints. We show that bounded model checking for timed automata is complete, and we give lower and upper bounds for the length \(k\) of counterexamples. Moreover, we define bounded model checking for networks of timed automata in a compositional way.
For the entire collection see [Zbl 1270.68035].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
03B44 Temporal logic
HyTech; ICS; Kronos; PVS; Tempo; Uppaal
Full Text: Link
[1] Alur R., ”Techniques for Automatic Verification of Real-Time Systems,” Ph.D. thesis, Stanford University (1991).
[2] Alur, R.: Timed automata. Lecture notes in computer science 1633, 8-22 (1999) · Zbl 1046.68574
[3] Alur, R.; Courcoubetis, C.; Dill, D.: Model-checking for real-time systems. 5th symp. On logic in computer science (LICS 90), 414-425 (1990)
[4] Alur, R.; Dill, D. L.: A theory of timed automata. Theoretical computer science 126, 183-235 (1994) · Zbl 0803.68071
[5] Audemard G., A. Cimatti, A. Kornilowicz and R. Sebastiani, Bounded model checking for timed systems, Proceedings of the 2nd Workshop on Real-Time Tools (RT-TOOLS’2002) (2002). · Zbl 1037.68549
[6] Barrett, C. W., D. L. Dill and A. Stump, Checking satisfiability of first-order formulas by incremental translation to SAT (2002), to be presented at CAV 2002. · Zbl 1010.68531
[7] Bryant, R. E.: Graph-based algorithms for Boolean function manipulation. IEEE transactions on computers 35, 677-691 (1986) · Zbl 0593.94022
[8] Clarke, E. M.; Biere, A.; Raimi, R.; Zhu, Y.: Bounded model checking using satisfiability solving. Formal methods in system design 19, 7-34 (2001) · Zbl 0985.68038
[9] Copty, F., L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella and M. Vardi, Benefits of bounded model checking in an industrial setting, in: Computer-Aided Verification, CAV 2001, Lecture Notes in Computer Science 2101 (2001), pp. 436–453. · Zbl 0991.68637
[10] Dams, D. R., ”Abstract Interpretation and Partition Refinement for Model Checking,” Ph.D. thesis, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands (1996). · Zbl 0848.68060
[11] Daws, C.; Olivero, A.; Tripakis, S.; Yovine, S.: The tool KRONOS. Lecture notes in computer science 1066, 208-219 (1996)
[12] de Moura L. and H. Rueß, Lemmas on demand for satisfiability solvers, in: Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002), Cincinnati, Ohio, 2002.
[13] de Moura L., H. Rueß and M. Sorea, Lazy theorem proving for bounded model checking over infinite domains, in: A. Voronkov, editor, 18th Conference on Automated Deduction (CADE), Lecture Notes in Computer Science 2392 (2002), pp. 438–455. · Zbl 1072.68602
[14] Dill D., Timing assumptions and verification of finite-state concurrent systems, in: Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407 (1989), pp. 197–212.
[15] Fillia\checktre J.-C., S. Owre, H. Rueß and N. Shankar, ICS: Integrated canonizer and solver, in: G. Berry, H. Comon and A. Finkel, editors, Proceedings of CAV’2001, Lecture Notes in Computer Science 2102 (2001), pp. 246–249. · Zbl 0996.68559
[16] Gerth, R.; Peled, D.; Vardi, M.; Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. Protocol specification testing and verification, 3-18 (1995)
[17] Henzinger, T. A.; Ho, P. -H.; Wong-Toi, H.: HYTECH: A model checker for hybrid systems. Lecture notes in computer science 1254, 460-463 (1997) · Zbl 1060.68603
[18] Henzinger, T. A.; Nicollin, X.; Sifakis, J.; Yovine, S.: Symbolic model checking for real-time systems. Information and computation 111, 193-244 (1994) · Zbl 0806.68080
[19] Kupferman, O.; Vardi, M. Y.: Model checking of safety properties. Formal methods in system design 19, 291-314 (2001) · Zbl 0995.68061
[20] Lamport, L.: A fast mutual exclusion algorithm. ACM transactions on computer systems 5, 1-11 (1987)
[21] Larsen, K. G.; Pearson, J.; Weise, C.; Yi, W.: Clock difference diagrams. Nordic journal of computing 6, 271-298 (1999) · Zbl 0937.68086
[22] Larsen, K. G.; Pettersson, P.; Yi, W.: UPPAAL in a nutshell. Int. journal on software tools for technology transfer 1, 134-152 (1997) · Zbl 1060.68577
[23] M\oslashller J., J. Lichtenberg, H. R. Andersen and H. Hulgaard, Difference decision diagrams, in: Computer Science Logic, The IT University of Copenhagen, Denmark, 1999. · Zbl 0944.68040
[24] Möller, M. O.; Rueß, H.; Sorea, M.: Predicate abstraction for dense real-time systems. Electronic notes in theoretical computer science 65 (2002) · Zbl 1270.68174
[25] Niebert P., M. Mahfoudh, E. Asarin, M. Bozga, N. Jain and O. Maler, Verification of timed automata via satisfiability checking, in: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT), Lecture Notes in Computer Science (2002). · Zbl 1278.68187
[26] Owre S., J. M. Rushby and N. Shankar, PVS: A prototype verification system, in: 11th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence 607 (1992), pp. 748–752.
[27] Penczek W., B. Wozna and A. Zbrzezny, Towards bounded model checking for the universal fragment of TCTL, in: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT), Lecture Notes in Computer Science (2002). · Zbl 1278.68192
[28] Shostak, R.: Deciding linear inequalities by computing loop residues. Journal of the ACM 28, 769-779 (1981) · Zbl 0468.68073
[29] Sistla, A. P.: Safety, liveness and fairness in temporal logic. Formal aspects of computing 6, 495-512 (1994) · Zbl 0820.68077
[30] Sorea M., Tempo: A model-checker for event-recording automata, in: Proceedings of RT-TOOLS’01, Aalborg, Denmark, 2001, also available as Technical Report SRI-CSL-01–04, Computer Science Laboratory, SRI International, Menlo Park, CA, 2001. URL http://www.csl.sri.com/papers/csl-01-04/
[31] Tripakis, S.; Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal methods in system design 18, 25-68 (2001) · Zbl 0971.68096
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.