Modal and Mixed Specifications: Key Decision Problems and their Complexities

Adam Antonik, Michael Huth, Kim Guldstrand Larsen, Ulrik Mathias Nyman, Andrzej Wasowski

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Abstract

Modal and mixed transition systems are specification formalisms that allow the 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 an individual specification has an implementation; and

— whether all implementations of an individual specification are implementations of another one.

For each of these decision problems we investigate the worst-case computational complexity for the modal and mixed cases. We show that the first decision problem is EXPTIME-complete for both modal and mixed specifications. We prove that the second decision problem is EXPTIME-complete for mixed specifications (it is known to be trivial for modal ones). The third decision problem is also shown to be EXPTIME-complete for mixed specifications.
Original languageEnglish
JournalMathematical Structures in Computer Science
Volume20
Pages (from-to)75-103
ISSN0960-1295
Publication statusPublished - 2010

Keywords

  • Modal Transition Systems
  • Mixed Transition Systems
  • Specification Formalisms
  • EXPTIME-complete
  • Decision Problems

Fingerprint

Dive into the research topics of 'Modal and Mixed Specifications: Key Decision Problems and their Complexities'. Together they form a unique fingerprint.

Cite this