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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066201" target="_blank" >RIV/00216224:14330/13:00066201 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-40184-8_7" target="_blank" >http://dx.doi.org/10.1007/978-3-642-40184-8_7</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-40184-8_7" target="_blank" >10.1007/978-3-642-40184-8_7</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2013

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

CONCUR 2013 - Concurrency Theory - 24th International Conference

ISBN

9783642401831

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

76-90

Název nakladatele

Springer

Místo vydání

Heidelberg Dordrecht London New York

Místo konání akce

Heidelberg Dordrecht London New York

Datum konání akce

1. 1. 2013

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—