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

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

51 Citationer (Scopus)

489 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.

Originalsprog	Engelsk
Titel	CONCUR 2007 – Concurrency Theory
Antal sider	15
Forlag	IEEE Computer Society Press
Publikationsdato	2007
Sider	105-119
ISBN (Trykt)	978-3-540-74406-1
DOI	https://doi.org/10.1007/978-3-540-74407-8_8
Status	Udgivet - 2007
Begivenhed	CONCUR 2007 - Lisabon, Portugal Varighed: 3 sep. 2007 → 8 sep. 2007 Konferencens nummer: 18

Konference

Konference	CONCUR 2007
Nummer	18
Land/Område	Portugal
By	Lisabon
Periode	03/09/2007 → 08/09/2007

Navn	Lecture Notes in Computer Science
Nummer	4703
ISSN	0302-9743

Adgang til dokumentet

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

CONCUR2007withappendixForlagets udgivne version, 260 KB

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Citationsformater

@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

Konference

Adgang til dokumentet

AUB Link

Fingeraftryk

Citationsformater