Behavioural and abstractor specifications revisited

Hennicker, Rolf; Madeira, Alexandre and Wirsing, Martin (2018): Behavioural and abstractor specifications revisited. In: Theoretical Computer Science, Vol. 741: pp. 32-43

Abstract

In the area of algebraic specification there are two main approaches for defining observational abstraction: behavioural specifications use a notion of observational satisfaction for the axioms of a specification, whereas abstractor specifications define an abstraction from the standard semantics of a specification w.r.t. an observational equivalence relation between algebras. Earlier work by Bidoit, Hennicker, Wirsing has shown that in the case of first-order logic specifications both concepts coincide semantically under mild assumptions. Analogous results have been shown by Sannella and Hofmann for higher-order logic specifications and recently, by Hennicker and Madeira, for specifications of reactive systems using a dynamic logic with binders. In this paper, we bring these results into a common setting: we isolate a small set of characteristic principles to express the behaviour/abstractor equivalence and show that all three mentioned specification frameworks satisfy these principles and therefore their behaviour and abstractor specifications coincide semantically (under mild assumptions). As a new case we consider observational modal logic where observational satisfaction of Hennessy-Milner logic formulae is defined "up to" silent transitions and observational abstraction is defined by weak bisimulation. We show that in this case the behaviour/abstractor equivalence can only be obtained, if we restrict models to weakly deterministic labelled transition systems.

• Item Type: Journal article
• Faculties: Mathematics, Computer Science and Statistics > Computer Science
• Subjects: 000 Computer science, information and general works > 004 Data processing computer science
• ISSN: 0304-3975
• Language: English