| Identifikační kód |
GA201/97/0456 |
| Důvěrnost údajů |
S - Není předmětem státního či obchodního tajemství a data lze v souladu s právními předpisy poskytnout do veřejně přístupných
informačních systémů včetně mezinárodních |
| Název projektu v původním jazyce |
Meze algoritmické verifikovatelnosti nekonečně stavových systémů |
| Název projektu anglicky |
Algorithmic verification boundaries for infinite-state systems |
| Poskytovatel |
GA0 - Grantová agentura České republiky (GA ČR) |
| Program |
GA - Standardní projekty (1993 - 2050) |
| Kategorie VaV |
- |
| Hlavní obor - skupina |
J - Průmysl |
| Hlavní obor |
JC - Počítačový hardware a software |
| Vedlejší obor |
BA - Obecná matematika |
| Další vedlejší obor |
- |
| Zahájení řešení |
1997 |
| Ukončení řešení |
1999 |
| Datum posledního uvolnění účelové podpory |
- |
| Číslo smlouvy |
- |
| Poslední stav řešení |
U - Ukončený (rok ukončení projektu < rok sběru dat, v roce sběru dat již není financován ze SR) |
| Finance projektu | 1996 | 1997 | 1998 | 1999 | 2000 | 2001 | celkem |
|---|
| Výše podpory z národních zdrojů | 0,000 | 200 000,00200 | 295 000,00295 | 338 000,00338 | 0,000 | 0,000 | 833 000,00833 | | Výše podpory z veřej. zahraničních zdrojů *** | 0,000 | 0,000 | 0,000 | 0,000 | 0,000 | 0,000 | 0,000 | | Celkové uznané náklady | 0,000 | 200 000,00200 | 405 000,00405 | 448 000,00448 | 0,000 | 0,000 | 1 053 000,001053 | | Typ | - | čerpané | čerpané | čerpané | - | - | |
** Finance v tisících Kč jsou automaticky zaokrouhleny z částky v jednotkách Kč s přesností na 2 desetinná místa
*** Výše podpory z veřejných zahraničních zdrojů je sledována od období sběru 2020 |
|
Zobrazit skutečně čerpané finance projektu z národních zdrojů »
| Skutečně čerpané finance projektu z národních zdrojů | 1996 | 1997 | 1998 | 1999 | 2000 | 2001 | celkem |
|---|
| Finance | 0,000 | 200 000,00200 | 295 000,00295 | 338 000,00338 | 0,000 | 0,000 | 833 000,00833 |
|
| Druh soutěže |
- |
| Veřejná soutěž ve výzkumu, vývoji a inovacích |
- |
| Cíle řešení v původním jazyce |
Projekt je motivován jednou z živých oblastí současného výzkumu týkajícího se analýzy a verifikace složitých (potenciálně nekonečně stavových) konkurentních systémů. Jedná se o oblast mezi algoritmické verifikovatelnosti, kde verifikací se rozumí ověřování ekvivalence 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 BPA, BPP a Petriho sítě, k nimž přispěl i grant. projekt GA ČR č. 201/93/2123. Hlavním cílem navrhovaného projektu je systematicky prozkoumat zmíněné a příbuzné modely a zaměřit se na: a) charakterizaci rozhodnutelných podtříd vzhledem k běžným ekvivalencím, b) testování regularity (tj. ekvivalence s konečně stavovým systémem), c) rozhodnutelné modálnía temporální logiky či rozumné fragmenty. Zároveň je plánováno studium složitosti příslušných algoritmů a pro vhodné případy jejich prototypová implementace a testování typických případů. Se zřetelem ke zmíněným otázkám bude zkoumána i nově se rozvíjejíc |
| Cíle řešení v anglickém jazyce |
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 |
| Klíčová slova v anglickém jazyce |
- |
| Kontrolní číslo stavu projektu v letech |
1997: 255008
1998: 359220
1999: 426807
2000: 504520 |
| Datum dodání posledního záznamu o projektu |
- |
| Systémové označení dodávky dat |
CEP/2000/GA0/GA00GA/U/6:2 |