Project information
Infinite state concurrent systems - models and verification
- Project Identification
- GA201/00/0400
- Project Period
- 1/2000 - 12/2002
- 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/GACR201000400.html
- Cooperating Organization
-
Technical University Ostrava
- Responsible person prof. RNDr. Petr Jančar, CSc.
This project proposal is motivated by one of the concurrent research trends in concurrency theory, e.i. by modelling, analysis and verification of concurrent infinite state systems. Verification is understood as (an examination of possibly algorithmic) c hecking of semantic equivalences between these systems (processes) or checking their properties expressed in suitable modal logics etc. Recently, some interesting results have been achieved in this area, e.g. for calculi BPA, PDA, BPP, PA, and Petri nets ; some contributions were made by members of the team submitting this proposal. The main goal is to investigate the mentioned and related classes with aims to characterise (sub) classes w.r.t. decidability of (some) equivalences, to describe their relati onships, to study regularity conditions, and to examine the possibilities of their so called characterisations w.r.t. relevant preorders. Also it is suggested to study decidability issues of modal a temporal logics (or their reasonable fragments) for the
Publications
Total number of publications: 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), year: 2002
-
Roadmap of Infinite Results
Bulletin of the European Association for Theoretical Computer Science, year: 2002, volume: 2002, edition: 78
-
Simulation Preorder over Simple Process Algebras
Information and Computation, year: 2002, volume: 173, edition: 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), year: 2002
-
Strong Bisimilarity and Regularity of Basic Process Algebra is PSPACE-Hard
Proceedings of 29th International Colloquium on Automata, Languages and Programming (ICALP'02), year: 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), year: 2002
-
Undecidability of Weak Bisimilarity for Pushdown Processes
Proceedings of 13th International Conference on Concurrency Theory (CONCUR'02), year: 2002
-
Weak Bisimilarity between Finite-State Systems and BPA or normed BPP is Decidable in Polynomial Time
Theoretical Computer Science, year: 2002, volume: 270, edition: 1-2
-
Why is Simulation Harder Than Bisimulation?
Proceedings of 13th International Conference on Concurrency Theory (CONCUR 2002), year: 2002
2001
-
Basic Process Algebra with Deadlocking States
Theoretical Computer Science, year: 2001, volume: 2001, edition: 266(1-2)