Simulation-Based Computation of Robust Invariants of Hybrid Dynamical Systems
Project goals
One of the most important objects used in the field of formal verification are invariants. An invariant is a set of states of a given system such that the system will always stay in this set of states. Recently, there has been a lot of progress on the constraint-based computation of invariants, that reduces invariant computation to a constraint solving problem in a decidable theory. However, this approach cannot be applied in cases where the corresponding logical theory is not decidable, or where the available constraint solvers are not efficient enough to solve problems of interesting size. The proposal concerns computation of invariants of hybrid dynamical systems, that is, dynamical systems that have partially discrete, partially continuous states and behavior. In order to circumvent the mentioned problems of undecidability and efficiency limitations of constraint solvers, we use a radically different approach that exploits robustness and simulations.
Keywords
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 19 (SGA0201500001)
Main participants
Ústav informatiky AV ČR, v. v. i.
Contest type
VS - Public tender
Contract ID
15-14484S
Alternative language
Project name in Czech
Výpočet robustních invariantů hybridních dynamických systémů s využitím simulací
Annotation in Czech
Jedním z nejdůležitějších nástrojů v oblasti formální verifikace jsou invarianty. Invariantem nazýváme množinu stavů daného systému, pro kterou platí, že každý dosažitelný stav systému náleží do této množiny. V poslední době došlo k velkému vývoji metod pro výpočet invariantů založených na dodržení omezujících podmínek, kdy výpočet invariantu je redukován na řešení problému s omezeními v rozhodnutelné teorii. Nicméně, takový postup nelze použít v případech, ve kterých je patřičná teorie nerozhodnutelná a nebo dostupné nástroje nejsou dost efektivní pro v praxi zajímavé úlohy. Tento návrh se zabývá výpočtem invariantů pro hybridní dynamické systémy, což jsou systémy, které mají částečné diskrétní a částečně spojité chování. Proto, abychom se vyhnuli již zmíněným problémům s nerozhodnutelností a nedostatečnou efektivností dostupných nástrojů, zvolíme značně odlišný způsob, který využívá robustnosti a simulací.
Scientific branches
Completed project evaluation
Provider evaluation
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Project results evaluation
The project focused on calculating the invariants of hybrid robustness and simulation. Among other things, the main outcome of the project is the method and relevant software that can handle differential equations with transcendental functional symbols. In the 2nd year, the project was personally changed, leading to changes, insufficient use of financial resources and complications with dedication
Solution timeline
Realization period - beginning
Jan 1, 2015
Realization period - end
Dec 31, 2017
Project status
U - Finished project
Latest support payment
Apr 5, 2017
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP18-GA0-GA-U/02:1
Data delivery date
May 4, 2018
Finance
Total approved costs
2,610 thou. CZK
Public financial support
2,610 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
2 610 CZK thou.
Public support
2 610 CZK thou.
100%
Provider
Czech Science Foundation
CEP
IN - Informatics
Solution period
01. 01. 2015 - 31. 12. 2017