Computation and Visualisation of Phase Portraits for Model Checking SPDIs

  • Gordon Pace
  • Gerardo Schneider
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


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 [1]. Nonetheless, various decidable subclasses have been identified, including polygonal hybrid systems (SPDIs) [2]. SPDIs can be used, for instance, in the analysis of approximations of non-linear differential equations in two-dimensions.


Model Check Hybrid System Phase Portrait Hybrid Automaton Reachability Analysis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: STOC 1995, pp. 373–382. ACM Press, New York (1995)CrossRefGoogle Scholar
  2. 2.
    Asarin, E., Schneider, G., Yovine, S.: On the decidability of the reachability problem for planar differential inclusions. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 89–104. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. 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
  4. 4.
    Aubin, J.P.: The substratum of impulse and hybrid control systems. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 105–118. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 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
  6. 6.
    Kourjanski, M., Varaiya, P.: Stability of hybrid systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 413–423. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  7. 7.
    Asarin, E., Schneider, G., Yovine, S.: Towards computing phase portraits of polygonal differential inclusions. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 49–61. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Schneider, G.: Computing invariance kernels of polygonal hybrid systems. Nordic Journal of Computing 11, 194–210 (2004)zbMATHMathSciNetGoogle Scholar
  9. 9.
    Pace, G., Schneider, G.: Static analysis for state-space reduction of polygonal hybrid systems. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 306–321. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 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
  11. 11.
    Asarin, E., Pace, G., Schneider, G., Yovine, S.: SPeeDI: a verification tool for polygonal hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 354–358. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Pace, G., Schneider, G.: A compositional algorithm for parallel model checking of polygonal hybrid systems. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 168–182. Springer, Heidelberg (2006)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Gordon Pace
    • 1
  • Gerardo Schneider
    • 2
  1. 1.Dept. of Computer ScienceUniversity of MaltaMsida, Malta 
  2. 2.Dept. of InformaticsUniversity of OsloOsloNorway

Personalised recommendations