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
2018
-
Black Ninjas in the Dark: Formal Analysis of Population Protocols
2018 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), rok: 2018
2014
-
Branching-time model-checking of probabilistic pushdown automata
Journal of Computer and System Sciences, rok: 2014, ročník: 80, vydání: 1, DOI
-
Minimizing Running Costs in Consumption Systems
Computer Aided Verification, rok: 2014
-
Solving adversarial patrolling games with bounded error: (extended abstract)
Proceedings of the 13th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'14), rok: 2014
-
Symbiotic 2: More Precise Slicing (Competition Contribution)
Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, rok: 2014
2013
-
Approximating the termination value of one-counter MDPs and stochastic games
Information and Computation, rok: 2013, ročník: 222, vydání: January, DOI
-
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
Computer Aided Verification - 25th International Conference, CAV 2013, rok: 2013
-
Comparison of LTL to Deterministic Rabin Automata Translators
Logic for Programming Artificial Intelligence and Reasoning, LPAR-19, rok: 2013
-
Continuous-Time Stochastic Games with Time-Bounded Reachability
Information and Computation, rok: 2013, ročník: 224, vydání: 1, DOI
-
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory
CONCUR 2013 - Concurrency Theory - 24th International Conference, rok: 2013