ParaPlan: a tool for parallel reachability analysis of planar polygonal differential inclusion systems. (English) Zbl 1483.68205

Bouyer, Patricia (ed.) et al., Proceedings of the eighth international symposium on games, automata, logics and formal verification, GandALF 2017, Roma, Italy, September 20–22, 2017. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 256, 283-296 (2017).
Summary: We present the ParaPlan tool which provides the reachability analysis of planar hybrid systems defined by differential inclusions (SPDI). It uses the parallelized and optimized version of the algorithm underlying the SPeeDI tool [E. Asarin et al., Lect. Notes Comput. Sci. 2404, 354–358 (2002; Zbl 1010.68791)]. The performance comparison demonstrates the speed-up of up to 83 times with respect to the sequential implementation on various benchmarks. Some of the benchmarks we used are randomly generated with the novel approach based on the partitioning of the plane with Voronoi diagrams.
For the entire collection see [Zbl 1436.68017].


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


Zbl 1010.68791
Full Text: arXiv Link


[1] E. Asarin, O. Maler & A. Pnueli (1995): Reachability Analysis of Dynamical Systems Hav-ing Piecewise-Constant Derivatives. Theoretical Comp. Science 138(1), pp. 35-65, doi:10.1016/ 0304-3975(94)00228-B. · Zbl 0884.68050
[2] E. Asarin, G. J. Pace, G. Schneider & S. Yovine (2002): SPeeDI -A Verification Tool for Polygonal Hybrid Systems. In: 14th International Conference on Computer Aided Verification (CAV), pp. 354-358, doi:10. 1007/3-540-45657-0_28. · Zbl 1010.68791
[3] E. Asarin, G. J. Pace, G. Schneider & S. Yovine (2008): Algorithmic analysis of polygonal hybrid systems, Part II: Phase portrait and tools. Theoretical Computer Science 390(1), pp. 1-26, doi:10.1016/j.tcs. 2007.09.025. · Zbl 1134.68026
[4] E. Asarin, G. Schneider & S. Yovine (2001): On the Decidability of the Reachability Problem for Planar Differential Inclusions. In: Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings, pp. 89-104, doi:10.1007/3-540-45351-2_11.
[5] E. Asarin, G. Schneider & S. Yovine (2007): Algorithmic analysis of polygonal hybrid systems, part I: Reachability. Theoretical Computer Science 379(1-2), pp. 231-265, doi:10.1016/j.tcs.2007.03.055. · Zbl 1121.68071
[6] X. Chen, E.Ábrahám & S. Sankaranarayanan (2013): Flow*: An Analyzer for Non-linear Hybrid Systems. In: Computer Aided Verification -25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, pp. 258-263, doi:10.1007/978-3-642-39799-8_18.
[7] X. Chen, S. Schupp, I. B. Makhlouf, E.Ábrahám, G. Frehse & S. Kowalewski (2015): A Benchmark Suite for Hybrid Systems Reachability Analysis. In: NASA Formal Methods -7th International Symposium, Pasadena, CA, USA, April 27-29, 2015, Proceedings, pp. 408-414, doi:10.1007/978-3-319-17524-9_29.
[8] A. Fehnker & F. Ivančić (2004): Benchmarks for hybrid systems verification. In: International Workshop on Hybrid Systems: Computation and Control, Springer, pp. 326-341, doi:10.1007/978-3-540-24743-2_22. · Zbl 1135.93324
[9] A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu & R. Ray (2016): Parallel reachability analysis for hybrid systems. In: 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016, Kanpur, India, November 18-20, 2016, pp. 12-22, doi:10.1109/MEMCOD. 2016.7797741.
[10] H. A. Hansen & G. Schneider (2009): GSPeeDi-a Verification Tool for Generalized Polygonal Hybrid Sys-tems. In: International Colloquium on Theoretical Aspects of Computing, Springer, pp. 343-348, doi:10. 1007/978-3-642-03466-4_23.
[11] T. A. Henzinger, P. W. Kopke, A. Puri & P. Varaiya (1998): What’s Decidable About Hybrid Automata? Journal of Computer and System Sciences 57(1), pp. 94-124, doi:10.1006/jcss.1998.1581. · Zbl 0920.68091
[12] S. Kong, S. Gao, W. Chen & E. M. Clarke (2015): dReach: δ -Reachability Analysis for Hybrid Systems. In: Tools and Algorithms for the Construction and Analysis of Systems -21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, pp. 200-205, doi:10.1007/978-3-662-46681-0_15.
[13] G. Pace & G. Schneider (2006): A compositional algorithm for parallel model checking of polygonal hybrid systems. In: International Colloquium on Theoretical Aspects of Computing, Springer, pp. 168-182, doi:10. 1007/11921240_12. · Zbl 1168.68426
[14] G. J. Pace & G. Schneider (2008): Relaxing Goodness Is Still Good. In: Theoretical Aspects of Computing -ICTAC 2008, 5th International Colloquium, Istanbul, Turkey, September 1-3, 2008. Proceedings, pp. 274-289, doi:10.1007/978-3-540-85762-4_19. · Zbl 1161.93316
[15] A. Platzer & J.-D. Quesel (2008): KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System De-scription). In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, pp. 171-178, doi:10.1007/978-3-540-71070-7_15. · Zbl 1165.68469
[16] S. Ratschan & Z. She (2005): Safety Verification of Hybrid Systems by Constraint Propagation Based Ab-straction Refinement. In: Hybrid Systems: Computation and Control, 8th International Workshop (HSCC), pp. 573-589, doi:10.1007/978-3-540-31954-2_37. · Zbl 1078.93508
[17] A. Sandler & O. Tveretina: ParaPlan Tool. Available at https://github.com/asandler/ParaPlan.
[18] G. Schneider & G. Pace (2006): SPeeDI+: A 2 Dimensional Hybrid System Model Checker. http://www.cs.um.edu.mt/∼svrg/Tools/SPeeDI/index.html. [Online; accessed 27-January-2017].
[19] S. Schupp, E.Ábrahám, X. Chen, I. B. Makhlouf, G. Frehse, S. Sankaranarayanan & S. Kowalewski (2015): Current challenges in the verification of hybrid systems. In: International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, Springer, pp. 8-24, doi:10.1007/978-3-319-25141-7_2.
[20] R. E. Tarjan (1973): Enumeration of the Elementary Circuits of a Directed Graph. SIAM J. Comput. 2(3), pp. 211-216, doi:10.1137/0202017. · Zbl 0274.05106
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.