Modal Transition Systems: Composition and LTL Model Checking

BENEŠ, Nikola; Ivana ČERNÁ a Jan KŘETÍNSKÝ. Modal Transition Systems: Composition and LTL Model Checking. In ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium. Heidelberg Dordrecht London New York: Springer, 2011, s. 228-242. ISBN 978-3-642-24371-4.

Základní údaje

Originální název

Modal Transition Systems: Composition and LTL Model Checking

Autoři

BENEŠ, Nikola; Ivana ČERNÁ ORCID a Jan KŘETÍNSKÝ

Vydání

Heidelberg Dordrecht London New York, ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium, od s. 228-242, 15 s. 2011

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Kód RIV

RIV/00216224:14330/11:00049982

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-24371-4

UT WoS

000306498800017

Klíčová slova anglicky

modal transition systems; model checking; refinement; conjunction

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.

---

Návaznosti

GAP202/11/0312, projekt VaV	Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems) Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
GD102/09/H042, projekt VaV	Název: 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ů Investor: Grantová agentura ČR, 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ů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
MUNI/A/0914/2009, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Přiložené soubory

paper_51-1_hqkmdxut.pdf

paper_51-1.pdf

Požádat o autorskou verzi souboru

ATVA11-mts-ltl.pdf

Požádat o autorskou verzi souboru