This project proposal 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 the team submitting
this proposal.

The main goal is to investigate the mentioned and related classes with
aims to characterise (sub)classes w.r.t.~decidability of (some)
equivalences and preorders, to describe their mutual relationship and
relative expressibility (incl.\,regularity and so called
characterisations w.r.t.\,preorders), and to study complexity of
respective decision algorithms. Also it is suggested to study
decidability and complexity issues of modal and temporal logics (or
their fragments) for these classes. The other goal is to investigate
(not only monotonic) models for concurrent constrained processes to
allow asynchronous and synchronous communication, and to develop
frameworks for reasoning about these systems.

Publications