Joint work with Rolf Hennicker (University of Munich) and Michel Bidoit (Ecole Normale Sup351rieure de Cachan).
The properties of a system being "observable" or "fully abstract" (all internal states can be distinguished by an external observer) and of being "reachable" (all internal states are relevant, i.e., can be reached by some input) are dual to each other.
This duality - discovered by Arbib and Manes in the 70s in the context of automata theory - now makes a reappearance in the field of algebraic specifications.
The presentation will consist of 3 parts:
We give a survey of the basic ideas of specifying algebraically a state-based system from the point of view of an external observer. A formalisation of this approach using (co)algebras is given.
We review the notion of a reachable algebra. An informal comparison to the observational specifications in 1) will suggest a generalisation of the standard concept of a reachable algebra.
We show that dualising the (co)algebraic formalisation in 1) describes the (generalised) notion of reachability in 2).