Control Synthesis and Formal Verification of Complex Hybrid Systems
Project goals
The aim of the project is to support and extend cooperation between laboratory ParaDiSe at Faculty of Informatics Masaryk University (FI MU) and laboratory HyNeSs at Boston University (BU) in research and development of techniques for controller synthesis and formal verification of complex hybrid systems with specialization towards robotic systems. One of the key points of the cooperation is to establish conditions for direct research contacts and mutual usage of research infrastructure of both partners. The project connects two complementing research areas. Project activities will lead to design of new methods and techniques for control and verification of hybrid systems by adapting verification techniques of temporal properties of discrete concurrentsystems developed at FI MU and methods for modeling and discretization of hybrid systems, which is a long-term research topic at BU. Combination of both will be basis for development of approach and experimental tool for control and verification.
Keywords
control strategy synthesisformal verificationhybrid and continuous systemsrobotic systemstemporal logic
Public support
Provider
Ministry of Education, Youth and Sports
Programme
KONTAKT II
Call for proposals
KONTAKT II 1 (SMSM2011LH1)
Main participants
—
Contest type
VS - Public tender
Contract ID
MSMT-6784/2013-311
Alternative language
Project name in Czech
Řízení a ověřování vlastností komplexních hybridních systémů
Annotation in Czech
Cílem projektu je podpořit a rozšířit vzájemnou spolupráci mezi laboratoří ParaDiSe na Fakultě informatiky Masarykovy univerzity (FI MU) a laboratoří HyNeSs na Boston University (BU) v oblasti výzkumu a vývoje technik pro syntézu řídících strategií a ověřování komplexních hybridních systémů, s částečnou specializací na robotické systémy. Jedním z hlavních bodů spolupráce je vytvoření podmínek pro bezprostřední vědecké kontakty a využívání výzkumné infrastruktury obou zúčastněných partnerů. Svým odbornýmzaměřením projekt vhodně propojuje doplňující se výzkumné aktivity obou partnerských týmů. Aktivity projektu směřují k návrhu a vývoji nových metod a technik pro řízení a verifikaci hybridních systémů, adaptujících techniky verifikace temporálních vlastností diskrétních souběžných systémů vybudované na FI MU a metody modelování a diskretizace hybridních systémů, kterým se dlouhodobě věnuje tým na BU. Kombinací obou bude vybudován přístup a experimentální nástroj pro efektivní řízení a verifikaci.
Scientific branches
Completed project evaluation
Provider evaluation
V - Vynikající výsledky projektu (s mezinárodním významem atd.)
Project results evaluation
The last year of the project aimed at analysis and control synthesis for discrete as well as hybrid models, with one or multiple agents. Results are based on the use of formal methods and supported by simulations or experiments on a robotic platform. Theresults include one journal and four conference papers. A tool ConTool was created for synthesis and simulation of control for discrete models.
Solution timeline
Realization period - beginning
Mar 1, 2011
Realization period - end
Dec 31, 2014
Project status
U - Finished project
Latest support payment
Mar 3, 2014
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
CEP15-MSM-LH-U/01:1
Data delivery date
Jul 2, 2015
Finance
Total approved costs
2,506 thou. CZK
Public financial support
2,506 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
2 506 CZK thou.
Public support
2 506 CZK thou.
100%
Provider
Ministry of Education, Youth and Sports
CEP
IN - Informatics
Solution period
01. 03. 2011 - 31. 12. 2014