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

BENEŠ, Nikola, Benoit DELAHAYE, Uli FAHRENBERG, Jan KŘETÍNSKÝ a 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, s. 76-90. ISBN 978-3-642-40183-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-40184-8_7.

Základní údaje

Originální název

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

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Benoit DELAHAYE (250 Francie), Uli FAHRENBERG (276 Německo), Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí) a Axel LEGAY (56 Belgie)

Vydání

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

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/13:00066201

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-40183-1

ISSN

DOI

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

Klíčová slova anglicky

modal transition systems; composition; specification; interface theory

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

---

Návaznosti

GAP202/10/1469, projekt VaV	Název: Formální metody pro analýzu a verifikaci komplexních systémů Investor: Grantová agentura ČR, Formální metody pro analýzu a verifikaci komplexních systémů
GAP202/11/0312, projekt VaV	Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems) Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
MUNI/A/0739/2012, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU) Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0760/2012, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty