Institutions for Behavioural Dynamic Logic with Binders

Dynamic logic with binders \(\mathcal {D}^{\downarrow }\) has been introduced as an institution for the development of reactive systems based on model class semantics. The satisfaction relation of this logic was, however, not abstract enough to enjoy the modal invariance property (bisimilar models should satisfy the same sentences). We recently overcame this problem by proposing an observational satisfaction relation where the equality on states is interpreted by bisimilarity of states. This entailed, however, a price to pay - the satisfaction condition required for institutions was lost. This paper works on this limitation by establishing a behavioural semantics for \(\mathcal {D}^{\downarrow }\) parametric to behavioural structures - families of equivalence relations on the states of each model. Such structures are taken in consideration in the signature category and, in particular, for the definition of signature morphisms. We show that with these changes we get again an institution with a behavioural model class semantics. The framework is instantiated with specific behavioural structures, resulting in the novel Institution of Crucial Actions.