Skip to main content
SpringerLink
Log in

Hybrid Systems with Finite Bisimulations

  • Conference paper
  • First Online:
Hybrid Systems V (HS 1997)

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

Included in the following conference series:

Abstract

The theory of formal verification is one of the main approaches to hybrid system analysis. Decidability questions for verification algorithms are obtained by constructing finite, reachability preserving quotient systems called bisimulations. In this paper, we use recent results from stratification theory, subanalytic sets, and model theory in order to extend the state-of-the-art results on the existence of bisimulations for certain classes of planar hybrid systems.

Research supported by the Army Research Office under grants DAAH 04-95-1-0588 and DAAH 04-96-1-0341.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Coucoubetis, N. Halbwachs, T.A. Henzinger, P.H. Ho, X. Nicolin, A. Olivero, J. Sifakis, and S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science 138 (1995), 3–34.

    Article  MathSciNet  Google Scholar 

  2. R. Alur and D.L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994), 183–235.

    Article  MathSciNet  Google Scholar 

  3. R. Alur, T.A. Henzinger, and E.D. Sontag (eds.), Hybrid systems III, Lecture Notes in Computer Science, vol. 1066, Springer-Verlag, 1996.

    Google Scholar 

  4. P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry (eds.), Hybrid systems II, Lecture Notes in Computer Science, vol. 999, Springer-Verlag, 1995.

    Google Scholar 

  5. P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry (eds.), Hybrid systems IV, Lecture Notes in Computer Science, vol. 1273, Springer-Verlag, 1997.

    Google Scholar 

  6. E. Bierstone and P.D. Milman, Semianalytic and subanalytic sets, Inst. Hautes Études Sci. Publ. Math. 67 (1988), 5–42.

    Article  MathSciNet  Google Scholar 

  7. P.E. Caines and Y.J. Wei, The hierarchical lattices of a finite state machine, Systems and Control Letters 25 (1995), 257–263.

    Article  MathSciNet  Google Scholar 

  8. ______, Hierarchical hybrid control systems: A lattice theoretic formulation, IEEE Transactions on Automatic Control: Special Issue on Hybrid Systems 43 (1998), no.4, 501–508.

    Article  MathSciNet  Google Scholar 

  9. K. Cerans and J. Viksna, Deciding reachability for planar multi-polynomial systems, Hybrid Systems III (R. Alur, T. Henzinger, and E.D. Sontag, eds.), Lecture Notes in Computer Science, vol. 1066, Springer Verlag, Berlin, Germany, 1996, pp. 389–400.

    Chapter  Google Scholar 

  10. R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel (eds.), Hybrid systems, Lecture Notes in Computer Science, vol. 736, Springer-Verlag, 1993.

    Google Scholar 

  11. T.A. Henzinger, Hybrid automata with finite bisimulations, ICALP 95: Automata, Languages, and Programming (Z. Fülöop and F. Gécseg, eds.), Springer-Verlag, 1995, pp. 324–335.

    Google Scholar 

  12. T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya, What’s decidable about hybrid automata?, Proceedings of the 27th Annual Symposium on Theory of Computing, ACM Press, 1995, pp. 373–382.

    Google Scholar 

  13. H. Hironaka, Subanalytic sets, In Number Theory, Algebraic Geometry, and Commutative Algebra, in honor of Y. Akizuki, Kinokuniya Publications, 1973, pp. 453–493.

    Google Scholar 

  14. W. Hodges, A shorter model theory, Cambridge University Press, 1997.

    Google Scholar 

  15. G. Lafferriere, G.J. Pappas, and S. Sastry, Subanalytic stratifications and bisimulations, Hybrid Systems: Computation and Control (T. Henzinger and S. Sastry, eds.), Lecture Notes in Computer Science, vol. 1386, Springer Verlag, Berlin, 1998, pp. 205–220.

    Chapter  Google Scholar 

  16. A. Macintyre and A.J. Wilkie, On the decidability of the real exponential field, Kreiseliana: About and around Georg Kreisel, A.K. Peters, 1996, pp. 441–467.

    Google Scholar 

  17. O. Maler (ed.), Hybrid and real-time systems, Lecture Notes in Computer Science, vol. 1201, Springer-Verlag, 1997.

    Google Scholar 

  18. G.J. Pappas, G. Lafferriere, and S. Sastry, Hierarchically consistent control systems, Proceedings of the 37th IEEE Conference in Decision and Control, Tampa, FL, December 1998, Submitted.

    Google Scholar 

  19. A. Puri and P. Varaiya, Decidability of hybrid systems with rectangular differential inclusions, Computer Aided Verification, 1994, pp. 95–104.

    Google Scholar 

  20. Héctor J. Sussmann, Subanalytic sets and feedback control, Journal of Differential Equations 31 (1979), no. 1, 31–52.

    Article  MathSciNet  Google Scholar 

  21. ______, Real-analytic desingularization and subanalytic sets: An elementary approach, Transactions of the American Mathematical Society 317 (1990), no. 2, 417–461.

    MathSciNet  MATH  Google Scholar 

  22. A. Tarski, A decision method for elementary algebra and geometry, second ed., University of California Press, 1951.

    Google Scholar 

  23. D. van Dalen, Logic and structure, third ed., Springer-Verlag, 1994.

    Google Scholar 

  24. L. van den Dries and C. Miller, On the real exponential field with restricted analytic functions, Israel Journal of Mathematics 85 (1994), 19–56.

    Article  MathSciNet  Google Scholar 

  25. A. J. Wilkie, Model completeness results for expansions of the ordered field of real numbers by restricted pfaffian functions and the exponential function, Journal of the American Mathematical Society 9 (1996), no. 4, 1051–1094.

    Article  MathSciNet  Google Scholar 

  26. A.J. Wilkie, A general theorem of the complement and some new o-minimal structures, Preprint, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematical Sciences, Portland State University, Portland, OR, 97207, USA

    Gerardo Lafferriere

  2. Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, Berkeley, CA, 94720, USA

    George J. Pappas & Shankar Sastry

Authors
  1. Gerardo Lafferriere
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. George J. Pappas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shankar Sastry
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electrical Engineering, University of Notre Dame, Notre Dame, IN, 46556, USA

    Panos Antsaklis  & Michael Lemmon  & 

  2. Hynomics Corporation, 10632 NE 37th Circle, Building 23, Kirkland, WA, 98033, USA

    Wolf Kohn

  3. Department of Mathematics, Cornell University, 217, White Hall, Ithaca, NY, 14853, USA

    Anil Nerode

  4. Electronic Research Laboratory, University of California at Berkeley, 253 Cory Hall, Berkeley, CA, 94720, USA

    Shankar Sastry

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lafferriere, G., Pappas, G.J., Sastry, S. (1999). Hybrid Systems with Finite Bisimulations. In: Antsaklis, P., Lemmon, M., Kohn, W., Nerode, A., Sastry, S. (eds) Hybrid Systems V. HS 1997. Lecture Notes in Computer Science, vol 1567. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49163-5_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-49163-5_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65643-2

  • Online ISBN: 978-3-540-49163-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation