New interface

# 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
Domain :

Cited literature [12 references]

https://hal.inria.fr/hal-01767472
Contributor : Hal Ifip Connect in order to contact the contributor
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)

### 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⟩

Record views