Meze algoritmické verifikovatelnosti nekonečně stavových systémů

Poskytovatel

Grantová agentura České republiky

Program

Standardní projekty

Veřejná soutěž

—

Hlavní účastníci

Vysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky

Druh soutěže

—

Číslo smlouvy

—

Název projektu anglicky

Algorithmic verification boundaries for infinite-state systems

Anotace anglicky

The project is motivated by a live current research area concerning analysis and verification of complex (infinite state) concurrent systems It is the area of boundaries for algorithmic verification, where verification means checking equivalencies of systems, their temporal logic properties etc. Recently, several interesting results have been obtained in the given area, e.g. for calculi BPA, BPP, and Petri nets, to which also the grant of the Czech Grant Agency, No. 201/93/2123, has contributed. The main target of the proposed project is to explore systematically the mentioned and related models and focus on : a) characterization of decidable subclasses wrt usual equivalences b)testin regularity (i.e. equivalence with a finite-state system ) c) decidable modal and temporal logics, or reasonable fragments. It is also planned to study complexity of relevant algorithms, and for suitable cases their implementation and testing. In addition, the recent research area of concurrent constarint systems

Kategorie VaV

—

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

Jde o velmi dobře vedený projekt s dobrými výsledky, které jsou přínosem pro rozvoj oboru. Charakteristika výsledků v závěrečné kartě je v pořádku. Projekt měl význam především pro rozvoj oboru a částečně i pro výchovu studentů. Výstupy z projektu, přede

Zahájení řešení

1. 1. 1997

Ukončení řešení

1. 1. 1999

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

CEP/2000/GA0/GA00GA/U/6:2

Datum dodání záznamu

—

Celkové uznané náklady

1 053 tis. Kč

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

833 tis. Kč

Ostatní veřejné zdroje financování

0 tis. Kč

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

0 tis. Kč