| Description
| - 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. Also it is suggested to study decidability issues of modal a temporal logics (or their reasonable fragments) (en)
- Projekt je motivován jednou z živých oblastí současného výzkumu týkajícího se modelování, analýzy a verifikace složitých (potenciálně nekonečně stavových) souběžných (concurrent) systémů. Jejich verifikací se rozumí (zkoumání možností algoritmického) ověřování jistých ekvivalencí těchto systémů, jejich temporálně logických vlastností apod. V poslední době bylo v dané oblasti dosaženo zajímavých výsledků, např. pro kalkuly BBA, BPP, PA a Petriho sítě, k nimž přispěly grant. projekty GAČR č. 201/93/212a č. 210/97/0456 ř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 k běžným ekvivalencím a jejich vzájemné vztahy, testování regularity (tj. ekvivalence s konečně stavovým systémem) a možností konečné charakterizace (i vzhledem k adekvátním předuspořádáním), a na rozhodnutelné modální a temporální logiky, či rozumné fragmenty. Dále chceme zkoumat vhodné model
|
![[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)