Abstract
One of the most important analysis problems of hybrid systems is the reachability problem. State of the art computational tools perform reachability computation for timed automata, multirate automata, and rectangular automata. In this paper, we extend the decidability frontier for classes of linear hybrid systems, which are introduced as hybrid systems with linear vector fields in each discrete location. This result is achieved by showing that any such hybrid system admits a finite bisimulation, and by providing an algorithm that computes it using decision methods from mathematical logic.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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:3–34, 1995.
R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
D.S. Arnon, G.E. Collins, and S. McCallum. Cylindrical algebraic decomposition I: The basic algorithm. SIAM Journal on Computing, 13(4):865–877, November 1984.
A. Dolzman and T. Sturm. REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin, 31(2): 2–9, June 1997.
T.A. Henzinger. Hybrid automata with finite bisimulations. In Z. Fülöp and F. Gécseg, editors, ICALP 95: Automata, Languages, and Programming, pages 324–335. Springer-Verlag, 1995.
T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? In Proceedings of the 27th Annual Symposium on Theory of Computing, pages 373–382. ACM Press, 1995.
G. Lafferriere, G.J. Pappas, and S. Sastry. O-minimal hybrid systems. Technical Report UCB/ERL M98/29, University of California at Berkeley, Berkeley, CA, April 1998.
G. Lafferriere, G.J. Pappas, and S. Yovine. Reachability computation of linear hybrid systems. In Proc. of 14th IFAC World Congress. Elsevier Science Ltd., 1999. To appear.
A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular differential inclusions. In Computer Aided Verification, pages 95–104, 1994.
A. Tarski. A decision method for elementary algebra and geometry. University of California Press, second edition, 1951.
C. Tomlin, G.J. Pappas, and S. Sastry. Conflict resolution for air traffic management: A study in multi-agent hybrid systems. IEEE Transactions on Automatic Control, 43(4):509–521, April 1998.
L. van den Dries. Tame Topology and o-minimal structures. Cambridge University Press, 1998.
L. van den Dries and C. Miller. On the real exponential field with restricted analytic functions. Israel Journal of Mathematics, 85:19–56, 1994.
P. Varaiya. Reach set computation using optimal control. 1997. preprint.
V. Weispfenning. A new approach to quantifier elimination for real algebra. Technical Report MIP-9305, Universität Passau, Germany, July 1993.
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(4):1051–1094, Oct 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lafferriere, G., Pappas, G.J., Yovine, S. (1999). A New Class of Decidable Hybrid Systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds) Hybrid Systems: Computation and Control. HSCC 1999. Lecture Notes in Computer Science, vol 1569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48983-5_15
Download citation
DOI: https://doi.org/10.1007/3-540-48983-5_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65734-7
Online ISBN: 978-3-540-48983-2
eBook Packages: Springer Book Archive