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
2005
-
Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances
Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), rok: 2005
-
Reachability Analysis of Multithreaded Software with Asynchronous Communication
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, rok: 2005
-
Reachability of Hennessy - Milner properties for weakly extended PRS
FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, rok: 2005
-
Recursion vs. Replication in Simple Cryptographic Protocols
Proceedings of 31st Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM'05), rok: 2005
-
Refining Undecidability Border of Weak Bisimilarity.
BRICS Notes Series, rok: 2005, ročník: 2005, vydání: NS-05-4
-
Refining Undecidability Border of Weak Bisimilarity. (full version of INFINITY 2005 paper)
Rok: 2005, druh: Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)
-
The stuttering principle revisited
Acta informatica, rok: 2005, ročník: 41, vydání: 7/8
-
Timed-Arc Petri Nets vs. Networks of Timed Automata
Proceedings of the 26th International Conference on Application and Theory of {P}etri Nets (ICATPN 2005), rok: 2005
2004
-
A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications
Proceedings of 15th International Conference on Concurrency Theory (CONCUR 2004), rok: 2004
-
A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata
Exploring New Frontiers of Theoretical Informatics : IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), rok: 2004