BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN a Jiří SRBA. EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems. Information and Computation. Elsevier, 2012, roč. 218, September, s. 54-68. ISSN 0890-5401. Dostupné z: https://dx.doi.org/10.1016/j.ic.2012.08.001. |
Další formáty:
BibTeX
LaTeX
RIS
@article{991084, author = {Beneš, Nikola and Křetínský, Jan and Larsen, Kim G. and Srba, Jiří}, article_number = {September}, doi = {http://dx.doi.org/10.1016/j.ic.2012.08.001}, keywords = {modal transition systems; refinement; computational complexity}, language = {eng}, issn = {0890-5401}, journal = {Information and Computation}, title = {EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems}, volume = {218}, year = {2012} }
TY - JOUR ID - 991084 AU - Beneš, Nikola - Křetínský, Jan - Larsen, Kim G. - Srba, Jiří PY - 2012 TI - EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems JF - Information and Computation VL - 218 IS - September SP - 54-68 EP - 54-68 PB - Elsevier SN - 08905401 KW - modal transition systems KW - refinement KW - computational complexity 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. ER -
BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN a Jiří SRBA. EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems. \textit{Information and Computation}. Elsevier, 2012, roč.~218, September, s.~54-68. ISSN~0890-5401. Dostupné z: https://dx.doi.org/10.1016/j.ic.2012.08.001.
|