On Modal Refinement and Consistency

Ulrik Nyman; Kim Guldstrand Larsen; Andrzej Wasowski

doi:10.1007/978-3-540-74407-8_8

On Modal Refinement and Consistency

Ulrik Nyman, Kim Guldstrand Larsen, Andrzej Wasowski

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

51 Citations (Scopus)

486 Downloads (Pure)

Abstract

Almost 20 years after the original conception, we revisit several fundamental question about modal transition systems. First, we demonstrate the incompleteness of the standard modal refinement using a counterexample due to Hüttel. Deciding any refinement, complete with respect to the standard notions of implementation, is shown to be computationally hard (co-NP hard). Second, we consider four forms of consistency (existence of implementations)
for modal specifications. We characterize each operationally, giving algorithms for deciding, and for synthesizing
implementations, together with their complexities.

Original language	English
Title of host publication	CONCUR 2007 – Concurrency Theory
Number of pages	15
Publisher	IEEE Computer Society Press
Publication date	2007
Pages	105-119
ISBN (Print)	978-3-540-74406-1
DOIs	https://doi.org/10.1007/978-3-540-74407-8_8
Publication status	Published - 2007
Event	CONCUR 2007 - Lisabon, Portugal Duration: 3 Sept 2007 → 8 Sept 2007 Conference number: 18

Conference

Conference	CONCUR 2007
Number	18
Country/Territory	Portugal
City	Lisabon
Period	03/09/2007 → 08/09/2007

Series	Lecture Notes in Computer Science
Number	4703
ISSN	0302-9743

Keywords

Consistency
Refinement
Modal Transition Systems
automata theory
behavioural equivalences

Access to Document

10.1007/978-3-540-74407-8_8

CONCUR2007withappendixFinal published version, 260 KB

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@inproceedings{6e1eabb0198911dca5a4000ea68e967b,

title = "On Modal Refinement and Consistency",

abstract = "Almost 20 years after the original conception, we revisit several fundamental question about modal transition systems. First, we demonstrate the incompleteness of the standard modal refinement using a counterexample due to H{\"u}ttel. Deciding any refinement, complete with respect to the standard notions of implementation, is shown to be computationally hard (co-NP hard). Second, we consider four forms of consistency (existence of implementations)for modal specifications. We characterize each operationally, giving algorithms for deciding, and for synthesizingimplementations, together with their complexities.",

keywords = "Consistency, Refinement, Modal Transition Systems, automata theory, behavioural equivalences",

author = "Ulrik Nyman and Larsen, {Kim Guldstrand} and Andrzej Wasowski",

year = "2007",

doi = "10.1007/978-3-540-74407-8_8",

language = "English",

isbn = "978-3-540-74406-1",

series = "Lecture Notes in Computer Science",

publisher = "IEEE Computer Society Press",

number = "4703",

pages = "105--119",

booktitle = "CONCUR 2007 – Concurrency Theory",

address = "United States",

note = "CONCUR 2007 ; Conference date: 03-09-2007 Through 08-09-2007",

}

TY - GEN

T1 - On Modal Refinement and Consistency

AU - Nyman, Ulrik

AU - Larsen, Kim Guldstrand

AU - Wasowski, Andrzej

N1 - Conference code: 18

PY - 2007

Y1 - 2007

N2 - Almost 20 years after the original conception, we revisit several fundamental question about modal transition systems. First, we demonstrate the incompleteness of the standard modal refinement using a counterexample due to Hüttel. Deciding any refinement, complete with respect to the standard notions of implementation, is shown to be computationally hard (co-NP hard). Second, we consider four forms of consistency (existence of implementations)for modal specifications. We characterize each operationally, giving algorithms for deciding, and for synthesizingimplementations, together with their complexities.

AB - Almost 20 years after the original conception, we revisit several fundamental question about modal transition systems. First, we demonstrate the incompleteness of the standard modal refinement using a counterexample due to Hüttel. Deciding any refinement, complete with respect to the standard notions of implementation, is shown to be computationally hard (co-NP hard). Second, we consider four forms of consistency (existence of implementations)for modal specifications. We characterize each operationally, giving algorithms for deciding, and for synthesizingimplementations, together with their complexities.

KW - Consistency

KW - Refinement

KW - Modal Transition Systems

KW - automata theory

KW - behavioural equivalences

U2 - 10.1007/978-3-540-74407-8_8

DO - 10.1007/978-3-540-74407-8_8

M3 - Article in proceeding

SN - 978-3-540-74406-1

T3 - Lecture Notes in Computer Science

SP - 105

EP - 119

BT - CONCUR 2007 – Concurrency Theory

PB - IEEE Computer Society Press

T2 - CONCUR 2007

Y2 - 3 September 2007 through 8 September 2007

ER -

On Modal Refinement and Consistency

Abstract

Conference

Keywords

Access to Document

AUB Link

Fingerprint

Cite this