Informace o projektu
Nekonečně stavové souběžné systémy - modely a verifikace
- Kód projektu
- GA201/00/0400
- Období řešení
- 1/2000 - 12/2002
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Standardní projekty
- Fakulta / Pracoviště MU
- Fakulta informatiky
- WWW stránky projektu
- http://www.fi.muni.cz/usr/kretinsky/projects/GACR201000400.html
- Spolupracující organizace
-
Vysoká škola báňská - Technická univerzita v Ostravě
- Odpovědná osoba prof. RNDr. Petr Jančar, CSc.
Projekt je motivován jednou z živých oblastí současného výzkumu týkajícího se modelování, analýzy a verifikace složitých (potenciálně nekonečně stavových) souběžných (concurrent) systémů. Jejich verifikací se rozumí (zkoumání možností algoritmického) ověřování jistých ekvivalencí těchto systémů, jejich temporálně logických vlastností apod. V poslední době bylo v dané oblasti dosaženo zajímavých výsledků, např. pro kalkuly BBA, BPP, PA a Petriho sítě, k nimž přispěly grant. projekty GAČR č. 201/93/2123 a č. 210/97/0456 ř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 ekvivalencím a jejich vzájemné vztahy, testování regularity (tj. ekvivalence s konečně stavovým systémem) a možností konečné charakterizace (i vzhledem k adekvátním předuspořádáním), a na rozhodnutelné modální a temporální logiky, či rozumné fragmenty.
Publikace
Počet publikací: 36
2002
-
On the Complexity of Semantic Equivalences for Pushdown Automata and BPA
Proceedings of 27th International Symposium on Mathematical Foundations of Computer Science (MFCS 2002), rok: 2002
-
Roadmap of Infinite Results
Bulletin of the European Association for Theoretical Computer Science, rok: 2002, ročník: 2002, vydání: 78
-
Simulation Preorder over Simple Process Algebras
Information and Computation, rok: 2002, ročník: 173, vydání: 2
-
Strong Bisimilarity and Regularity of Basic Parallel Processes is PSPACE-Hard
Proceedings of 19th International Symposium on Theoretical Aspects of Computer Science (STACS'02), rok: 2002
-
Strong Bisimilarity and Regularity of Basic Process Algebra is PSPACE-Hard
Proceedings of 29th International Colloquium on Automata, Languages and Programming (ICALP'02), rok: 2002
-
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL
Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02), rok: 2002
-
Undecidability of Weak Bisimilarity for Pushdown Processes
Proceedings of 13th International Conference on Concurrency Theory (CONCUR'02), rok: 2002
-
Weak Bisimilarity between Finite-State Systems and BPA or normed BPP is Decidable in Polynomial Time
Theoretical Computer Science, rok: 2002, ročník: 270, vydání: 1-2
-
Why is Simulation Harder Than Bisimulation?
Proceedings of 13th International Conference on Concurrency Theory (CONCUR 2002), rok: 2002
2001
-
Basic Process Algebra with Deadlocking States
Theoretical Computer Science, rok: 2001, ročník: 2001, vydání: 266(1-2)