Informace o projektu
Analýza konkurentních nekonečně stavových systémů
- Kód projektu
- GA201/93/2123
- Období řešení
- 1/1993 - 1/1995
- 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/GACR201932123.html
- Spolupracující organizace
-
Ostravská univerzita v Ostravě
- Odpovědná osoba prof. RNDr. Petr Jančar, CSc.
Analýza a verifikace vlastností konkurentních, konečně-stavových systémů je díky konečné množině stavů algoritmicky zvládnutelná, neboť ji lze provádět prohledáváním celého stavového prostoru procesu. Obecně jistě nelze očekávat, že vlastnosti nekonečně stavových problémů budou rozhodnutelné, avšak některé nejnovější výsledky jsou do značné míry překvapivé (např. rozhodnutelnost bisimulativní ekvivalence pro bezkontextové procesy) a nabízí celou řadu nových problémů. Návrh je zaměřen na studium otázek (ne)rozhodnutelnosti dalších tříd nekonečně stavových procesů a otázek (ne)rozhodnutelnosti dalších vlastností bezkontextových procesů. Současně se navrhuje zkoumat notaci, jež by umožnila vhodně reprezenovat nekonečné množiny stavů pro omezené třídy modelů (s pespektivním cílem tvorby experimentálního nástroje). Součástí návrhu je provedení analýzy typických případů procesů (case study) pomocí vhodného softwarového nástroje.
Publikace
Počet publikací: 16
1996
-
A process Algebra for Synchronous Concurrent Constraint Programming
TR City University, U.K., rok: 1996, ročník: 1996, vydání: 6
-
A process algebra for Synchronous Concurrent Constraint Programming
ALP96: Fifth Int. Conference on Algebraic and Logic Programm, rok: 1996, počet stran: 14 s.
-
Bisimilarity is Decidable in the Union of Normed BPA and Normed BPP Processes
Proceedings of 1st International Workshop on Verification of Infinite State Systems (INFINITY'96), rok: 1996
-
Comparing Expressibility of Normed BPA and Normed BPP Processes
FI MU Report Series, rok: 1996, ročník: 1996, vydání: RS-96-02
-
New versions of asks for synchronous communication in concurrent constraint programming
TR City University, U.K., rok: 1996, ročník: 1996, vydání: 3
-
On the Relationship between Sequential and Parallel Compositions in Process Algebras
CSL96 - The 1996 Annual Conference of the European Assoc.., rok: 1996, počet stran: 3 s.
-
Regularity is Decidable for Normed BPA and Normed BPP Processes in Polynomial Time.
Proceedings of 23rd Seminar on Current Trends in Theory and Practice of Informatics (SOFSEM´96), rok: 1996
-
Regularity is Decidable for Normed PA Processes in Polynomial Time
Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS´96), rok: 1996
-
Regularity is Decidable for Normed PA Processes in Polynomial Time
FI MU Report Series, rok: 1996, ročník: 1996, vydání: RS-96-01
1995
-
A process algebra for Synchronous Concurrent Constraint Programming
Technical Report of Namur University, rok: 1995, ročník: 1995, vydání: 8