Faculty of Informatics logo Analysis of concurrent infinite state systems
- - - - -
Funding: Grant Agency of Czech Republic, Project No. 201/93/2123
Starting Date: October 1, 1993
Duration: 3 years
Project Leader: M. Kretinsky
Co-leader: P. Jancar (TU Ostrava)
- - - - -
Description Characteristic of the project:
Analysis and verification of finite-state concurrent systems is algorithmically tractable since it is possible to check by an exhaustive search whether some desirable property holds. In general, one cannot expect properties of infinite-state systems to be decidable, however some recent results are quite surprising (e.g. decidability of (strong) bisimulation relation for context-free processes) and offering a number of new problems.
This project proposes to study if there are further decidable classes (w.r.t. strong bisimulation equivalence) of infinite-state processes and classes of properties (characterisable by suitable modal and temporal logics) for context-free processes which might be decidable as well. Also, it is proposed to study what notations and frameworks are needed for representing the infinite sets of states involved (with perspective of developing an experimental tool).
- - - - -
Faculty of Informatics, Masaryk University Brno
University of Ostrava
- - - - -
People L. Brim (FI)
P. Jancar (U. of Ostrava)
M. Kretinsky (FI)
A. Kucera (FI)
- - - - -
Contact M. Kretinsky
- - - - -
Publications List of publications (by FI staff only)