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.

Basic information

Original name

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

Authors

BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Jana DRAŽANOVÁ (203 Czech Republic, belonging to the institution), Samuel PASTVA (703 Slovakia, guarantor, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, belonging to the institution)

Edition

New York, NY, USA, Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control, p. 99-108, 10 pp. 2019

Publisher

ACM

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

URL

RIV identification code

RIV/00216224:14330/19:00107360

Organization unit

Faculty of Informatics

ISBN

978-1-4503-6282-5

DOI

http://dx.doi.org/10.1145/3302504.3311793

UT WoS

000516713900011

Keywords in English

SMT solver; discrete abstraction; dynamical systems; hybrid systems

Abstract

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.

Links

GA18-00178S, research and development project

Name: Diskrétní bifurkační analýza reaktivních systémů

Investor: Czech Science Foundation

MUNI/A/1018/2018, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.

Investor: Masaryk University, Category A

Citovat

BENEŠ, Nikola, Luboš BRIM, Jana DRAŽANOVÁ, Samuel PASTVA and 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, p. 99-108. ISBN 978-1-4503-6282-5. Available from: 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 and 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, p.~99-108. ISBN~978-1-4503-6282-5. Available from: https://dx.doi.org/10.1145/3302504.3311793.

Detailed Information on Publication Record