×

The power of reachability testing for timed automata. (English) Zbl 1023.68060

Summary: The computational engine of the verification tool U consists of a collection of efficient algorithms for the analysis of reachability properties of systems. Model-checking of properties other than plain reachability ones may currently be carried out in such a tool as follows. Given a property \(\phi\) to model-check, the user must provide a test automaton \(T_{\phi}\) for it. This test automaton must be such that the original system \(S\) has the property expressed by \(\phi\) precisely when none of the distinguished reject states of \(T_{\phi}\) can be reached in the synchronized parallel composition of \(S\) with \(T_{\phi}\) . This raises the question of which properties may be analysed by UPPAAL in such a way. This paper gives an answer to this question by providing a complete characterization of the class of properties for which model-checking can be reduced to reachability testing in the sense outlined above. This result is obtained as a corollary of a stronger statement pertaining to the compositionality of the property language considered in this study. In particular, it is shown that our language is the least expressive compositional language that can express a simple safety property stating that no reject state can ever be reached.
Finally, the property language characterizing the power of reachability testing is used to provide a definition of characteristic properties with respect to a timed version of the ready simulation preorder, for nodes of \(\tau\)-free, deterministic timed automata.

MSC:

68Q45 Formal languages and automata

Keywords:

model-checking

Software:

CMC; Uppaal; Kronos; HyTech
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S.; Vickers, S., Quantales, observational logic and process semantics, Math. Struct. Comput. Sci., 3, 2, 161-227 (1993) · Zbl 0823.06011
[2] L. Aceto, P. Bouyer, A. Burgueño, K.G. Larsen, The power of reachability testing for timed automata, in: Proc. 18th Conf. on Found. of Software Technology and Theoretical Computer Science (FST&TCS’98), Lecture Notes in Computer Science, Vol. 1530, Springer, Berlin, 1998. pp. 245-256. Also available as BRICS Report RS-98-48, Aalborg University, 1998.; L. Aceto, P. Bouyer, A. Burgueño, K.G. Larsen, The power of reachability testing for timed automata, in: Proc. 18th Conf. on Found. of Software Technology and Theoretical Computer Science (FST&TCS’98), Lecture Notes in Computer Science, Vol. 1530, Springer, Berlin, 1998. pp. 245-256. Also available as BRICS Report RS-98-48, Aalborg University, 1998.
[3] L. Aceto, A. Burgueño, K.G. Larsen, Model-checking via reachability testing for timed automata, in: Proc. 4th Internat. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), Lecture Notes in Computer Science, Vol. 1384, Springer, Berlin, 1998. pp. 263-280. Also available as BRICS Report RS-97-29, Aalborg University, 1997.; L. Aceto, A. Burgueño, K.G. Larsen, Model-checking via reachability testing for timed automata, in: Proc. 4th Internat. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), Lecture Notes in Computer Science, Vol. 1384, Springer, Berlin, 1998. pp. 263-280. Also available as BRICS Report RS-97-29, Aalborg University, 1997.
[4] Aceto, L.; Laroussinie, F., Is your model-checker on time?, J. Logic Algebraic Programming, 52-53, 7-51 (2002) · Zbl 1008.68030
[5] Alur, R.; Courcoubetis, C.; Dill, D., Model-checking in dense real-time, Inform. and Comput., 104, 1, 2-34 (1993) · Zbl 0783.68076
[6] Alur, R.; Dill, D., A theory of timed automata, Theoret. Comput. Sci., 126, 2, 183-235 (1994) · Zbl 0803.68071
[7] T. Amnell, G. Behrmann, J. Bengtsson, P.R. D’Argenio, A. David, A. Fehnker, T. Hune, B. Jeannet, K.G. Larsen, O. öller, P. Pettersson, C. Weise, Yi.W. UPPAAL; T. Amnell, G. Behrmann, J. Bengtsson, P.R. D’Argenio, A. David, A. Fehnker, T. Hune, B. Jeannet, K.G. Larsen, O. öller, P. Pettersson, C. Weise, Yi.W. UPPAAL
[8] Andersen, H. R., Partial model-checking (extended abstract), (Proc. 10th IEEE Symp. Logic in Computer Science (LICS’95) (1995), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 398-407
[9] Bengtsson, J.; Griffioen, W. D.; Kristoffersen, K. J.; Larsen, K. G.; Larsson, F.; Pettersson, P.; Yi, W., Verification of an audio protocol with bus collision using UPPAAL, (Proc. 8th Internat. Conf. on Computer Aided Verification (CAV’96). Proc. 8th Internat. Conf. on Computer Aided Verification (CAV’96), Lecture Notes in Computer Science, Vol. 1102 (1996), Springer: Springer Berlin), 244-256
[10] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, Y. Wang, C. Weise, New generation of UPPAAL; J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, Y. Wang, C. Weise, New generation of UPPAAL
[11] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi, UPPAAL; J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi, UPPAAL
[12] Bérard, B.; Fribourg, L., Automatic verification of a parametric real-time program: the ABR conformance protocol, (Proc. 11th Internat. Conf. on Computer Aided Verification (CAV’99), Vol. 1633 (1999), Springer: Springer Berlin), 96-107 · Zbl 1046.68501
[13] B. Bérard, L. Sierra, Comparing verification with HYECHRONOSPPAAL; B. Bérard, L. Sierra, Comparing verification with HYECHRONOSPPAAL
[14] Bloom, B.; Istrail, S.; Meyer, A. R., Bisimulation can’t be traced, J. Assoc. Comput. Mach., 42, 1, 232-268 (1995) · Zbl 0886.68027
[15] Bouyer, P.; Dufourd, C.; Fleury, E.; Petit, A., Are timed automata updatable?, (Proc. 12th Internat. Conf. on Computer Aided Verification (CAV’2000). Proc. 12th Internat. Conf. on Computer Aided Verification (CAV’2000), Lecture Notes in Computer Science, Vol. 1855 (2000), Springer: Springer Berlin), 464-479 · Zbl 0974.68084
[16] Bozga, M.; Daws, C.; Maler, O.; Olivero, A.; Tripakis, S.; Yovine, S., Kronos, A model-checking tool for real-time systems, (Proc. 10th Internat. Conf. on Computer Aided Verification (CAV’98). Proc. 10th Internat. Conf. on Computer Aided Verification (CAV’98), Lecture Notes in Computer Science, Vol. 1427 (1998), Springer: Springer Berlin), 546-550
[17] Cerans, K., Decidability of bisimulation equivalences for parallel timer processes, (Proc. 4th Internat. Conf. on Computer Aided Verification (CAV’92). Proc. 4th Internat. Conf. on Computer Aided Verification (CAV’92), Lecture Notes in Computer Science, Vol. 663 (1992), Springer: Springer Berlin), 302-315
[18] Courcoubetis, C.; Yannakakis, M., Minimum and maximum delay problems in real-time systems, Formal methods in System Design, 385-415 (1992) · Zbl 0777.68045
[19] Daws, C.; Yovine, S., Two examples of verification of multivariate timed automata with KRONOS, (Proc. 16th IEEE Real-Time Systems Symposium (RTSS’95) (1995), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 66-75
[20] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518
[21] Gabbay, D. M.; Pnueli, A.; Shelah, S.; Stavi, J., On the temporal analysis of fairness, (Proc. 6th ACM Symp. on Principles of Programming Languages. Proc. 6th ACM Symp. on Principles of Programming Languages, Lecture Notes in Computer Science, Vol. 1384 (1980), Springer: Springer Berlin), 163-173
[22] Henzinger, T. A.; Ho, P.-H.; Wong-Toi, H., HYTECH: the next generation, (Proc. 16th IEEE Real-Time Systems Symposium (RTSS’95) (1995), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 56-65
[23] T. Henzinger, P. Ho, H. Wong-Toi, HyTech: a model checker for hybrid systems, in: Software Tools for Technology Transfer, 1997, pp. 110-122.; T. Henzinger, P. Ho, H. Wong-Toi, HyTech: a model checker for hybrid systems, in: Software Tools for Technology Transfer, 1997, pp. 110-122. · Zbl 1060.68603
[24] T.A. Henzinger, P.W. Kopke, Undecidability results for hybrid systems, in: Proc. Workshop on Hybrid Systems and Autonomous Control, 1994. Also appeared as Cornell University Technical Report TR95-1483.; T.A. Henzinger, P.W. Kopke, Undecidability results for hybrid systems, in: Proc. Workshop on Hybrid Systems and Autonomous Control, 1994. Also appeared as Cornell University Technical Report TR95-1483.
[25] T.A. Henzinger, P.W. Kopke, A. Puri, P. Varaiya, What’s decidable about hybrid automata? in: Proc. 27th ACM Symp. Theory of Computing (STOC’95), 1995, pp. 373-382. Also appeared as Cornell University Technical Report TR95-1541.; T.A. Henzinger, P.W. Kopke, A. Puri, P. Varaiya, What’s decidable about hybrid automata? in: Proc. 27th ACM Symp. Theory of Computing (STOC’95), 1995, pp. 373-382. Also appeared as Cornell University Technical Report TR95-1541. · Zbl 0978.68534
[26] Ho, P.-H.; Wong-Toi, H., Automated analysis of an audio control protocol, (Proc. 7th. Internat. Conf. on Computer Aided Verification (CAV’95). Proc. 7th. Internat. Conf. on Computer Aided Verification (CAV’95), Lecture Notes in Computer Science, Vol. 939 (1995), Springer: Springer Berlin), 381-394
[27] T.K. Iversen, K.J. Kristoffersen, K.G. Larsen, M. Laursen, R.G. Madsen, S.K. Mortensen, P. Pettersson, C.B. Thomasen, Model-checking real-time control programs—verifying LEGO mindstorms systems using UPPAAL; T.K. Iversen, K.J. Kristoffersen, K.G. Larsen, M. Laursen, R.G. Madsen, S.K. Mortensen, P. Pettersson, C.B. Thomasen, Model-checking real-time control programs—verifying LEGO mindstorms systems using UPPAAL
[28] H.E. Jensen, K.G. Larsen, A. Skou, Modelling and analysis of a collision avoidance protocol using SPIN and UPPAAL; H.E. Jensen, K.G. Larsen, A. Skou, Modelling and analysis of a collision avoidance protocol using SPIN and UPPAAL · Zbl 0880.68085
[29] Kleene, S. C., Representation of events in nerve nets and finite automata, (Automata Studies (1956), Princeton University Press: Princeton University Press Princeton, NJ), 3-41 · Zbl 0061.01003
[30] K.J. Kristoffersen, P. Pettersson, Modelling and analysis of a steam generator using UPPAAL; K.J. Kristoffersen, P. Pettersson, Modelling and analysis of a steam generator using UPPAAL
[31] F. Laroussinie, K.G. Larsen, Compositional model-checking of real-time systems, in: Proc. 6th Internat. Conf. on Theory of Concurrency (CONCUR’95), Lecture Notes in Computer Science, Vol. 962, Springer, Berlin, 1995, pp. 529-539. Also available as BRICS Report RS-95-19, Aalborg University, 1995.; F. Laroussinie, K.G. Larsen, Compositional model-checking of real-time systems, in: Proc. 6th Internat. Conf. on Theory of Concurrency (CONCUR’95), Lecture Notes in Computer Science, Vol. 962, Springer, Berlin, 1995, pp. 529-539. Also available as BRICS Report RS-95-19, Aalborg University, 1995.
[32] F. Laroussinie, K.G. Larsen, CMC: a tool for compositional model-checking of real-time systems, in: Proc. IFIP Joint Internat. Conf. on Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV’98), Kluwer Academic, Dordrecht, 1998, pp. 439-456.; F. Laroussinie, K.G. Larsen, CMC: a tool for compositional model-checking of real-time systems, in: Proc. IFIP Joint Internat. Conf. on Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV’98), Kluwer Academic, Dordrecht, 1998, pp. 439-456.
[33] F. Laroussinie, K.G. Larsen, C. Weise, From timed automata to logic—and back, in: Proc. 20th Internat. Symp. on Mathematical Foundations of Computer Science (MFCS’95), Lecture Notes in Computer Science, Vol. 969, Springer, Berlin, 1995, pp. 27-41. Also available as BRICS Report RS-95-2, Aalborg University, 1995.; F. Laroussinie, K.G. Larsen, C. Weise, From timed automata to logic—and back, in: Proc. 20th Internat. Symp. on Mathematical Foundations of Computer Science (MFCS’95), Lecture Notes in Computer Science, Vol. 969, Springer, Berlin, 1995, pp. 27-41. Also available as BRICS Report RS-95-2, Aalborg University, 1995. · Zbl 1193.03069
[34] Larsen, K. G., Proof systems for satisfiability in Hennessy-Milner logic with recursion, Theoret. Comput. Sci., 72, 2-3, 265-288 (1990) · Zbl 0698.68014
[35] Larsen, K. G.; Pettersson, P.; Yi, W., UPPAAL in a Nutshell, J. Software Tools Technol. Transfer, 1, 1-2, 134-152 (1997) · Zbl 1060.68577
[36] Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Inform. and Comput., 94, 1-28 (1991) · Zbl 0756.68035
[37] Larsen, K. G.; Xinxin, L., Compositionality through an operational semantics of contexts, J. Logic Comput., 1, 761-795 (1991) · Zbl 0738.68056
[38] Margenstern, M., Frontier between decidability and undecidabilitya survey, Theoret. Comput. Sci., 231, 2, 217-251 (2000) · Zbl 0956.03041
[39] Milner, R., Communication and Concurrency (1989), Prentice-Hall International: Prentice-Hall International Englewood Cliffs, NJ · Zbl 0683.68008
[40] Olivero, A.; Yovine, S., KRONOS: A Tool for Verifying Real-Time Systems. User’s Guide and Reference Manual (1993), VERIMAG: VERIMAG Grenoble, France
[41] Steffen, B.; Ingólfsdóttir, A., Characteristic formulae for processes with divergence, Inform. and Comput., 110, 1, 149-163 (1994) · Zbl 0804.68097
[42] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 285-309 (1955) · Zbl 0064.26004
[43] Taşiran, S.; Brayton, R. K., STARI: a case study in compositional verification and hierarchical timing verification, (Proc. 9th Internat. Conf. on Computer Aided Verification (CAV’97). Proc. 9th Internat. Conf. on Computer Aided Verification (CAV’97), Lecture Notes in Computer Science, Vol. 1254 (1997), Springer: Springer Berlin), 191-201
[44] Vardi, M. Y.; Wolper, P., An automata-theoretic approach to automatic program verification, (Proc. 1st Ann. Symp. on Logic in Computer Science (LICS’86) (1986), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 322-331
[45] P. Wolper, Where could SPIN go next? A unifying approach to exploring infinite state spaces. Slides for an invited talk at the 1997 SPIN Workshop, Enschede, The Netherlands, 1997. Available at the URL http://www.montefiore.ulg.ac.be/ pw/papers/psfiles/SPIN4-97.ps; P. Wolper, Where could SPIN go next? A unifying approach to exploring infinite state spaces. Slides for an invited talk at the 1997 SPIN Workshop, Enschede, The Netherlands, 1997. Available at the URL http://www.montefiore.ulg.ac.be/ pw/papers/psfiles/SPIN4-97.ps
[46] Yi, W., Real-time behaviour of asynchronous agents, (Proc. 1st Internat. Conf. on Theory of Concurrency (CONCUR’90). Proc. 1st Internat. Conf. on Theory of Concurrency (CONCUR’90), Lecture Notes in Computer Science, Vol. 458 (1990), Springer: Springer Berlin), 502-520
[47] W. Yi, A calculus of real-time systems, Ph.D. Thesis, Chalmers University of Technology, Göteborg, Sweden, 1991.; W. Yi, A calculus of real-time systems, Ph.D. Thesis, Chalmers University of Technology, Göteborg, Sweden, 1991.
[48] Yovine, S., KRONOSa verification tool for real-time systems, J. Software Tools Technol. Transfer, 1, 1-2, 123-133 (1997) · Zbl 1060.68606
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.