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.

Publications