Refinement checking on parametric modal transition systems (2015)výskyt výsledku
| Identifikační kód | RIV/00216224:14330/15:00080734 |
|---|---|
| Název v anglickém jazyce | Refinement checking on parametric modal transition systems |
| Druh | J - Článek v odborném periodiku |
| Jazyk | eng - angličtina |
| Obor - skupina | I - Informatika |
| Obor | IN - Informatika |
| Rok uplatnění | 2015 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku | 2 |
| Počet tvůrců celkem | 6 |
| Počet domácích tvůrců | 3 |
| Výčet všech uvedených jednotlivých tvůrců | Nikola Beneš (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2050587) Jan Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3503054) Kim G. Larsen (státní příslušnost: DK - Dánské království) Mikael H. Moller (státní příslušnost: DK - Dánské království) Salomon Sickert (státní příslušnost: DE - Spolková republika Německo) Jiří Srba (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2753057) |
| Popis výsledku v anglickém jazyce | Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many ofthe limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. |
| Klíčová slova oddělená středníkem | modal transition systems; refinement; specification; logic |
| Stránka www, na které se nachází výsledek | - |
| DOI výsledku | 10.1007/s00236-015-0215-4 |
Údaje o výsledku v závislosti na druhu výsledku
| Název periodika | Acta Informatica |
|---|---|
| ISSN | 0001-5903 |
| Svazek periodika | 52 |
| Číslo periodika v rámci uvedeného svazku | 2-3 |
| Stát vydavatele periodika | DE - Spolková republika Německo |
| Počet stran výsledku | 29 |
| Strana od-do | 269-297 |
| Kód UT WoS článku podle Web of Science | 000351160200008 |
| EID výsledku v databázi Scopus | - |
Ostatní informace 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 | 2016 |
| Specifikace | RIV/00216224:14330/15:00080734!RIV16-MSM-14330___ |
| Datum poslední aktualizace výsledku | 24.05.2016 |
| Kontrolní číslo | 191635722 |
Informace o dalších výskytech výsledku dodaného stejným předkladatelem
| Dodáno GA ČR v roce 2016 | RIV/00216224:14330/15:00080734 v dodávce dat RIV16-GA0-14330___/01:1 |
|---|
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
| Projekt podporovaný MŠMT v programu EE | EE2.3.30.0009 - Zaměstnáním čerstvých absolventů doktorského studia k vědecké excelenci (2012 - 2015) |
|---|---|
| Projekt podporovaný GA ČR v programu GB | GBP202/12/G061 - Centrum excelence - Institut teoretické informatiky (CE-ITI) (2012 - 2018) |
| Podpora / návaznosti | Specifický výzkum na vysokých školách, poskytovatel MŠMT |