Skip to main content
SpringerLink
Log in
Book cover

International Hybrid Systems Workshop

HS 1997: Hybrid Systems V pp 38–69Cite as

On Hybrid Systems and the Modal µ-calculus

  • Conference paper
  • First Online:

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

Abstract

We start from a basic and fruitful idea in current work on the formal analysis and verification of hybrid and real-time systems: the uniform representation of both sorts of state dynamics — both continuous evolution within a control mode, and the effect of discrete jumps between control modes — as abstract transition relations over a hybrid space X ⊆ Q × ℝn, where Q is a finite set of control modes. The resulting “machine” or transition system model is currently analyzed using the resources of concurrent and reactive systems theory and temporal logic verification, abstracted from their original setting of finite state spaces and purely discrete transitions. One such resource is the propositional μ-calculus: a richly expressive formal logic of transition system models (of arbitrary cardinality), which subsumes virtually all temporal and modal logics. The key move here is to view the transition system models of hybrid automata not merely as some form of “discrete abstraction”, but rather as a skeleton which can be fleshed out by imbuing the state space with topological, metric tolerance or other structure. Drawing on the resources of modal logics, we give explicit symbolic representation to such structure in polymodal logics extending the modal μ-calculus. The result is a logical formalism in which we can directly and simply express continuity properties of transition relations and metric tolerance properties such as “being within distance ∈” of a set. Moreover, the logics have sound and complete deductive proof systems, so assumptions of continuity or tolerance can be used as hypotheses in deductive verification. By also viewing transition relations in their equivalent form as set-valued functions, and drawing on the resources of set-valued analysis and dynamical systems theory, we open the way to a richer formal analysis of robustness and stability for hybrid automata and related classes of systems.

Research supported by the ARO under the MURI program “Integrated Approach to Intelligent Systems”, grant no. DAA H04-96-1-0341.

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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Akin, The General Topology of Dynamical Systems, Graduate Studies in Mathematics 1 (American Mathematical Society, Providence, 1993).

    Google Scholar 

  2. R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine, “The Algorithmic Analysis of Hybrid Systems”, Theoretical Computer Science138 (1995) 3–34.

    Article  MathSciNet  Google Scholar 

  3. R. Alur and D. L. Dill, “A Theory of Timed Automata”, Theoretical Computer Science126 (1994) 183–235.

    Article  MathSciNet  Google Scholar 

  4. R. Alur, T. A. Henzinger and P.-H. Ho, “Automatic Symbolic Veri_cation of Embedded Systems”, IEEE Transactions on Software Engineering22 (1996) 181–201.

    Article  Google Scholar 

  5. S. Ambler, M. Kwiatkowska and N. Measor, “Duality and the Completeness of the Modal µ-calculus”, Theoretical Computer Science151 (1995) 3–27.

    Article  MathSciNet  Google Scholar 

  6. J-P. Aubin and H. Frankasowa, Set-Valued Analysis (Birkhäuser, Boston, 1990).

    Google Scholar 

  7. J-P. Aubin, Viability Theory (Birkhäuser, Boston, 1991).

    MATH  Google Scholar 

  8. M. M. Bonsangue and M. Z. Kwiatkowska, “Reinterpreting the Modal µ-calculus”, in A. Ponse, M. de Rijke and Y. Venema (eds.), Modal Logic and Process Algebra, CSLI Lecture Notes 53 (CLSI Publications, Stanford, 1995); 65–83.

    Google Scholar 

  9. B. F. Chellas, Modal Logic: An Introduction (Cambridge University Press, 1980.

    Google Scholar 

  10. J. M. Davoren, Modal Logics for Continuous Dynamics, PhD dissertation, Department of Mathematics, Cornell University, January 1998.

    Google Scholar 

  11. J. M. Davoren, “Topologies, Continuity and Bisimulations”, presented at Fixed Points in Computer Science, Brno, August 1998; submitted for publication.

    Google Scholar 

  12. J. M. Davoren, “On Continuous Dynamics and Modal Logics”, in preparation.

    Google Scholar 

  13. C. Daws, A. Olivero, S. Tripakis and S. Yovine, “The Tool Kronos”, in R. Alur, T. A. Henzinger and E. D. Sontag (eds.), Hybrid Systems III, Lecture Notes in Computer Science 1066 (Springer-Verlag, Berlin, 1996); 208–219.

    Chapter  Google Scholar 

  14. L. van den Dries, Tame Topology and O-minimal Structures, London Mathematical Society Lecture Notes Series 248 (Cambridge University Press, 1998).

    Google Scholar 

  15. E. A. Emerson, “Modal Checking and the Mu-calculus”, in N. Immerman and P. G. Kolaitis (eds.), Descriptive Complexity and Finite Models, DIMACS Series in Discrete Mathematics and Theoretical Computer Science 31 (American Mathematical Society, Providence, 1997); 185–208.

    Google Scholar 

  16. R. Fagin, J. Y. Halpern, Y. Moses and M. Y. Vardi, Reasoning About Knowledge (MIT Press, Cambridge MA, 1995).

    MATH  Google Scholar 

  17. V. Gupta, T. A. Henzinger and R. Jagadeesan, “Robust Timed Automata”, in O. Maler (ed.), Hybrid and Real-Time Systems: International Workshop HART’97, March 1997, Lecture Notes in Computer Science 1201 (Springer-Verlag, Berlin, 1997); 331–345.

    Chapter  Google Scholar 

  18. L. Henkin, “Completeness in the Theory of Types“, Journal of Symbolic Logic15 (1950) 81–91.

    Article  MathSciNet  Google Scholar 

  19. T. A. Henzinger, “The Theory of Hybrid Automata”, Proceedings of the 11 thAnnual IEEE Symposium on Logic in Computer Science (LICS’ 96) (IEEE Computer Society Press, 1996); 278–292.

    Google Scholar 

  20. T. A. Henzinger, O. Kupferman, and S. Qadeer, “From Pre-historic to Post-modern Symbolic Model Checking”, Proceedings of the Tenth International Conference on Computer-aided Verification (CAV 1998), Lecture Notes in Computer Science (Springer-Verlag, Berlin, 1998).

    Google Scholar 

  21. T. A. Henzinger, Z. Manna and A. Pnueli, “Towards Refining Temporal Specifications into Hybrid Systems”, in R. Grossman et al. (eds.), Hybrid Systems, Lecture Notes in Computer Science 736 (Springer-Verlag, Berlin,1993), 60–76.

    Chapter  Google Scholar 

  22. M. J. Hollenberg, Logic and Bisimulation, PhD dissertation, Department of Philosophy, Utrecht University, March 1998.

    Google Scholar 

  23. D. Kozen, “Results on the Propositional µ-Calculus”, Theoretical Computer Science27 (1983) 333–354.

    Article  MathSciNet  Google Scholar 

  24. K. Kuratowski, Topology, Volume 1, revised edition (Academic Press, New York, 1966). Translated by J. Jaworowski from the French 1958 edition of Topologie, Volume 1, Polska Akademia Nauk Monogra_e Matematyczne, Tom 21 (Panstwowe Wydawnictwo Naukowe, Warsaw, 1958).

    Google Scholar 

  25. D. Janin and I. Walukiewicz, “On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic”, Proceedings of the Seventh International Conference on Concurrency Theory (CONCUR’96), Lecture Notes in Computer Science 1119 (Springer-Verlag, Berlin, 1996), 263–277.

    Google Scholar 

  26. B. Jonsson and A. Tarski, “Boolean Algebras with Operators, Part I”, American Journal of Mathematics 73 (1951) 891–939.

    Article  MathSciNet  Google Scholar 

  27. G. Laerriere, G. J. Pappas and S. Sastry, “O-Minimal Hybrid Systems”, Technical report UCB/ERL M98/29, Department of Electrical Engineering and Computer Science, University of California at Berkeley, May 1998.

    Google Scholar 

  28. G. Laerriere, G. J. Pappas and S. Yovine, “Decidable Hybrid Systems”, Technical report UCB/ERL M98/39, Department of Electrical Engineering and Computer Science, University of California at Berkeley, June 1998.

    Google Scholar 

  29. Z. Manna and A. Pnueli, “Verifying Hybrid Systems”, in R. Grossman et al. (eds.) Hybrid Systems, Lecture Notes in Computer Science 736 (Springer-Verlag, Berlin,1993), 4–35.

    Chapter  Google Scholar 

  30. Z. Manna and H. B. Simpa, “Deductive Verification of Hybrid Systems Using STeP”, in T. A. Henzinger and S. Sastry (eds), Hybrid Systems-Computation and Control: Proceedings of the First International Workshop (HSCC’ 98), Lecture Notes in Computer Science 1386, (Springer-Verlag, Berlin, 1998).

    Google Scholar 

  31. J. C.C. McKinsey, “A Solution of the Decision Problem for the Lewis Systems S2 and S4, with an Application to Topology”, Journal of Symbolic Logic6 (1941) 117–134.

    Article  MathSciNet  Google Scholar 

  32. J. C.C. McKinsey and A. Tarski, “The Algebra of Topology”, Annals of Mathematics45 (1944) 141–191.

    Article  MathSciNet  Google Scholar 

  33. J. R. Munkres, Topology: A First Course (Prentice Hall, Englewood Cliffs, 1975).

    MATH  Google Scholar 

  34. A. Nerode and W. Kohn, “Models for Hybrid Systems: Automata, Topologies, Controllability, Observability”, in R. Grossman et al. (eds.), Hybrid Systems, Lecture Notes in Computer Science 736 (Springer-Verlag, Berlin,1993), 297–316.

    Chapter  Google Scholar 

  35. A. Nerode and R. Shore, Logic for Applications (2nd ed.), Graduate Texts in Computer Science (Springer-Verlag, Berlin, 1997).

    Google Scholar 

  36. H. Rasiowa and R. Sikorski, The Mathematics of Metamathematics, Polska Akademia Nauk Monogra_e Matematyczne, Tom 41 (Panstwowe Wydawnictwo Naukowe, Warsaw, 1963).

    Google Scholar 

  37. M. B. Smyth, “Semi-metrics, closure spaces and digital topology”, Theoretical Computer Science151 (1995) 257–276.

    Article  MathSciNet  Google Scholar 

  38. C. Stirling, “Modal and Temporal Logics”, in S. Abramsky, D. M. Gabbay and T. Maibaum (eds.), Handbook of Logic in Computer Science, Vol. 2:Computational Structures (Oxford University Press,_ Clarendon Press, Oxford, 1992), 477–563

    Google Scholar 

  39. I. Walukiewicz, “On Completeness of the µ-calculus”, Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (LICS’ 93) (IEEE Computer Society Press, 1993); 136–146.

    Google Scholar 

  40. I. Walukiewicz, “A Note on the Completeness of Kozen’s Axiomatization of the Propositonal µ-calculus”, Bulletin of Symbolic Logic2 (1996) 349–366.

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Center for Foundations of Intelligent Systems, Cornell University, 626 Rhodes Hall, Ithaca, NY, 14853, USA

    J. M. Davoren

Authors
  1. J. M. Davoren
    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

Davoren, J.M. (1999). On Hybrid Systems and the Modal µ-calculus. 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_3

Download citation

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

  • 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