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
2004
-
DP lower bounds for equivalence-checking and model-checking of one-counter automata
Information and Computation, year: 2004, volume: 188, edition: 1
2003
-
Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming
Electronic Notes in Theoretical Computer Science, year: 2003, volume: 68, edition: 3
2002
-
Boundaries and Efficiency of Verification
Proceedings of summer school MOVEP~2002, year: 2002
-
CONCUR 2002 - Concurrency Theory. 13th International Conference. Proceedings.
Year: 2002, number of pages: 609 s.
-
Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming
Foundations of Coordination Languages and Software Architecture (FOCLASA`02), year: 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), year: 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), year: 2002
-
Infinity 2002. 4th International Workshop on Verification of Infinite-State Systems
Year: 2002, number of pages: 106 s.
-
Modifications of Expansion Trees for Weak Bisimulation in BPA
Verification of Infinite-State Systems Infinity'2002, year: 2002
-
Note on the Tableau Technique for Commutative Transition Systems
Proceedings of 5th Foundations of Software Science and Computation Structures (FOSSACS'02), year: 2002