Technical Reports
The report FIMU-RS-2009-03
Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
by
Nikola Beneš,
Jan Křetínský,
Kim Guldstrand Larsen,
Jiří Srba,
A full version of the paper presented at conference ICTAC 2009. July 2009, 28 pages.
FIMU-RS-2009-03.
Available as Postscript,
PDF.
Abstract:
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.
