Title
Verifikace nekonečně stavových systémů
Code
GA201/03/1161
Summary
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)check ing 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 Petrinets; 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, todescribe their mutual relationship and relative expressibility (incl. regularity and so called characterisations w.r.t. preorders), and to study complexity of respective decision algorithms.
Start year
2003
End year
2005
Provider
Grantová agentura ČR
Category
Obecná forma
Type
Standardní projekty
Solver
Information system of research, development and innovation (in Czech)