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

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

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

Fakulta informatiky

Citace
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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.