Skip to main content
SpringerLink
Log in
Book cover

International Symposium of Formal Methods Europe

FME 2003: FME 2003: Formal Methods pp 562–581Cite as

Computing Meta-transitions for Linear Transition Systems with Polynomials

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2805))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer Academic Press, Netherlands (1993)

    Book  Google Scholar 

  2. 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)

    Google Scholar 

  3. Benveniste, A., LeGuernic, P.: Hybrid dynamical systems theory and the SIGNAL language. IEEE Transactions on Automatic Control 35, 535–546 (1990)

    Article  MathSciNet  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)

    MATH  Google Scholar 

  6. 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)

    Article  MathSciNet  Google Scholar 

  7. 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)

    Google Scholar 

  8. 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)

    Google Scholar 

  9. 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)

    Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223–239. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. Boigelot, B.: Symbolic Method for Exploring Infinite State Spaces. PhD thesis, Université de Liège (1997–1998)

    Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 514–525. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1987)

    MATH  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. Dumas, C.: Méthodes déductives pour la preuve de programmes LUSTRE. PhD thesis, Université Joseph Fourier – Grenoble 1 (2002)

    Google Scholar 

  20. 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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Projet CASSIS, Inria-Lorraine, Nancy, France

    Julien Musset & Michaël Rusinowitch

Authors
  1. Julien Musset
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michaël Rusinowitch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Communication Engineering, Graduate School of Information Science and Electrical Engineering, Kyushu University, 6-10-1-Hakozaki, Higashi-ku, 812-8581, Fukuoka, Japan

    Keijiro Araki

  2. Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, ISTI - CNR, Pisa, Italy

    Stefania Gnesi

  3. Dipartimento di Elettronica e Informazione, Politecnico di Milano, Italy

    Dino Mandrioli

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation