Informace o publikaci

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

Autoři

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

Druh Článek ve sborníku
Konference Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://dl.acm.org/citation.cfm?id=3311793
Doi http://dx.doi.org/10.1145/3302504.3311793
Klíčová slova SMT solver; discrete abstraction; dynamical systems; hybrid systems
Popis 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.
Související projekty: