Abstract
In this paper we develop an algorithm for solving the reachability problem of two-dimensional piece-wise rectangular differential inclusions. Our procedure is not based on the computation of the reach-set but rather on the computation of the limit of individual trajectories. A key idea is the use of one-dimensional affne Poincaré maps for which we can easily compute the fixpoints. As a first step, we show that between any two points linked by an arbitrary trajectory there always exists a trajectory without self-crossings. Thus, solving the reachability problem requires considering only those. We prove that, indeed, there are only finitely many “qualitative types” of those trajectories. The last step consists in giving a decision procedure for each of them. These procedures are essentially based on the analysis of the limits of extreme trajectories. We illustrate our algorithm on a simple model of a swimmer spinning around a whirlpool.
This work was partially supported by Projet IMAG MASH “Modéelisation et Analyse de Systèmes Hybrides’.
Partially supported by the NATO under grant CRG-961115.
Supported by ESPRIT-LTR Project 26270 VHS “Verification of Hybrid Systems”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. TCS 138 (1995) 3–34.
R. Alur and D.L. Dill. A theory of timed automata. TCS 126 (1994) 183–235.
E. Asarin, O. Bournez, T. Dang, and O. Maler. Reachability analysis of piecewise-linear dynamical systems. In HSCC’00, 20–31. LNCS 1790, Springer Verlag, 2000.
E. Asarin, O. Maler, and A. Pnueli. On the analysis of dynamical systems having piecewise-constant derivatives. TCS, 138 (1995) 35–65.
E. Asarin, G. Schneider and S. Yovine. On the Decidability of the Reachability Problem for Planar Differential Inclusions. VERIMAG Technical Report. 2001. http://www-verimag.imag.fr/~gerardo.
O. Botchkarev and S. Tripakis. Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In HSCC’00. LNCS 1790, Springer Verlag, 2000.
M. Broucke. A geometric approach to bisimulation and verification of hybrid systems. In HSCC’99. LNCS 1569, Springer Verlag, 1999.
K. Čerāns and J. Vīksna. Deciding reachability for planar multi-polynomial systems. In Hybrid Systems III. LNCS 1066, Springer Verlag, 1996.
T. Dang and O. Maler. Reachability analysis via face lifting. In HSCC’98, 96–109. LNCS 1386, Springer Verlag, 1998.
J. Della Dora and S. Yovine. Looking for a methodology for analyzing hybrid systems. Submitted to ECC 2001, 2000.
M. R. Greenstreet and I. Mitchell. Reachability analysis using polygonal projections. In HSCC’99. LNCS 1569, 103–116. Springer Verlag, 1999.
T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? In 27th Annual Symposium on Theory of Computing, 373–382. ACM Press, 1995.
P. Koiran. My favourite problems. http://www.ens-lyon.fr/~koiran/problems.html.
A.B. Kurzhanski and P. Varaiya. Ellipsoidal techniques for reachability analysis. In HSCC’00. LNCS 1790, Springer Verlag, 2000.
G. Lafferriere, G. J. Pappas, and S. Yovine. A new class of decidable hybrid systems. In HSCC’99. LNCS 1569, 137–151. Springer Verlag, 1999.
O. Maler and A. Pnueli. Reachability analysis of planar multi-linear systems. In CAV’93. LNCS 697, 194–209. Springer Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asarin, E., Schneider, G., Yovine, S. (2001). On the Decidability of the Reachability Problem for Planar Differential Inclusions. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds) Hybrid Systems: Computation and Control. HSCC 2001. Lecture Notes in Computer Science, vol 2034. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45351-2_11
Download citation
DOI: https://doi.org/10.1007/3-540-45351-2_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41866-5
Online ISBN: 978-3-540-45351-2
eBook Packages: Springer Book Archive