Modal Transition Systems: Composition and LTL Model Checking

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BENEŠ Nikola ČERNÁ Ivana KŘETÍNSKÝ Jan

Rok publikování 2011
Druh Článek ve sborníku
Konference ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova modal transition systems; model checking; refinement; conjunction
Přiložené soubory
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.