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

Nikola Beneš 1 Benoît Delahaye 2 Uli Fahrenberg 3 Jan Křetínský 4 Axel Legay 3
2 AELOS
LINA - Laboratoire d'Informatique de Nantes Atlantique
3 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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.
Type de document :
Communication dans un congrès
Pedro R. D’Argenio; Hernán Melgratti. CONCUR 2013 - 24th International Conference Concurrency Theory, Aug 2013, Buenos Aires, Argentina. Springer, 8052, pp.76 - 90, 2013, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-642-40184-8_7〉
Liste complète des métadonnées

Littérature citée [39 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087914
Contributeur : Uli Fahrenberg <>
Soumis le : jeudi 27 novembre 2014 - 09:35:54
Dernière modification le : mercredi 11 avril 2018 - 01:51:23
Document(s) archivé(s) le : vendredi 14 avril 2017 - 21:55:35

Fichier

concur.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Nikola Beneš, Benoît Delahaye, Uli Fahrenberg, Jan Křetínský, Axel Legay. Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. Pedro R. D’Argenio; Hernán Melgratti. CONCUR 2013 - 24th International Conference Concurrency Theory, Aug 2013, Buenos Aires, Argentina. Springer, 8052, pp.76 - 90, 2013, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-642-40184-8_7〉. 〈hal-01087914〉

Partager

Métriques

Consultations de la notice

720

Téléchargements de fichiers

124