Facetal Abstraction for Non-linear Dynamical Systems Based on delta-decidable SMT
| Autoři | |
|---|---|
| Rok publikování | 2019 |
| Druh | Článek ve sborníku |
| Konference | Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control |
| Fakulta / Pracoviště MU | |
| Citace | BENEŠ, Nikola, Luboš BRIM, Jana DRAŽANOVÁ, Samuel PASTVA a David ŠAFRÁNEK. Facetal Abstraction for Non-linear Dynamical Systems Based on delta-decidable SMT. In Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control. New York, NY, USA: ACM, 2019, s. 99-108. ISBN 978-1-4503-6282-5. Dostupné z: https://dx.doi.org/10.1145/3302504.3311793. |
| www | http://dx.doi.org/10.1145/3302504.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: |