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
2004
-
DP lower bounds for equivalence-checking and model-checking of one-counter automata
Information and Computation, rok: 2004, ročník: 188, vydání: 1
2003
-
Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming
Electronic Notes in Theoretical Computer Science, rok: 2003, ročník: 68, vydání: 3
2002
-
Boundaries and Efficiency of Verification
Proceedings of summer school MOVEP~2002, rok: 2002
-
CONCUR 2002 - Concurrency Theory. 13th International Conference. Proceedings.
Rok: 2002, počet stran: 609 s.
-
Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming
Foundations of Coordination Languages and Software Architecture (FOCLASA`02), rok: 2002
-
Equivalence-Checking with Infinite-State Systems: Techniques and Results.
Proceedings of 29th Conference on Current Trends in Theory and Practice of Informatics (SOFSEM 2002), rok: 2002
-
Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds
Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002), rok: 2002
-
Infinity 2002. 4th International Workshop on Verification of Infinite-State Systems
Rok: 2002, počet stran: 106 s.
-
Modifications of Expansion Trees for Weak Bisimulation in BPA
Verification of Infinite-State Systems Infinity'2002, rok: 2002
-
Note on the Tableau Technique for Commutative Transition Systems
Proceedings of 5th Foundations of Software Science and Computation Structures (FOSSACS'02), rok: 2002