×
Asarin, Eugene; Pace, Gordon; Schneider, Gerardo; Yovine, Sergio

Algorithmic analysis of polygonal hybrid systems. II: Phase portrait and tools. (English) Zbl 1134.68026

Theor. Comput. Sci. 390, No. 1, 1-26 (2008).
Summary: Polygonal differential inclusion systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. The reachability problem as well as the computation of certain objects of the phase portrait is decidable. In this paper we show how to compute the viability, controllability and invariance kernels, as well as semi-separatrix curves for SPDIs. We also present the tool SPeeDI\(^{+}\), which implements a reachability algorithm and computes phase portraits of SPDIs.
[For Part I see Theor. Comput. Sci. 379, No. 1–2, 231–265 (2007; Zbl 1121.68071).]

Cited in 1 Document

MSC:

68Q45 Formal languages and automata
34A60 Ordinary differential inclusions
68Q60 Specification and verification (program logics, model checking, etc.)
93B05 Controllability
93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)

Keywords:

hybrid systems; differential inclusions; verification; phase portrait

Citations:

Zbl 1121.68071

Software:

HyTech; SPeeDI; Haskell
PDF BibTeX XML Cite
\textit{E. Asarin} et al., Theor. Comput. Sci. 390, No. 1, 1--26 (2008; Zbl 1134.68026)
Full Text: DOI
  • logo of hbz
  • logo of WorldCat

References:

[1] Aubin, J.-P.; Cellina, Arrigo, ()
[2] Alur, R.; Dill, D.L., A theory of timed automata, Theoretical computer science, 126, 183-235, (1994) · Zbl 0803.68071
[3] J.-P. Aubin, J. Lygeros, M. Quincampoix, S. Sastry, N. Seube, Towards a viability theory for hybrid systems, in: European Control Conference, 2001
[4] Aubin, J.-P.; Lygeros, J.; Quincampoix, M.; Sastry, S.; Seube, N., Viability and invariance kernels of impulse differential inclusions, (), 340-345
[5] Asarin, E.; Pace, G.; Schneider, G.; Yovine, S., Speedi: A verification tool for polygonal hybrid systems, (), 354-358 · Zbl 1010.68791
[6] Asarin, E.; Schneider, G.; Yovine, S., On the decidability of the reachability problem for planar differential inclusions, (), 89-104 · Zbl 0991.93009
[7] Asarin, E.; Schneider, G.; Yovine, S., Towards computing phase portraits of polygonal differential inclusions, (), 49-61 · Zbl 1054.93030
[8] Asarin, E.; Schneider, G.; Yovine, S., Algorithmic analysis of polygonal hybrid systems. part I: reachability, Theoretical computer science, 379, 1-2, 231-265, (2007) · Zbl 1121.68071
[9] Aubin, J.-P., A survey on viability theory, SIAM journal on control and optimization, 28, 4, 749-789, (1990)
[10] Bird, R.; Wadler, P., Introduction to functional programming, (1988), Prentice Hall International New York
[11] Deshpande, A.; Varaiya, P., Viable control of hybrid systems, (), 128-147
[12] Field, A.J.; Harrison, P.G., Functional programming, (1988), Addison Wesley Reading, MA · Zbl 0828.68033
[13] T.A. Henzinger, P.-H. Ho, H. Wong-Toi, Hytech: The next generation, in: Proc. IEEE Real-Time Systems Symposium RTSS’95, Pisa, Italy, December 1995
[14] Henzinger, T.A.; Kopke, P.W.; Puri, A.; Varaiya, P., What’s decidable about hybrid automata?, (), 373-382 · Zbl 0978.68534
[15] Henzinger, T.A.; Ho, P.-H.; Wong-toi, H., Hytech: A model checker for hybrid systems, Software tools for technology transfer, 1, 1, (1997) · Zbl 1060.68603
[16] Hirsch, M.W.; Smale, S., Differential equations, dynamical systems and linear algebra, (1974), Academic Press Inc. · Zbl 0309.34001
[17] Peyton Jones, S., Haskell 98 language and libraries: the revised report, (2003), Cambridge University Press · Zbl 1067.68041
[18] Kowalczyk, P.; di Bernardo, M., On a novel class of bifurcations in hybrid dynamical systems, (), 361-374 · Zbl 0991.93048
[19] Kourjanski, M.; Varaiya, P., Stability of hybrid systems, (), 413-423
[20] M. Leucker, T. Noll, P. Stevens, M. Weber, Functional programming languages for verification tools: Experiences with ML and Haskell, in: Proceedings of the Scottish Functional Programming Workshop, SFPW’01, 2001
[21] 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
[22] Maler, O.; Pnueli, A., Reachability analysis of planar multi-linear systems, (), 194-209
[23] Matveev, A.; Savkin, A., Qualitative theory of hybrid dynamical systems, (2000), Birkhäuser Boston · Zbl 1052.93004
[24] Pace, G.; Schneider, G., A compositional algorithm for parallel model checking of polygonal hybrid systems, (), 168-182 · Zbl 1168.68426
[25] G. Pace, G. Schneider, SPeeDI^{+}, http://www.cs.um.edu.mt/speedi/
[26] Pace, G.; Schneider, G., Static analysis for state-space reduction of polygonal hybrid systems, (), 306-321 · Zbl 1141.68438
[27] G. Schneider, Algorithmic Analysis of Polygonal Hybrid Systems, Ph.D. Thesis, VERIMAG-UJF, Grenoble, France, July 2002
[28] Schneider, G., Computing invariance kernels of polygonal hybrid systems, Nordic journal of computing, 11, 2, 194-210, (2004) · Zbl 1088.68092
[29] Simić, S.; Johansson, K.; Sastry, S.; Lygeros, J., Towards a geometric theory of hybrid systems, (), 421-436 · Zbl 0963.93044
[30] Saint-Pierre, P., Hybrid kernels and capture basins for impulse constrained systems, () · Zbl 1050.93041
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.