Project information
Verification of infinite-state systems
- Project Identification
- GA201/03/1161
- Project Period
- 1/2003 - 12/2005
- Investor / Pogramme / Project type
-
Czech Science Foundation
- Standard Projects
- MU Faculty or unit
- Faculty of Informatics
- Keywords
- concurrency theory, infinite-state systems, equivalence checking, decidability, complexity
- Cooperating Organization
-
Technical University Ostrava
- Responsible person prof. RNDr. Petr Jančar, CSc.
This project proposal is motivated by one of the current research trends
in concurrency theory, i.e.~by modelling, analysis and verification of
concurrent infinite state systems. Verification is understood as (an
examination of possibly algorithmic) checking 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 and preorders, to describe their mutual relationship and
relative expressibility (incl.\,regularity and so called
characterisations w.r.t.\,preorders), and to study complexity of
respective decision algorithms. Also it is suggested to study
decidability and complexity issues of modal and temporal logics (or
their fragments) for these classes. The other goal is to investigate
(not only monotonic) models for concurrent constrained processes to
allow asynchronous and synchronous communication, and to develop
frameworks for reasoning about these systems.
Publications
Total number of publications: 43
2004
-
Completeness Results for Undecidable Bisimilarity Problems
Proccedings of the 5th International Workshop on Verification of Infinite-State Systems (INFINITY'03), year: 2004
-
Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems
Proceedings of 15th International Conference on Concurrency Theory (CONCUR 2004), year: 2004
-
DP lower bounds for equivalence-checking and model-checking of one-counter automata
Information and Computation, year: 2004, volume: 188, edition: 1
-
Extended Process Rewrite Systems: Expressiveness and Reachability
CONCUR 2004 - Concurrency Theory, year: 2004
-
Highly Undecidable Questions for Process Algebras
Proceedings of 3rd IFIP International Conference on Theoretical Computer Science (TCS'04), year: 2004
-
Model Checking Probabilistic Pushdown Automata
Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), year: 2004
-
On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit
INFINITY'2003: 5th International Workshop on Verification of Infinite-State Systems, year: 2004
-
On the Computational Complexity of Bisimulation, Redux
Information and Computation, year: 2004, volume: ?, edition: ?
-
On the Expressive Power of Extended Process Rewrite Systems
BRICS Report Series, year: 2004, volume: 2004, edition: RS-04-7
-
Reachability for Extended Process Rewrite Systems
MOVEP'04: 6th school on MOdeling and VErifying parallel Processes, year: 2004