Project information
Analysis of Concurrent Infinite State Systems
- Project Identification
- GA201/93/2123
- Project Period
- 1/1993 - 1/1995
- Investor / Pogramme / Project type
-
Czech Science Foundation
- Standard Projects
- MU Faculty or unit
- Faculty of Informatics
- Project Website
- http://www.fi.muni.cz/usr/kretinsky/projects/GACR201932123.html
- Cooperating Organization
-
University of Ostrava
- Responsible person 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.
Publications
Total number of publications: 16
1996
-
A process Algebra for Synchronous Concurrent Constraint Programming
TR City University, U.K., year: 1996, volume: 1996, edition: 6
-
A process algebra for Synchronous Concurrent Constraint Programming
ALP96: Fifth Int. Conference on Algebraic and Logic Programm, year: 1996, number of pages: 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), year: 1996
-
Comparing Expressibility of Normed BPA and Normed BPP Processes
FI MU Report Series, year: 1996, volume: 1996, edition: RS-96-02
-
New versions of asks for synchronous communication in concurrent constraint programming
TR City University, U.K., year: 1996, volume: 1996, edition: 3
-
On the Relationship between Sequential and Parallel Compositions in Process Algebras
CSL96 - The 1996 Annual Conference of the European Assoc.., year: 1996, number of pages: 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), year: 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), year: 1996
-
Regularity is Decidable for Normed PA Processes in Polynomial Time
FI MU Report Series, year: 1996, volume: 1996, edition: RS-96-01
1995
-
A process algebra for Synchronous Concurrent Constraint Programming
Technical Report of Namur University, year: 1995, volume: 1995, edition: 8