| Description
| - 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 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. Also it is suggested to study decidability and complexity (en)
- Návrh je motivován jednou z živých oblastí současného výzkumu týkajícího se formální verifikace (a tedy i modelování a analýzy) nekonečně stavových souběžných (concurrent) systémů, kde verifikací se rozumí (zkoumání rozhodnutelnosti a složitosti)ověřování jistých sémantických ekvivalencí těchto systémů a jejich temporálně logických vlastností. V poslední době bylo v dané oblasti dosaženo zajímavých výsledků,např.\,pro kalkuly BPA, BPP, PA, PDA a Petriho sítě, k nimž přispěly i grantové projektyGAČR reg.č. 201/93/2123, 210/97/0456 a 210/00/0400 řešené týmem, který předkládá tento návrh. Hlavním cílem navrhovaného projektu je systematicky prozkoumat zmíněné a příbuzné modely a zaměřit se na charakterizaci rozhodnutelných podtříd vzhledem kběžným sémantickým ekvivalencím (a k adekvátním předuspořádáním), na jejich vzájemné vztahy a expresibilitu (včetně testování regularity a možností konečné charakterizace) a na rozhodnutelné modální a temporální logiky, či jejich rozumné fragmenty. Dále
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)