Informace o projektu
Formální metody pro analýzu a verifikaci komplexních systémů
- Kód projektu
- GAP202/10/1469
- Období řešení
- 1/2010 - 12/2014
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Standardní projekty
- Fakulta / Pracoviště MU
-
Fakulta informatiky
- prof. RNDr. Antonín Kučera, Ph.D.
- doc. RNDr. Tomáš Brázdil, Ph.D.
- RNDr. Václav Brožek, Ph.D.
- RNDr. Vojtěch Forejt, Ph.D., LL.B. (Hons)
- doc. RNDr. Vojtěch Řehák, Ph.D.
- prof. RNDr. Jan Strejček, Ph.D.
- Klíčová slova
- formální verifikace; stochastické systémy; teorie automatů; temporální logiky
Ve formální verifikaci se pomocí matematických metod dokazuje, že daný
systém splňuje požadované vlastnosti. Verifikační a analytické metody
jsou obvykle tvořeny na míru dané třídě systémů, která je
charakterizována nějakou specifickou vlastností jako například
náhodnost, závislost na reálném čase, počet stavů, apod. Reálné
systémy jsou ale obvykle komplexní a kombinují více těchto
charakteristických vlastností.
Naším cílem je studovat verifikační a analytické metody pro systémy,
které kombinují náhodnost s dalšími aspekty chování, jako je
nedeterministická volba, reálný čas, interakce, apod. Speciální
pozornost bude věnována systémům s nekonečně mnoha stavy. Studovány
budou vlastnosti formálních modelů těchto systémů, například
stochastických her s reálným časem, pravděpodobnostních zásobníkových
automatů, systémů s čítači, popisných jazyků komunikačních protokolů,
apod. Mezi cíle výzkumu patří také návrh nových formalismů vhodných
pro specifikaci vlastností takových systémů a analýza
rozhodnutelnosti a složitosti příslušných verifikačních problémů.
Publikace
Počet publikací: 33
2013
-
On Refinements of Boolean and Parametric Modal Transition Systems
Theoretical Aspects of Computing - ICTAC 2013 - 10th International Colloquium, rok: 2013
2012
-
Almost linear Büchi automata
Mathematical Structures in Computer Science, rok: 2012, ročník: 22, vydání: 2, DOI
-
Dual-Priced Modal Transition Systems with Time Durations
LPAR-18 - Logic for Programming, Artificial Intelligence, and Reasoning: 18th International Conference, rok: 2012
-
Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
Computer Aided Verification - 24th International Conference, CAV 2012, rok: 2012
-
EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems
Information and Computation, rok: 2012, ročník: 218, vydání: September, DOI
-
LTL to Büchi Automata Translation: Fast and More Deterministic
TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, rok: 2012
-
Minimizing Expected Termination Time in One-Counter Markov Decision Processes
Proceedings of 39th International Colloquium on Automata, Languages and Programming (ICALP 2012), rok: 2012
-
Space-efficient scheduling of stochastically generated tasks
Information and Computation, rok: 2012, ročník: 210, vydání: January, DOI
-
Stabilization of Branching Queueing Networks
Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science, rok: 2012
2011
-
Approximating the Termination Value of One-Counter MDPs and Stochastic Games
Proceedings of 38th International Colloquium on Automata, Languages and Programming (ICALP 2011), rok: 2011