Talk "Behavioural and Abstractor Specifications Revisited"

by Rolf Hennicker

Mon, 04 September 2017 at 04:00 pm in Berlin, Germany

Joint work with: Alexandre Madeira, Martin Wirsing

Abstract: In the area of algebraic specification there are two main approaches for defining observational abstraction: abstractor specifications define an abstraction from the standard semantics w.r.t. an observational equivalence relation between algebras, whereas behavioural specifications use a notion of observational satisfaction for the axioms of the specification. 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 talk, 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 another 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.