J 2012

EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems

BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN a Jiří SRBA

Základní údaje

Originální název

EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí), Kim G. LARSEN (208 Dánsko) a Jiří SRBA (203 Česká republika, domácí)

Vydání

Information and Computation, Elsevier, 2012, 0890-5401

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

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

Impakt faktor

Impact factor: 0.699

Kód RIV

RIV/00216224:14330/12:00057563

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000309195100004

Klíčová slova anglicky

modal transition systems; refinement; computational complexity

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 24. 10. 2013 16:17, RNDr. Nikola Beneš, Ph.D.

Anotace

V originále

Modal transition systems (MTS), a specification formalism introduced more than 20 years ago, has recently received a considerable attention in several different areas. Many of the fundamental questions related to MTSs have already been answered. However, the problem of the exact computational complexity of thorough refinement checking between two finite MTSs remained unsolved. We settle down this question by showing EXPTIME-completeness of thorough refinement checking on finite MTSs. The upper-bound result relies on a novel algorithm running in single exponential time providing a direct goal-oriented way to decide thorough refinement. If the right-hand side MTS is moreover deterministic, or has a fixed size, the running time of the algorithm becomes polynomial. The lower-bound proof is achieved by reduction from the acceptance problem of alternating linear bounded automata and the problem remains EXPTIME-hard even if the left-hand side MTS is fixed and deterministic.

Návaznosti

GAP202/10/1469, projekt VaV
Název: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Grantová agentura ČR, Formální metody pro analýzu a verifikaci komplexních systémů
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
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

IC.pdf
Požádat o autorskou verzi souboru