Observational interpretations of hybrid dynamic logic with binders and silent transitions

Abstract

We extend hybrid dynamic logic with binders (for state variables) by distinguishing between observable and silent transitions. This differentiation gives rise to two kinds of observational interpretations: The first one relies on observational abstraction from the ordinary model class of a specification Sp by considering its closure under weak bisimulation. The second one uses an observational satisfaction relation for the axioms of the specification Sp, which relaxes the interpretation of state variables and the satisfaction of modal formulæ by abstracting from silent transitions. We establish a formal relationship between both approaches and show that they are equivalent under mild conditions. For the proof we instantiate the previously introduced concept of a behaviour-abstractor framework to the case of dynamic logic with binders and silent transitions. As a particular outcome we provide an invariance theorem and show the Hennessy-Milner property for weakly bisimilar labelled transition systems and observational satisfaction. In the second part of the paper we integrate our results in a development methodology for reactive systems leading to two versions of observational refinement. We provide conditions under which both kinds of refinement are semantically equivalent, involving implementation constructors for relabelling, hiding, and parallel composition.