| BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN and Jiří SRBA. Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete. In Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings. Heidelberg: Springer-Verlag, 2009, p. 112-126. ISBN 978-3-642-03465-7. Available from: https://dx.doi.org/10.1007/978-3-642-03466-4_7. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{833644,
author = {Beneš, Nikola and Křetínský, Jan and Larsen, Kim G. and Srba, Jiří},
address = {Heidelberg},
booktitle = {Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings},
doi = {http://dx.doi.org/10.1007/978-3-642-03466-4_7},
keywords = {compositional verification; modal transition systems; refinement},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Heidelberg},
isbn = {978-3-642-03465-7},
pages = {112-126},
publisher = {Springer-Verlag},
title = {Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete},
year = {2009}
}
TY - JOUR
ID - 833644
AU - Beneš, Nikola - Křetínský, Jan - Larsen, Kim G. - Srba, Jiří
PY - 2009
TI - Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
PB - Springer-Verlag
CY - Heidelberg
SN - 9783642034657
KW - compositional verification
KW - modal transition systems
KW - refinement
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 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.
ER -
BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN and Jiří SRBA. Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete. In \textit{Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings}. Heidelberg: Springer-Verlag, 2009, p.~112-126. ISBN~978-3-642-03465-7. Available from: https://dx.doi.org/10.1007/978-3-642-03466-4\_{}7.
|
