Abstract
Modal and mixed transition systems are specification formalisms that allow mixing of
over- and under-approximation. We discuss three fundamental decision problems for
such specifications: whether a set of specifications has a common implementation,
whether a sole specification has an implementation, and whether all implementations of
one specification are implementations of another one. For each of these decision problems
we investigate the worst-case computational complexity for the modal and mixed case.
We show that the first decision problem is EXPTIME-complete for modal as well as for
mixed specifications. We prove that the second decision problem is EXPTIME-complete
for mixed specifications (while it is known to be trivial for modal ones). The third
decision problem is furthermore demonstrated to be EXPTIME-complete for mixed
specifications.
over- and under-approximation. We discuss three fundamental decision problems for
such specifications: whether a set of specifications has a common implementation,
whether a sole specification has an implementation, and whether all implementations of
one specification are implementations of another one. For each of these decision problems
we investigate the worst-case computational complexity for the modal and mixed case.
We show that the first decision problem is EXPTIME-complete for modal as well as for
mixed specifications. We prove that the second decision problem is EXPTIME-complete
for mixed specifications (while it is known to be trivial for modal ones). The third
decision problem is furthermore demonstrated to be EXPTIME-complete for mixed
specifications.
Originalsprog | Engelsk |
---|---|
Tidsskrift | Mathematical Structures in Computer Science |
Vol/bind | 20 |
Udgave nummer | Special Issue 01 |
Sider (fra-til) | 75-103 |
ISSN | 0960-1295 |
DOI | |
Status | Udgivet - feb. 2010 |