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
2006
-
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
Automated Technology for Verification and Analysis (ATVA'06), year: 2006
-
Undecidability Results for Bisimilarity on Prefix Rewrite Systems
LNCS, Foundations of Software Science and Computation Structures (FOSSACS'06), year: 2006, volume: 2006, edition: 3921
-
Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
LNCS, Annual Conference on Computer Science Logic (CSL'06), year: 2006, volume: 2006, edition: 4207
2005
-
Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion
Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), year: 2005
-
Computing the Expected Accumulated Reward and Gain for a Subclass of Infinite Markov Chains
25th International Conference on Foundations of Software Technology and Theoretical Computer Science, year: 2005
-
Decidability Issues for Extended Ping-Pong Protocol
Journal of Automated Reasoning, year: 2005, volume: ?, edition: ?
-
Distributed Analysis of Large Systems
Formal Methods for Components and Objects, year: 2005
-
Characteristic Patterns for LTL
SOFSEM 2005: Theory and Practice of Computer Science, year: 2005
-
On the Controller Synthesis for Finite-State Markov Decision Processes
25th International Conference on Foundations of Software Technology and Theoretical Computer Science, year: 2005
-
On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005), year: 2005