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.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Facetal Abstraction for Non-linear Dynamical Systems Based on delta-decidable SMT
Autoři BENEŠ, Nikola (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Jana DRAŽANOVÁ (203 Česká republika, domácí), Samuel PASTVA (703 Slovensko, garant, domácí) a David ŠAFRÁNEK (203 Česká republika, domácí).
Vydání New York, NY, USA, Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control, od s. 99-108, 10 s. 2019.
Nakladatel ACM
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
WWW URL
Kód RIV RIV/00216224:14330/19:00107360
Organizační jednotka Fakulta informatiky
ISBN 978-1-4503-6282-5
Doi http://dx.doi.org/10.1145/3302504.3311793
UT WoS 000516713900011
Klíčová slova anglicky SMT solver; discrete abstraction; dynamical systems; hybrid systems
Štítky firank_B
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: doc. RNDr. David Šafránek, Ph.D., učo 3159. Změněno: 15. 4. 2021 12:17.
Anotace
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.
Návaznosti
GA18-00178S, projekt VaVNázev: Diskrétní bifurkační analýza reaktivních systémů
Investor: Grantová agentura ČR, Diskrétní bifurkační analýza reaktivních systémů
MUNI/A/1018/2018, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 26. 4. 2024 05:32