2009
Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN a Jiří SRBAZákladní údaje
Originální název
Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
Název česky
Zevrubné zjemnění na modálních přechodových systémech je EXPTIME-úplný problém
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í
Heidelberg, Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings, od s. 112-126, 15 s. 2009
Nakladatel
Springer-Verlag
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Malajsie
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
tištěná verze "print"
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/09:00065771
Organizační jednotka
Fakulta informatiky
ISBN
978-3-642-03465-7
ISSN
UT WoS
000269931000007
Klíčová slova anglicky
compositional verification; modal transition systems; refinement
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 30. 4. 2014 05:53, RNDr. Pavel Šmerk, Ph.D.
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 and was repeatedly stated as an open problem. 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.
Česky
Modální přechodové systémy (MTS), specifikační formalismus zavedený před více než 20 lety, jsou nyní ve středu zájmů v řadě různých oblastí. Mnoho základních otázek o MTS již bylo zodpovězeno. Nicméně otázka přesné složitosti zevrubného zjemnění mezi dvěma konečnými MTS zůstala otevřená a byla opakována jako otevřený problém. Tuto otázku zodpovídáme důkazem EXPTIME-úplnosti tohoto problému. Horního odhadu je docíleno exponenciálním algoritmem. Navíc pokud je pravá strana deterministická nebo fixovaná, algoritmus se stává polynomiálním. Dolní odhad je dokázán redukcí z problému akceptace alternujícího lineáně ohraničeného automatu a problém zůstává EXPTIME-těžký, i pokud je levá strana fixována.
Návaznosti
| MSM0021622419, záměr |
| ||
| 1ET408050503, projekt VaV |
| ||
| 1M0545, projekt VaV |
|