Hennessy-Milner Logic with Greatest Fixed Points as a Complete
Behavioural Specification Theory

D 2013

Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory

BENEŠ, Nikola, Benoit DELAHAYE, Uli FAHRENBERG, Jan KŘETÍNSKÝ, Axel LEGAY et. al.

Basic information

Original name

Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory

Authors

BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Benoit DELAHAYE (250 France), Uli FAHRENBERG (276 Germany), Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution) and Axel LEGAY (56 Belgium)

Edition

Heidelberg Dordrecht London New York, CONCUR 2013 - Concurrency Theory - 24th International Conference, p. 76-90, 15 pp. 2013

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/13:00066201

Organization unit

Faculty of Informatics

ISBN

978-3-642-40183-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-40184-8_7

Keywords in English

modal transition systems; composition; specification; interface theory

Abstract

V originále

There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of Hennessy-Milner logic with greatest fixed points and the behavioural formalism of disjunctive modal transition systems. We also introduce a new operation of quotient for the above equivalent formalisms, which is adjoint to structural composition and allows synthesis of missing specifications from partial implementations. This is a~substantial generalisation of the quotient for deterministic modal transition systems defined in earlier papers.

Links

GAP202/10/1469, research and development project

Name: Formální metody pro analýzu a verifikaci komplexních systémů

Investor: Czech Science Foundation

GAP202/11/0312, research and development project

Name: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)

Investor: Czech Science Foundation

MUNI/A/0739/2012, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

MUNI/A/0760/2012, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)

Investor: Masaryk University, Category A

Citovat

BENEŠ, Nikola, Benoit DELAHAYE, Uli FAHRENBERG, Jan KŘETÍNSKÝ and Axel LEGAY. Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. In CONCUR 2013 - Concurrency Theory - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2013, p. 76-90. ISBN 978-3-642-40183-1. Available from: https://dx.doi.org/10.1007/978-3-642-40184-8_7.

@inproceedings{1112166,
   author = {Beneš, Nikola and Delahaye, Benoit and Fahrenberg, Uli and Křetínský, Jan and Legay, Axel},
   address = {Heidelberg Dordrecht London New York},
   booktitle = {CONCUR 2013 - Concurrency Theory - 24th International Conference},
   doi = {http://dx.doi.org/10.1007/978-3-642-40184-8_7},
   keywords = {modal transition systems; composition; specification; interface theory},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Heidelberg Dordrecht London New York},
   isbn = {978-3-642-40183-1},
   pages = {76-90},
   publisher = {Springer},
   title = {Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory},
   year = {2013}
}

TY  - JOUR
ID  - 1112166
AU  - Beneš, Nikola - Delahaye, Benoit - Fahrenberg, Uli - Křetínský, Jan - Legay, Axel
PY  - 2013
TI  - Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory
PB  - Springer
CY  - Heidelberg Dordrecht London New York
SN  - 9783642401831
KW  - modal transition systems
KW  - composition
KW  - specification
KW  - interface theory
N2  - There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of Hennessy-Milner logic with greatest fixed points and the behavioural formalism of disjunctive modal transition systems. We also introduce a new operation of quotient for the above equivalent formalisms, which is adjoint to structural composition and allows synthesis of missing specifications from partial implementations. This is a~substantial generalisation of the quotient for deterministic modal transition systems defined in earlier papers.
ER  -

BENEŠ, Nikola, Benoit DELAHAYE, Uli FAHRENBERG, Jan KŘETÍNSKÝ and Axel LEGAY. Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. In \textit{CONCUR 2013 - Concurrency Theory - 24th International Conference}. Heidelberg Dordrecht London New York: Springer, 2013, p.~76-90. ISBN~978-3-642-40183-1. Available from: https://dx.doi.org/10.1007/978-3-642-40184-8\_{}7.

Detailed Information on Publication Record