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).
Organisations
University of Ostrava
P. Jancar (U. of Ostrava)
M. Kretinsky (FI)
A. Kucera (FI)