Paper Info
Title
Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
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.
Year
DOI
Venue
2009
10.1007/978-3-642-03466-4_7
Lecture Notes in Computer Science
Keywords
Field
DocType
right-hand side,single exponential time,modal transition,acceptance problem,thorough refinement checking,thorough refinement,considerable attention,novel algorithm,left-hand side,finite mtss,checking thorough refinement,fixed size,goal orientation,upper bound,lower bound
Discrete mathematics,Exponential function,EXPTIME,Polynomial,Computer science,Algorithm,Theoretical computer science,Linear bounded automaton,Formalism (philosophy),Modal,Computational complexity theory,Distributed computing
Conference
Volume
ISSN
Citations 
5684
0302-9743
19
PageRank 
References 
Authors
0.72
22
4
Name
Order
Citations
PageRank
Nikola Beneš19412.24
Jan Křetínský219012.05
Kim G. Larsen33922254.03
Jiří Srba462931.24