| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/11:00049982 |
| Název v původním jazyce | Modal Transition Systems: Composition and LTL Model Checking |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor | IN - Informatika |
| Rok uplatnění | 2011 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů |
| Počet výskytů výsledku | 2 |
| Údaje z Hodnocení výsledků výzkumných organizací 2014 |
| Výsledek byl hodnocen v Pilíři I |
| Rozsah vyřazení výsledku | Tento výskyt výsledku není vyřazen |
| Zařazení výsledku v hodnocení | D - Článek ve sborníku |
| Skupina oboru v hodnocení | 04 - Technické a informatické vědy |
| Konkrétní způsob(y) hodnocení výsledku | Výsledek hodnocený již v předchozím hodnocení, body se přebírají |
| Bodové ohodnocení | 44,387 |
| Faktor korekce | 100,9 % |
| Body (upravené podle přílohy č. 8 Metodiky) | 44,799 |
| Rozdělení výsledku mezi předkladatele |
| Organizace | Výzkumná organizace? | Podíl | Body | Body (upravené podle přílohy č. 8 Metodiky) |
|---|
| Masarykova univerzita / Fakulta informatiky | ano | 100,0 % | 44,387 | 44,799 |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 3 |
| Počet domácích tvůrců | 3 |
| Tvůrce | Beneš Nikola (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 2050587) |
| Tvůrce | Černá Ivana (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 2361132) |
| Tvůrce | Křetínský Jan (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku; vedidk: 3503054) |
| Údaje blíže specifikující výsledek |
| Popis v původním jazyce | Modal transition systems (MTS) is a~well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we provide algorithms showing that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we identify an error in a~previous attempt at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition. Secondly, we give a~solution to the common implementation and conjunctive composition problems lowering the complexity from EXPTIME to PTIME. |
| Klíčová slova | modal transition systems; model checking; refinement; conjunction |
| Název sborníku | ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium |
| Rozsah stran | 228-242 |
| Počet stran výsledku | 15 |
| ISBN | 978-3-642-24371-4 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Heidelberg Dordrecht London New York |
| Místo konání akce | Taipei, Taiwan |
| Rok konání akce | 2011 |
| Typ akce podle státní příslušnoti účastníků | WRD - Světová |
| Údaje o tomto záznamu o výsledku |
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
| Dodavatel | MSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT) |
| Rok sběru | 2012 |
| Systémové označení dodávky dat | RIV12-MSM-14330___/01:1 |
| Specifikace | RIV/00216224:14330/11:00049982!RIV12-MSM-14330___ |
| Kontrolní kód | [2D6B5002C905] |
| Další výskyty tohoto výsledku od stejného předkladatele |
| Dodáno GA ČR v roce 2012 | Záznam s identifikačním kódem RIV/00216224:14330/11:00049982 v dodávce dat RIV12-GA0-14330___/02:1 |
| Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl |
| Projekt | GAP202/11/0312 - Vývoj a verifikace softwarových komponent v zapouzdřených systémech (2011-2013, GA0/GA) |
| Projekt | GD102/09/H042 - Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů (2009-2012, GA0/GD) |
| Výzkumný záměr | MSM0021622419 - Vysoce paralelní a distribuované výpočetní systémy (2005-2011, MSM) |
| S - Specifický výzkum na vysokých školách |