| Identifikační kód | RIV/00216224:14330/13:00066201 |
|---|
| Název v anglickém jazyce | Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2013 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 2 |
|---|
| Počet tvůrců celkem | 5 |
|---|
| Počet domácích tvůrců | 2 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Nikola Beneš (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2050587)
Benoit Delahaye (státní příslušnost: FR - Francouzská republika)
Uli Fahrenberg (státní příslušnost: DE - Spolková republika Německo)
Jan Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3503054)
Axel Legay (státní příslušnost: BE - Belgické království) |
|---|
| Popis výsledku v anglické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. |
|---|
| Klíčová slova oddělená středníkem | modal transition systems; composition; specification; interface theory |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-642-40184-8_7 |
|---|