Project details


Decidability and complexity of observational equivalences on infinite - state processes

Project Identification:GA201/99/D026
Project Period:9/1999 - 8/2002
Investor:link to a new windowCzech Science Foundation
Programme / Project Type:Standard Projects -
MU Faculty/Unit:
Faculty of Informatics
MU Investigator:Mgr. Jitka Stříbrná, Ph.D.
Project Team Member:Prof. RNDr. Mojmír Křetínský, CSc.
Field:BC - Management theory and systems (B - Physics and mathematics)
Project Website:link to a new window

The aim of the project is to contribute new knowledge to the study of concurrent systems, inparticular with regard to the decidability of the problems connected to verification of infinite - state processes. The main question we want to address is the te sting of certain observational equivalences on potentially infinite - state processes. In particular we want to study strong, and weak bisimulation equivalences on various process algebras, mainly BPA and BPPA, and their extensions PDA and PDDA, fro m the point of view of decidability and computational optimality of decision procedures that might exist. For strong bisimulation equivalence we want to find out whether there exist feasible (polynomial) decision algorithms for the aforementioned pr ocess algebras. In the case of weak bisimulation equivalence we want to investigate whether it is decidable on these classes of processes.