Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete

Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, Jiri Srba

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

21 Citationer (Scopus)

Abstrakt

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.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind5684
Sider (fra-til)112-126
ISSN0302-9743
DOI
StatusUdgivet - 2009
Begivenhed6th International Colloquium on Theoretical Aspects of Computing (ICTAC'09) - Kuala Lumpur, Malaysia
Varighed: 16 aug. 200920 aug. 2009
Konferencens nummer: 6

Konference

Konference6th International Colloquium on Theoretical Aspects of Computing (ICTAC'09)
Nummer6
LandMalaysia
ByKuala Lumpur
Periode16/08/200920/08/2009

Bibliografisk note

Titel:
Theoretical Aspects of Computing - ICTAC 2009

Oversat titel:


Oversat undertitel:


Forlag:
Springer

ISBN (Trykt):
978-3-642-03465-7

ISBN (Elektronisk):


Publikationsserier:
Lecture Notes in Computer Science, Springer Verlag, 0302-9743, 1611-3349, 5684

Emneord

  • modal transition systems
  • complexity
  • thorough refinement

Citationsformater