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

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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	https://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:	Diskrétní bifurkační analýza reaktivních systémů Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.