Title
Nekonečně stavové souběžné systémy - modely a verifikace
Code
GA201/00/0400
Summary
This project proposal is motivated by one of the concurrent research trends in concurrency theory, e.i. 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, to describe their relationships, to study regularity conditions, and to examine the possibilities of their so called characterisations w.r.t. relevant preorders.
Start year
2000
End year
2002
Provider
Grantová agentura ČR
Category
Obecná forma
Type
Standardní projekty
Solver
Information system of research, development and innovation (in Czech)