Informace o projektu
Verifikace nekonečně stavových systémů
- Kód projektu
- GA201/03/1161
- Období řešení
- 1/2003 - 12/2005
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Standardní projekty
- Fakulta / Pracoviště MU
- Fakulta informatiky
- Klíčová slova
- concurrency theory, infinite-state systems, equivalence checking, decidability, complexity
- Spolupracující organizace
-
Vysoká škola báňská - Technická univerzita v Ostravě
- Odpovědná osoba prof. RNDr. Petr Jančar, CSc.
Návrh je motivován jednou z živých oblastí současného výzkumu týkajícího se formální verifikace (a tedy i modelování a analýzy) nekonečně stavových souběžných (concurrent) systémů, kde verifikací se rozumí (zkoumání rozhodnutelnosti a složitosti) ověřování jistých sémantických ekvivalencí těchto systémů a jejich temporálně logických vlastností. V poslední době bylo v dané oblasti dosaženo zajímavých výsledků,
např.\,pro kalkuly BPA, BPP, PA, PDA a Petriho sítě, k nimž přispěly i grantové projekty GAČR reg.\,č.\ 201/93/2123, 210/97/0456 a 210/00/0400
řešené týmem, který předkládá tento návrh.
Hlavním cílem navrhovaného projektu je systematicky prozkoumat zmíněné a příbuzné modely a zaměřit se na charakterizaci rozhodnutelných podtříd vzhledem k běžným sémantickým ekvivalencím (a k adekvátním předuspořádáním), na jejich vzájemné vztahy a expresibilitu (včetně
testování regularity a možností konečné charakterizace) a na rozhodnutelné modální a temporální logiky, či jejich rozumné fragmenty.
Dále chceme zkoumat vhodné modely pro oblast (i nemonotonních)souběžných systémů s omezeními (concurrent constraint systems), které by
umožnily asynchronní i synchronní komunikaci v tomto paradigmatu a studovat výše uvedené problémy i pro tyto systémy.
Publikace
Počet publikací: 43
2006
-
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
Automated Technology for Verification and Analysis (ATVA'06), rok: 2006
-
Undecidability Results for Bisimilarity on Prefix Rewrite Systems
LNCS, Foundations of Software Science and Computation Structures (FOSSACS'06), rok: 2006, ročník: 2006, vydání: 3921
-
Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
LNCS, Annual Conference on Computer Science Logic (CSL'06), rok: 2006, ročník: 2006, vydání: 4207
2005
-
Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion
Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), rok: 2005
-
Computing the Expected Accumulated Reward and Gain for a Subclass of Infinite Markov Chains
25th International Conference on Foundations of Software Technology and Theoretical Computer Science, rok: 2005
-
Decidability Issues for Extended Ping-Pong Protocol
Journal of Automated Reasoning, rok: 2005, ročník: ?, vydání: ?
-
Distributed Analysis of Large Systems
Formal Methods for Components and Objects, rok: 2005
-
Characteristic Patterns for LTL
SOFSEM 2005: Theory and Practice of Computer Science, rok: 2005
-
On the Controller Synthesis for Finite-State Markov Decision Processes
25th International Conference on Foundations of Software Technology and Theoretical Computer Science, rok: 2005
-
On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005), rok: 2005