Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory
verfasst von : Nikola Beneš, Benoît Delahaye, Uli Fahrenberg, Jan Křetínský, Axel Legay
Erschienen in: CONCUR 2013 – Concurrency Theory
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.