TY - GEN
T1 - Checking thorough refinement on modal transition systems is exptime-complete
AU - Beneš, Nikola
AU - Křetínský, Jan
AU - Larsen, Kim G.
AU - Srba, Jiří
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70349319950&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-03466-4_7
DO - 10.1007/978-3-642-03466-4_7
M3 - Conference contribution
AN - SCOPUS:70349319950
SN - 3642034659
SN - 9783642034657
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 112
EP - 126
BT - Theoretical Aspects of Computing - ICTAC 2009 - 6th International Colloquium, Proceedings
T2 - 6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009
Y2 - 16 August 2009 through 20 August 2009
ER -