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

D 2019

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

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

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

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"

Odkazy

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ěněno: 15. 4. 2021 12:17, doc. RNDr. David Šafránek, Ph.D.

Anotace

V originále

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 VaV

Ná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 MU

Ná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

Citovat

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.

@inproceedings{1521178,
   author = {Beneš, Nikola and Brim, Luboš and Dražanová, Jana and Pastva, Samuel and Šafránek, David},
   address = {New York, NY, USA},
   booktitle = {Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control},
   doi = {http://dx.doi.org/10.1145/3302504.3311793},
   keywords = {SMT solver; discrete abstraction; dynamical systems; hybrid systems},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {New York, NY, USA},
   isbn = {978-1-4503-6282-5},
   pages = {99-108},
   publisher = {ACM},
   title = {Facetal Abstraction for Non-linear Dynamical Systems Based on delta-decidable SMT},
   url = {http://dx.doi.org/10.1145/3302504.3311793},
   year = {2019}
}

TY  - JOUR
ID  - 1521178
AU  - Beneš, Nikola - Brim, Luboš - Dražanová, Jana - Pastva, Samuel - Šafránek, David
PY  - 2019
TI  - Facetal Abstraction for Non-linear Dynamical Systems Based on delta-decidable SMT
PB  - ACM
CY  - New York, NY, USA
SN  - 9781450362825
KW  - SMT solver
KW  - discrete abstraction
KW  - dynamical systems
KW  - hybrid systems
UR  - http://dx.doi.org/10.1145/3302504.3311793
N2  - 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.
ER  -

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 \textit{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.

Podrobný výpis o publikaci