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
2011
-
Efficient Analysis of Probabilistic Programs with an Unbounded Counter
Computer Aided Verification, 23rd International Conference, CAV 2011, rok: 2011
-
Fixed-delay Events in Generalized Semi-Markov Processes Revisited
CONCUR 2011 - Concurrency Theory: 22nd International Conference, rok: 2011
-
Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata
HSCC 11: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, rok: 2011
-
Qualitative Reachability in Stochastic BPA Games
Information and Computation, rok: 2011, ročník: 209, vydání: 8
-
Runtime Analysis of Probabilistic Programs with Unbounded Recursion
Proceedings of 38th International Colloquium on Automata, Languages and Programming (ICALP 2011), rok: 2011
-
Turn-Based Stochastic Games
Lectures in Game Theory for Computer Scientists, rok: 2011, počet stran: 39 s.
-
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes
Proceedings 26th Annual IEEE Symposium on Logic in Computer Science, rok: 2011
2010
-
Decidable Race Condition and Open Coregions in HMSC
Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010), rok: 2010
-
On the Complexity of Checking Semantic Equivalences between Pushdown Processes and Finite-state Processes
Information and Computation, rok: 2010, ročník: 208, vydání: February
-
One-Counter Stochastic Games
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), rok: 2010