Algorithmic analysis of polygonal hybrid systems. I: Reachability. (English) Zbl 1121.68071

Asarin, Eugene; Schneider, Gerardo; Yovine, Sergio

Theor. Comput. Sci. 379, No. 1-2, 231-265 (2007).

Summary: We are concerned with the formal verification of two-dimensional non-deterministic hybrid systems, namely polygonal differential inclusion systems (SPDIs). SPDIs are a class of non-deterministic systems that correspond to piecewise constant differential inclusions on the plane, for which we study the reachability problem.
Our contribution is the development of an algorithm for solving exactly the reachability problem of SPDIs. We extend the geometric approach due to Maler and Pnueli [O. Maler and A. Pnueli, “Reachability analysis of planar multi-linear systems”, Lect. Notes Comput. Sci. 697, 194–209 (1993; Zbl 0825.00130)] to non-deterministic systems, based on the combination of three techniques: the representation of the two-dimensional continuous-time dynamics as a one-dimensional discrete-time system (using Poincaré maps), the characterization of the set of qualitative behaviors of the latter as a finite set of types of signatures, and acceleration used to explore reachability according to each of these types.

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
34A60	Ordinary differential inclusions
93B03	Attainable sets, reachability
93C30	Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)

Keywords:

hybrid systems; differential inclusions; verification; decision algorithm; reachability analysis

Citations:

Zbl 0825.00130

Software:

HyTech; SPeeDI; Charon

References:

[1]	Abdulla, P.; Annichini, A.; Bouajjani, A., Symbolic verification of lossy channel systems: application to the bounded retransmission protocol, (), 208-222
[2]	E. Asarin, O. Bournez, T. Dang, O. Maler, Approximate reachability analysis of piecewise-linear dynamical systems, in: Lynch and Krogh [39], pp. 20-31 · Zbl 0938.93502
[3]	Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T.A.; Ho, P.-H.; Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The algorithmic analysis of hybrid systems, Theoretical computer science, 138, 3-34, (1995) · Zbl 0874.68206
[4]	Alur, R.; Dill, D.L., A theory of timed automata, Theoretical computer science, 126, 183-235, (1994) · Zbl 0803.68071
[5]	R. Alur, R. Grosu, Y. Hur, V. Kumar, I. Lee, Modular specification of hybrid systems in {\sccharon}, in: Lynch and Krogh [39], pp. 6-19 · Zbl 0992.93040
[6]	(), Rutgers University in New Brunswick, NJ, USA
[7]	()
[8]	()
[9]	()
[10]	Asarin, E.; Maler, O., On some relations between dynamical systems and transition systems, (), 59-72 · Zbl 1418.68088
[11]	Asarin, E.; Maler, O.; Pnueli, A., Reachability analysis of dynamical systems having piecewise-constant derivatives, Theoretical computer science, 138, 35-65, (1995) · Zbl 0884.68050
[12]	Asarin, E.; Pace, G.; Schneider, G.; Yovine, S., Speedi: A verification tool for polygonal hybrid systems, (), 354-358 · Zbl 1010.68791
[13]	Asarin, E.; Schneider, G., Widening the boundary between decidable and undecidable hybrid systems, (), 193-208 · Zbl 1012.68141
[14]	E. Asarin, G. Schneider, S. Yovine, On the decidability of the reachability problem for planar differential inclusions, in: di Benedetto and Sangiovanni-Vincentelli [26], pp. 89-104 · Zbl 0991.93009
[15]	E. Asarin, G. Schneider, S. Yovine, Towards computing phase portraits of polygonal differential inclusions, in: Tomlin and Greenstreet [50], pp. 49-61 · Zbl 1054.93030
[16]	A. Balluchi, L. Benvenuti, G.M. Miconi, U. Pozzi, T. Villa, M.D. Di Benedetto, H. Wong-Toi, A.L. Sangiovanni-Vincentelli, Maximal safe set computation for idle speed control of an automotive engine, in: Lynch and Krogh [39], pp. 32-44 · Zbl 0962.93070
[17]	Boigelot, B.; Godefroid, P.; Willems, B.; Wolper, P., The power of qdds, (), 172-186
[18]	Bouajjani, A.; Habermehl, P., Symbolic reachability analysis of FIFO channel systems with nonregular sets of configurations (extended abstract), (), 560-570 · Zbl 1401.68186
[19]	Boigelot, B.; Herbreteau, F.; Jodogne, S., Hybrid acceleration using real vector automata, (), 193-205 · Zbl 1278.68156
[20]	Bauer, N.; Kowalewski, S.; Sand, G., A case study: multi product batch plant for the demonstration of control and scheduling problems, (), 969-974
[21]	M. Broucke, A geometric approach to bisimulation and verification of hybrid systems, in: Vaandrager and van Schuppen [53], pp. 61-75 · Zbl 0928.93024
[22]	O. Botchkarev, S. Tripakis, Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations, in: Lynch and Krogh [39], pp. 73-88 · Zbl 1037.93510
[23]	Boigelot, B.; Wolper, P., Symbolic verification with periodic sets, (), 55-67
[24]	A. Chutinan, B.H. Krogh, Computing polyhedral approximations to dynamic flow pipes, in: Proc. of the 37th Annual International Conference on Decision and Control, CDC’98. IEEE, 1998
[25]	T. Dang, d/dt manual, Technical report, Verimag, Grenoble, 2000
[26]	()
[27]	Dang, T.; Maler, O., Reachability analysis via face lifting, (), 96-109
[28]	J. Della Dora, S. Yovine, Looking for a methodology for analyzing hybrid systems, in: European Control Conference, Porto, Portugal, September 2001
[29]	J.J.H. Fey, J.H. van Schuppen, VHS case study 4—modeling and control of a juice processing plant.http://www-verimag.imag.fr/VHS/CS4/dcs42.ps.gz, 1999
[30]	J. Guckenheimer, S. Johnson, Planar hybrid systems, in: Hybrid Systems and Autonomous Control Workshop, pp. 202-225, 1994
[31]	M. R. Greenstreet, I. Mitchell, Reachability analysis using polygonal projections, in: Vaandrager and van Schuppen [53], pp. 103-116 · Zbl 1038.93509
[32]	()
[33]	Henzinger, T.A.; Kopke, P.W.; Puri, A.; Varaiya, P., What’s decidable about hybrid automata?, (), 373-382 · Zbl 0978.68534
[34]	Henzinger, T.A.; Ho, P.-H.; Wong-toi, H., Hytech: A model checker for hybrid systems, Software tools for technology transfer, 1, 1, 110-122, (1997) · Zbl 1060.68603
[35]	Hirsch, M.W.; Smale, S., Differential equations, dynamical systems and linear algebra, (1974), Academic Press · Zbl 0309.34001
[36]	P. Koiran, My favourite problems. http://www.ens-lyon.fr/ koiran/problems.html
[37]	A.B. Kurzhanski, P. Varaiya, Ellipsoidal techniques for reachability analysis, in: Lynch and Krogh [39], pp. 202-214 · Zbl 0962.93009
[38]	Lay, S.R., Convex sets and their applications, (1982), John Wiley and Sons New York · Zbl 0492.52001
[39]	()
[40]	Lafferriere, G.; Pappas, G.; Yovine, S., Symbolic reachability computation of families of linear vector fields, Journal of symbolic computation, 32, 3, 231-253, (2001) · Zbl 0983.93004
[41]	Maler, O.; Pnueli, A., Reachability analysis of planar multi-linear systems, (), 194-209
[42]	Mysore, V.; Pnueli, A., Refining the undecidability frontier of hybrid automata, (), 261-272 · Zbl 1172.68521
[43]	Nemytskii, V.V.; Stepanov, V.V., Qualitative theory of differential equations, (1960), Princeton University Press · Zbl 0089.29502
[44]	PATH Project. http://paleale.eecs.berkeley.edu/
[45]	Pace, G.; Schneider, G., Model checking polygonal differential inclusions using invariance kernels, (), 110-121 · Zbl 1202.68254
[46]	Pace, G.; Schneider, G., A compositional algorithm for parallel model checking of polygonal hybrid systems, (), 168-182 · Zbl 1168.68426
[47]	Pace, G.; Schneider, G., Static analysis for state-space reduction of polygonal hybrid systems, (), 306-321 · Zbl 1141.68438
[48]	A. Puri, P. Varaiya, V. Borkar, Epsilon approximations of differential inclusions, in: Alur et al. [6], pp. 362-376
[49]	Schneider, G., Computing invariance kernels of polygonal hybrid systems, Nordic journal of computing, 11, 2, 194-210, (2004) · Zbl 1088.68092
[50]	()
[51]	Tomlin, C.; Lygeros, J.; Sastry, S., Conflict resolution for air traffic management: A study in multi-agent hybrid systems, IEEE transactions on automatic control, 43, 4, 509-521, (1998)
[52]	K. C˘erāns, J. Vīksna, Deciding reachability for planar multi-polynomial systems, in: Alur et al. [6], pp. 389-400
[53]	()