Abstract
The reachability problem as well as the computation of the phase portrait for the class of planar hybrid systems defined by constant differential inclusions (SPDI), has been shown to be decidable. The existing reachability algorithm is based on the exploitation of topological properties of the plane which are used to accelerate certain kind of cycles. The complexity of the algorithm makes the analysis of large systems generally unfeasible. In this paper we present a compositional parallel algorithm for reachability analysis of SPDIs. The parallelization is based on the qualitative information obtained from the phase portrait of an SPDI, in particular the controllability kernel.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Asarin, E., Pace, G.J., 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)
Asarin, E., Schneider, G.: Widening the boundary between decidable and undecidable hybrid systems. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 193–208. Springer, Heidelberg (2002)
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)
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, p. 49. Springer, Heidelberg (2002)
Foley, J.D., van Dam, A., Feiner, S.K., Hughes, J.F.: Computer graphics (2nd ed. in C): principles and practice. Addison-Wesley Longman Publishing Co., Inc., Boston (1996)
Henle, M.: A combinatorial introduction to topology. Dover publications, Inc., Mineola (1979)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: STOC 1995, pp. 373–382. ACM Press, New York (1995)
Lafferriere, G., Pappas, G., Yovine, S.: Symbolic reachability computation of families of linear vector fields. Journal of Symbolic Computation 32(3), 231–253 (2001)
Maler, O., Pnueli, A.: Reachability analysis of planar multi-linear systems. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 194–209. Springer, Heidelberg (1993)
Pace, G.J., 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)
Pace, G., Schneider, G.: Static analysis of SPDIs for state-space reduction. Technical Report 336, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway (April 2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pace, G., Schneider, G. (2006). A Compositional Algorithm for Parallel Model Checking of Polygonal Hybrid Systems. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds) Theoretical Aspects of Computing - ICTAC 2006. ICTAC 2006. Lecture Notes in Computer Science, vol 4281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11921240_12
Download citation
DOI: https://doi.org/10.1007/11921240_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48815-6
Online ISBN: 978-3-540-48816-3
eBook Packages: Computer ScienceComputer Science (R0)