Facetal abstraction for non-linear dynamical systems based on δ-decidable SMT

N. Beneš, L. Brim, J. Dražanová, S. Pastva, D. Šafránek

International Conference on Hybrid Systems: Computation and Control (HSCC) 2019

Formal analysis of non-linear continuous and hybrid systems is a hot topic. A common approach builds on computing a suitable finite discrete abstraction of the continuous system. In this paper, we propose a facetal abstraction which eliminates certain drawbacks of existing abstractions. The states of our abstraction are built primarily from facets of a polytopal partitioning of the system's state space taking thus into account the flow of the continuous dynamics and leading to global over-approximation. The transition system construction is based on queries solved by a δ-decision SMT-solver. The method is evaluated on several case studies.

Cite this paper as: Beneš N., Brim L., Drazanova J., Pastva S., Šafránek D. (2019) Facetal abstraction for non-linear dynamical systems based on δ-decidable SMT. In: Vojnar T., Zhang L. (eds) Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control. HSCC 2019. ACM