Skip to Main content Skip to Navigation
Conference papers

Observational Semantics for Dynamic Logic with Binders

Abstract : 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 $$.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Hal Ifip <>
Submitted on : Monday, April 16, 2018 - 11:35:00 AM
Last modification on : Monday, May 18, 2020 - 5:14:11 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Rolf Hennicker, Alexandre Madeira. Observational Semantics for Dynamic Logic with Binders. 23th International Workshop on Algebraic Development Techniques (WADT), Sep 2016, Gregynog, United Kingdom. pp.135-152, ⟨10.1007/978-3-319-72044-9_10⟩. ⟨hal-01767472⟩



Record views


Files downloads