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
2001
-
Distributed LTL Model-Checking Based on Negative Cycle Detection
FST-TCS 2001, year: 2001
-
Multi-Agents Systems as Concurrent Constraint Processes
SOFSEM 2001 28th Conf.on Current Trends in Theory and Practice of Informatics, year: 2001
-
On the Power of Labels in Transition Systems
Proceedings of 12th International Conference on Concurrency Theory (CONCUR'01), year: 2001
-
Properties of Distributed Timed-Arc Petri Nets
Proceedings of 21st International Conference on Foundations of SoftwareTechnology and Theoretical Computer Science (FSTTCS'01), year: 2001
-
Randomization Helps in LTL Model Checking
Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001, year: 2001
-
Rewrite Systems with Constraints
EXPRESS'01 the 8th International Workshop on Expressiveness in Concurrency, year: 2001
-
Towards a Notion of Distributed Time for Petri Nets
Proceedings of 22nd International Conference on Application and Theory ofPetri Nets (ICATPN'01), year: 2001
2000
-
Complexity of Weak Bisimilarity and Regularity for BPA and BPP
Expressiveness in Concurrency, EXPRESS'00, year: 2000
-
Constrained Rewrite Transition Systems
Year: 2000, type: R&D Presentation
-
Efficient Verification Algorithms for One-Counter Processes
Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP 2000), year: 2000