Advertisement

What Will Be Eventually True of Polynomial Hybrid Automata?

  • Martin Fränzle
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)

Abstract

Hybrid automata have been introduced in both control engineering and computer science as a formal model for the dynamics of hybrid discrete-continuous systems. While computability issues concerning safety properties have been extensively studied, liveness properties have remained largely uninvestigated. In this article, we investigate decidability of state recurrence and of progress properties.

First, we show that state recurrence and progress are in general undecidable for polynomial hybrid automata. Then, we demonstrate that they are closely related for hybrid automata subject to a simple model of noise, even though these automata are infinite-state systems. Based on this, we augment a semi-decision procedure for recurrence with a semidecision method for length-boundedness of paths in such a way that we obtain an automatic verification method for progress properties of linear and polynomial hybrid automata that may only fail on pathological, practically uninteresting cases. These cases are such that satisfaction of the desired progress property crucially depends on the complete absence of noise, a situation unlikely to occur in real hybrid systems.

Keywords

Hybrid systems State recurrence Progress properties Decidability Verification procedures 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AB01]
    Eugene Asarin and Ahmed Bouajjani. Perturbed turing machines and hybrid systems. In Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001). IEEE, 2001.Google Scholar
  2. [AD94]
    Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  3. [AHS96]
    Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag, editors. Hybrid Systems III-Verification and Control, volume 1066 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Google Scholar
  4. [AHV93]
    Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In Proceedings of the 25th Annual ACM Symposium on Theory of Computing, pages 592–601, 1993.Google Scholar
  5. [AKNS95]
    P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors. Hybrid Systems II, volume 999 of Lecture Notes in Computer Science. Springer-Verlag, 1995.zbMATHGoogle Scholar
  6. [Frä99]
    Martin Fränzle. Analysis of hybrid systems: An ounce of realism can save an infinity of states. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic (CSL’99), volume 1683 of Lecture Notes in Computer Science, pages 126–140. Springer-Verlag, 1999.CrossRefGoogle Scholar
  7. [GHJ97]
    Vineet Gupta, Thomas A. Henzinger, and Radha Jagadeesan. Robust timed automata. In Oded Maler, editor, Proceedings of the First International Workshop on Hybrid and Real-Time Systems (HART 97), volume 1201 of Lecture Notes in Computer Science, pages 331–345. Springer-Verlag, 1997.Google Scholar
  8. [GNRR93]
    Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors. Hybrid Systems, volume 736 of Lecture Notes in Computer Science. Springer-Verlag, 1993.Google Scholar
  9. [HHWT95]
    Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: The next generation. In 16th Annual IEEE Real-time Systems Symposium (RTSS 1995), pages 56–65. IEEE Computer Society Press, 1995.Google Scholar
  10. [HKPV95]
    Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What’s decidable about hybrid automata. In Proceedings of the Twenty-Seventh Annual ACM Symposium on the Theory of Computing, pages 373–382. ACM, 1995.Google Scholar
  11. [Moo98]
    Chris Moore. Finite-dimensional analog computers: Flows, maps, and recurrent neural networks. In C.S. Calude, J. Casti, and M.J. Dinneen, editors, 1st International Conference on Unconventional Models of Computation. Springer-Verlag, 1998.Google Scholar
  12. [MS97]
    Wolfgang Maass and Eduardo D. Sontag. Analog neural nets with Gaussian or other common noise distributions cannot recognize arbitrary regular languages. In Electronic Colloquium on Computational Complexity, technical reports. 1997.Google Scholar
  13. [Pur98]
    Anuj Puri. Dynamical properties of timed automata. In A. P. Ravn and H. Rischel, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’98), volume 1486 of Lecture Notes in Computer Science, pages 210–227. Springer-Verlag, 1998.CrossRefGoogle Scholar
  14. [Tar48]
    Alfred Tarski. A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica, Calif., 1948.zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Martin Fränzle
    • 1
  1. 1.Department of Computer ScienceCarl-von-Ossietzky Universität OldenburgOldenburgGermany

Personalised recommendations