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 \).
A. Madeira—This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within projects POCI-01-0145-FEDER-016692 and UID/MAT/04106/2013 and also with its Operational Programme NORTE 2020, trough the project NORTE-01-0145-FEDER-000037. The second author is also supported by the individual grant SFRH/BPD/103004/2014.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
It exists since bisimulation equivalence is reflexive and it is an equivalence relation on the states of \(\mathcal {M}\).
- 2.
i.e. in any state there are at most finitely many outgoing transitions labelled with the same atomic action.
References
Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)
Bidoit, M., Hennicker, R.: Constructor-based observational logic. J. Log. Algebr. Program. 67(1–2), 3–51 (2006)
Bidoit, M., Hennicker, R., Wirsing, M.: Behavioural and abstractor specifications. Sci. Comput. Program. 25(2–3), 149–186 (1995)
Bräuner, T.: Hybrid Logic and Its Proof-Theory. Applied Logic Series. Springer, Dordrecht (2010). https://doi.org/10.1007/978-94-007-0002-4
Goguen, J.A., Malcolm, G.: A hidden agenda. Theor. Comput. Sci. 245(1), 55–101 (2000)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Madeira, A., Barbosa, L.S., Hennicker, R., Martins, M.A.: Dynamic logic with binders and its application to the development of reactive systems. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 422–440. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_24
Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)
Reichel, H.: Behavioural validity of conditional equations in abstract data types. In: Proceedings of the Vienna Conference on Contributions to General Algebra 3, pp. 301–324. B. G. Teubner Verlag (1985)
Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-17336-3
Acknowledgement
We would like to thank the anonymous reviewers of this paper for their careful reviews with many useful comments and suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 IFIP International Federation for Information Processing
About this paper
Cite this paper
Hennicker, R., Madeira, A. (2017). Observational Semantics for Dynamic Logic with Binders. In: James, P., Roggenbach, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2016. Lecture Notes in Computer Science(), vol 10644. Springer, Cham. https://doi.org/10.1007/978-3-319-72044-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-72044-9_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-72043-2
Online ISBN: 978-3-319-72044-9
eBook Packages: Computer ScienceComputer Science (R0)