| Identifikační kód | RIV/00216224:14330/11:00049982 |
|---|
| Název v anglickém jazyce | Modal Transition Systems: Composition and LTL Model Checking |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2011 |
|---|
| 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 | 3 |
|---|
| 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)
Ivana Černá (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2361132)
Jan Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3503054) |
|---|
| Popis výsledku v anglické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 inthe 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 oddělená středníkem | modal transition systems; model checking; refinement; conjunction |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|