Facetal Abstraction for Non-linear Dynamical Systems Based on delta-decidable SMT

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BENEŠ Nikola BRIM Luboš DRAŽANOVÁ Jana PASTVA Samuel ŠAFRÁNEK David

Year of publication 2019
Type Article in Proceedings
Conference Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1145/3302504.3311793
Doi http://dx.doi.org/10.1145/3302504.3311793
Keywords SMT solver; discrete abstraction; dynamical systems; hybrid systems
Description 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 delta-decision SMT-solver. The method is evaluated on several case studies.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.