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
2004
-
Recursive Ping-Pong Protocols
Proceedings of 4th International Workshop on Issues in the Theory of Security (WITS'04), rok: 2004
-
Roadmap of Infinite Results
Current Trends in Theoretical Computer Science, The Challenge of the New Century, rok: 2004, ročník: 2, vydání: 1
2003
-
A Logical Viewpoint on Process-algebraic Quotients
Journal of logic and computation, rok: 2003, ročník: 13, vydání: 6
-
Complexity of Weak Bisimilarity and Regularity for BPA and BPP
Mathematical Structures in Computer Science, rok: 2003, ročník: 12, vydání: 1
-
Deciding Bisimilarity between BPA and BPP Processes
Proceedings of 14th International Conference on Concurrency Theory (CONCUR 2003), rok: 2003
-
Fast Mu-calculus Model Checking when Tree-width is Bounded
CAV 2003, rok: 2003
-
Modelling Multi-Agents Systems as Concurrent Constraint Processes
Computing and Informatics, rok: 2003, ročník: 21, vydání: 6
-
On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit
Prelim.Proc.of the 5th Internat.Workshop on Verification of Infinite-State Systems (INFINITY'2003), rok: 2003
-
Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds
Acta Informatica, rok: 2003, ročník: 39, vydání: 1
-
The Complexity of Bisimilarity-Checking for One-Counter Processes
Theoretical Computer Science, rok: 2003, ročník: 304, vydání: 1-3