The dynamic logic with binders

$$\mathcal {D}^{\downarrow }$$ was recently introduced as a suitable formalism to support a rigorous stepwise development method for reactive software. The commitment of this logic concerning bisimulation equivalence is, however, not satisfactory: the model class semantics of specifications in $$\mathcal {D}^{\downarrow }$$ is not closed under bisimulation equivalence; there are $$\mathcal {D}^{\downarrow }$$ -sentences that distinguish bisimulation equivalent models, i.e., $$\mathcal {D}^{\downarrow }$$ does not enjoy the modal invariance property. This paper improves on these limitations by providing an observational semantics for dynamic logic with binders. This involves the definition of a new model category and of a more relaxed satisfaction relation. We show that the new logic $$\mathcal {D}^{\downarrow }_\sim$$ enjoys modal invariance and even the Hennessy-Milner property. Moreover, the new model category provides a categorical characterisation of bisimulation equivalence by observational isomorphism. Finally, we consider abstractor semantics obtained by closing the model class of a specification $$SP$$ in $$\mathcal {D}^{\downarrow }$$ under bisimulation equivalence. We show that, under mild conditions, abstractor semantics of $$SP$$ in $$\mathcal {D}^{\downarrow }$$ is the same as observational semantics of $$SP$$ in $$\mathcal {D}^{\downarrow }_\sim$$ .