TY - JOUR
T1 - EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems
AU - Beneš, Nikola
AU - Křetínský, Jan
AU - Larsen, Kim Guldstrand
AU - Srba, Jiri
PY - 2012
Y1 - 2012
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 and deterministic.
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 and deterministic.
KW - modal transition systems, complexity, refinement
UR - http://www.scopus.com/inward/record.url?scp=84865530103&partnerID=8YFLogxK
U2 - 10.1016/j.ic.2012.08.001
DO - 10.1016/j.ic.2012.08.001
M3 - Journal article
SN - 0890-5401
VL - 218
SP - 54
EP - 68
JO - Information and Computation
JF - Information and Computation
IS - 1
ER -