Computation and Visualisation of Phase Portraits for Model Checking SPDIs
Hybrid systems combining discrete and continuous dynamics arise as mathematical models of various artificial and natural systems, and as an approximation to complex continuous systems. Reachability analysis has been the principal research question in the verification of hybrid systems, even though it is a wellknown result that most non-trivial subclasses of hybrid systems reachability and most verification problems are undecidable . Nonetheless, various decidable subclasses have been identified, including polygonal hybrid systems (SPDIs) . SPDIs can be used, for instance, in the analysis of approximations of non-linear differential equations in two-dimensions.
KeywordsModel Check Hybrid System Phase Portrait Hybrid Automaton Reachability Analysis
- 3.Aubin, J.P., Lygeros, J., Quincampoix, M., Sastry, S., Seube, N.: Viability and invariance kernels of impulse differential inclusions. In: Conference on Decision and Control. IEEE, vol. 40, pp. 340–345 (2001)Google Scholar
- 5.Deshpande, A., Varaiya, P.: Viable control of hybrid systems. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 128–147. Springer, Heidelberg (1995)Google Scholar
- 10.Pace, G., Schneider, G.: Model checking polygonal differential inclusions using invariance kernels. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 110–121. Springer, Heidelberg (2004)Google Scholar