Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
CONCUR 2013 - Concurrency Theory - 24th International Conference
ISBN
9783642401831
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
76-90
Publisher name
Springer
Place of publication
Heidelberg Dordrecht London New York
Event location
Heidelberg Dordrecht London New York
Event date
Jan 1, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—