Verifikace nekonečně stavových systémů

Poskytovatel

Grantová agentura České republiky

Program

Standardní projekty

Veřejná soutěž

Standardní projekty 2 (SGA02003GA-ST)

Hlavní účastníci

Masarykova univerzita / Fakulta informatiky

Druh soutěže

VS - Veřejná soutěž

Číslo smlouvy

—

Název projektu anglicky

Verification of infinite-state systems

Anotace anglicky

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; somecontributions 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 theirmutual 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

Kategorie VaV

ZV - Základní výzkum

CEP - hlavní obor

JC - Počítačový hardware a software

CEP - vedlejší obor

BA - Obecná matematika

CEP - další vedlejší obor

—

OECD FORD - odpovídající obory <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)

10101 - Pure mathematics<br>20206 - Computer hardware and architecture

Hodnocení poskytovatelem

V - Vynikající výsledky projektu (s mezinárodním významem atd.)

Zhodnocení výsledků projektu

Hlavní výsledky patří do oblasti základního výzkumu v oblasti formální verifikace nekonečně stavových souběžných (concurrent) systémů, a to jak pro standardní modely procesů, tak i jejich rozšíření. Na těchto třídách procesů byly studovány zejména problé

Zahájení řešení

1. 1. 2003

Ukončení řešení

1. 1. 2005

Poslední stav řešení

U - Ukončený projekt

Poslední uvolnění podpory

—

Důvěrnost údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Systémové označení dodávky dat

CEP06-GA0-GA-U/07:6

Datum dodání záznamu

15. 1. 2009

Celkové uznané náklady

6 141 tis. Kč

Výše podpory ze státního rozpočtu

2 211 tis. Kč

Ostatní veřejné zdroje financování

3 930 tis. Kč

Neveřejné tuz. a zahr. zdroje finan.

0 tis. Kč