This project is motivated by one of the current research trends in concurrency theory, i.e. by modelling, analysis and verification of concurrent infinite state systems. Verification is understood as (an examination of possibly algorithmic) checking 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 this project research team (see past projects of of the Grant Agency of the Czech Republic, grant no. 201/93/2123 and grant no. 201/97/0456 ).

The main goal is to investigate the mentioned and related classes with aims

• to characterise (sub)classes w.r.t. decidability of (some) semantic (behavioral) equivalences,
• to describe their relationships,
• to study regularity conditions, and
• to examine the possibilities of their so called characterisations w.r.t. relevant preorders.

• (Un)decidable problems in process algebras
  Grant Agency of the Czech Republic, grant no. 201/98/P046
  (project leader: Antonín Kučera)
• Decidability and complexity of behavioral equivalences on infinite state processes
  Grant Agency of the Czech Republic, grant no. 201/99/D026
  (project leader: Jitka Stříbrná)