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

https://hal.inria.fr/hal-01767472
Contributor : Hal Ifip <>
Submitted on : Monday, April 16, 2018 - 11:35:00 AM
Last modification on : Monday, May 18, 2020 - 5:14:11 PM

File

433330_1_En_10_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

87

Files downloads

188