Abstract
Transition systems have been intensively applied to the modeling of complex systems. Their safety properties can be verified using model-checking procedures based on an iterative computation of least or greatest fixed points. The approach has to face two main difficulties: the complexity of computations on the data domain and the termination of the iterative algorithm. In many cases an analysis of the transition system can be exploited in order to speed up the calculus. Meta-transitions are are over-approximations of transition relations that lead in one step to an superset of the set of the the states that can be reached by an infinite trajectory. Using polynomials, we compute meta-transitions for complex transition systems. Finally, we illustrate this method on a train controller.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer Academic Press, Netherlands (1993)
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: A declarative language for programming synchronous systems. In: Proceedings of the 14th ACM Symposium on Principles of Programming Languages. ACM Press, New York (1987)
Benveniste, A., LeGuernic, P.: Hybrid dynamical systems theory and the SIGNAL language. IEEE Transactions on Automatic ControlĀ 35, 535ā546 (1990)
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, pp. 278ā292. IEEE Computer Society Press, Los Alamitos (1996)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Queille, J.P.P., Sifakis, J.: Fairness and related properties in transition systems: a temporal logic to deal with fairness. Acta InformaticaĀ 19, 195ā220 (1983)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol.Ā B, pp. 995ā1072. Elsevier Science Publishers, Amsterdam (1990)
Halbwachs, N., Lagnier, F., Raymond., P.: Synchronous observers and the verification of reactive systems. In: Enschede, N. (ed.) Univ. Twente; Proceedings of Third International Conference on Algebraic Methodology and Software Technology, AMAST, pp. 131ā144 (1993)
Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Proc. 10th International Computer Aided Verification Conference, pp. 319ā331 (1998)
Cousot, P., Cousot, R.: Comparing the Galois Connection and Widening/ Narrowing Approaches to Abstract Interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol.Ā 631, pp. 269ā295. Springer, Heidelberg (1992)
Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.Ā 1579, pp. 223ā239. Springer, Heidelberg (1999)
Henzinger, T.A., Rusu, V.: Reachability verification for hybrid automata. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol.Ā 1386, pp. 190ā204. Springer, Heidelberg (1998)
Boigelot, B.: Symbolic Method for Exploring Infinite State Spaces. PhD thesis, UniversitĆ© de LiĆØge (1997ā1998)
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast Acceleration of Symbolic Transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.Ā 2725, pp. 118ā121. Springer, Heidelberg (2003)
Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.Ā 2623, pp. 514ā525. Springer, Heidelberg (2003)
Ireland, A., Bundy, A.: Extensions to a generalization critic for inductive proof. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.Ā 1104, pp. 47ā61. Springer, Heidelberg (1996)
Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1987)
Bensalem, S., Caspi, P., Parent-Vigouroux, C., Dumas, C.: A methodology for proving control systems with Lustre and PVS. In: Weinstock, C.B., Rushby, J. (eds.) Dependable Computing for Critical Applicationsā7, San Jose, CA. Dependable Computing and Fault Tolerant Systems, vol.Ā 12, pp. 89ā107. IEEE Computer Society Press, Los Alamitos (1999)
Dumas, C.: MĆ©thodes dĆ©ductives pour la preuve de programmes LUSTRE. PhD thesis, UniversitĆ© Joseph Fourier ā Grenoble 1 (2002)
Maidl, M.: A unifying model checking approach for safety properties of parameterized systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.Ā 2102, pp. 311ā323. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
Ā© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Musset, J., Rusinowitch, M. (2003). Computing Meta-transitions for Linear Transition Systems with Polynomials. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive