Using symmetry transformations in equivariant dynamical systems for their safety verification. (English) Zbl 1447.93021

Chen, Yu-Fang (ed.) et al., Automated technology for verification and analysis. 17th international symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11781, 98-114 (2019).
Summary: In this paper, we investigate how symmetry transformations of equivariant dynamical systems can reduce the computation effort for safety verification. Symmetry transformations of equivariant systems map solutions to other solutions. We build upon this result, producing reachsets from other previously computed reachsets. We augment the standard simulation-based verification algorithm with a new procedure that attempts to verify the safety of the system starting from a new initial set of states by transforming previously computed reachsets. This new algorithm required the creation of a new cache-tree data structure for multi-resolution reachtubes. Our implementation has been tested on several benchmarks and has achieved significant improvements in verification time.
For the entire collection see [Zbl 1428.68012].


93B03 Attainable sets, reachability
93B17 Transformations
93C83 Control/observation systems involving computers (process control, etc.)
93B70 Networked control


HARE; DryVR; S-TaLiRo; Breach
Full Text: DOI


[1] Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254-257. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_21 · Zbl 1316.68069
[2] Antuña, L., Araiza-Illan, D., Campos, S., Eder, K.: Symmetry reduction enables model checking of more complex emergent behaviours of swarm navigation algorithms. In: Dixon, C., Tuyls, K. (eds.) TAROS 2015. LNCS (LNAI), vol. 9287, pp. 26-37. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22416-9_4
[3] Clarke, E.M., Jha, S.: Symmetry and induction in model checking. In: Computer Science Today: Recent Trends and Developments, pp. 455-470 (1995)
[4] Coddington, E.A., Levinson, N.: Theory of Ordinary Differential Equations. McGraw-Hill, New York (1955) · Zbl 0064.33002
[5] Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167-170. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_17
[6] Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: EMSOFT (2013)
[7] Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Computer Aided Verification, 5th International Conference, CAV 1993, Elounda, Greece, Proceedings, 28 June-1 July 1993, pp. 463-478 (1993)
[8] Fan, C., Mitra, S.: Bounded verification with on-the-fly discrepancy computation. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 446-463. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24953-7_32 · Zbl 1471.68140
[9] Fan, C., Qi, B., Mitra, S.: Data-driven formal reasoning and their applications in safety analysis of vehicle autonomy features. IEEE Design Test 35(3), 31-38 (2018)
[10] Fan, C., Qi, B., Mitra, S., Viswanathan, M.: DryVR: data-driven verification and compositional reasoning for automotive systems. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 441-461. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_22
[11] Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 531-538. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_29
[12] Freund, P.G.O.: Introduction to Supersymmetry. Cambridge Monographs on Mathematical Physics. Cambridge University Press, Cambridge (1986)
[13] Gérard, L., Slotine, J.J.: Neuronal networks and controlled symmetries, a generic framework. arXiv preprint q-bio/0612049 (2006)
[14] Golubitsky, M., Stewart, I.: The Symmetry Perspective: From Equilibrium to Chaos in Phase Space and Physical Space. Progress in Mathematics, Birkhäuser Basel (2012) · Zbl 1031.37001
[15] Golubitsky, M., Stewart, I., Török, A.: Patterns of synchrony in coupled cell networks with multiple arrows. SIAM J. Appl. Dyn. Syst. 4(1), 78-100 (2005) · Zbl 1090.34030
[16] Huang, Z., Fan, C., Mereacre, A., Mitra, S., Kwiatkowska, M.: Invariant verification of nonlinear hybrid automata networks of cardiac cells. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 373-390. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_25
[17] Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Proceedings of the 11th IFIP WG10.2 International Conference Sponsored by IFIP WG10.2 and in Cooperation with IEEE COMPSOC on Computer Hardware Description Languages and Their Applications, CHDL 1993, pp. 97-111. North-Holland Publishing Co., Amsterdam, The Netherlands (1993)
[18] Koopman, P., Wagner, M.: Challenges in autonomous vehicle testing and validation. SAE Int. J. Transp. Saf. 4(2016-01-0128), 15-24 (2016)
[19] Kwiatkowska, M.Z., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: 18th International Conference on Computer Aided Verification, CAV 2006, Seattle, WA, USA, 17-20 August 2006, Proceedings, pp. 234-248 (2006) · Zbl 1188.68194
[20] Marsden, J.E., Ratiu, T.S.: Introduction to Mechanics and Symmetry: A Basic Exposition of Classical Mechanical Systems. Springer, New York (2010). https://doi.org/10.1007/978-0-387-21792-5 · Zbl 0933.70003
[21] Mehta, P.G., Hagen, G., Banaszuk, A.: Symmetry and symmetry-breaking for a wave equation with feedback. SIAM J. Appl. Dyn. Syst. 6(3), 549-575 (2007) · Zbl 1210.74091
[22] Olver, P.J.: Applications of Lie Groups to Differential Equations. Springer, New York (1986). https://doi.org/10.1007/978-1-4684-0274-2 · Zbl 0588.22001
[23] Pham, Q.C., Slotine, J.J.: Stable concurrent synchronization in dynamic system networks. Neural Netw. 20(1), 62-77 (2007) · Zbl 1158.68449
[24] Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automata-based cegar for rectangular hybrid systems. Form. Methods Syst. Des. 46(2), 105-134 (2015) · Zbl 1341.68109
[25] Russo, G., Slotine, J.J.E.: Symmetries, stability, and control in nonlinear systems and networks. Phys. Rev. E 84(4), 041929 (2011)
[26] Spong, M. · Zbl 1365.93329
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.