Abstract
Dynamic logic with binders \(\mathcal {D}^{\downarrow }\) has been introduced as an institution for the development of reactive systems based on model class semantics. The satisfaction relation of this logic was, however, not abstract enough to enjoy the modal invariance property (bisimilar models should satisfy the same sentences). We recently overcame this problem by proposing an observational satisfaction relation where the equality on states is interpreted by bisimilarity of states. This entailed, however, a price to pay - the satisfaction condition required for institutions was lost. This paper works on this limitation by establishing a behavioural semantics for \(\mathcal {D}^{\downarrow }\) parametric to behavioural structures - families of equivalence relations on the states of each model. Such structures are taken in consideration in the signature category and, in particular, for the definition of signature morphisms. We show that with these changes we get again an institution with a behavioural model class semantics. The framework is instantiated with specific behavioural structures, resulting in the novel Institution of Crucial Actions.
This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and 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 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.
- 2.
For sake of uniformity, we still use along the section the relational notation to present this function, i.e. we use \((w,w')\in \mathcal {BB}h\) to represent \(\mathcal {BB}h (w)=w'\).
References
Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL: the common algebraic specification language. Theor. Comput. Sci. 286(2), 153–196 (2002)
Barbuti, R., Francesco, N.D., Santone, A., Vaglini, G.: Selective mu-calculus and formula-based equivalence of transition systems. J. Comput. Syst. Sci. 59(3), 537–556 (1999)
Bidoit, M., Hennicker, R.: Constructor-based observational logic. J. Log. Algebr. Program. 67(1–2), 3–51 (2006)
Braüner, T.: Hybrid Logic and Its Proof-Theory. Applied Logic Series. Springer, Dordrecht (2010). doi:10.1007/978-94-007-0002-4
Goguen, J.: Types as theories. In: George Michael Reed, A.W.R., Wachter, R.F., (eds.) Topology and Category Theory in Computer Science (1991)
Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)
Goguen, J.A., Malcolm, G.: A hidden agenda. Theor. Comput. Sci. 245(1), 55–101 (2000)
Goguen, J., Roşu, G.: Hiding more of hidden algebra. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1704–1719. Springer, Heidelberg (1999). doi:10.1007/3-540-48118-4_40
Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Hennicker, R., Bidoit, M.: Observational logic. In: Haeberer, A.M. (ed.) AMAST 1999. LNCS, vol. 1548, pp. 263–277. Springer, Heidelberg (1998). doi:10.1007/3-540-49253-4_20
Hennicker, R., Madeira, A.: Behavioural semantics for the dynamic logic with binders. In: Roggenbach, M. (ed.) Recent Trends in Algebraic Development Methods - Selected Papers of WADT 2016. Springer (2016, to appear)
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). doi:10.1007/978-3-319-46750-4_24
Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)
Misiak, M.: Behavioural semantics of algebraic specifications in arbitrary logical systems. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 144–161. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31959-7_9
Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_40
Tarlecki, A.: Towards heterogeneous specifications. In: Frontiers of Combining Systems (FroCoS 1998). Applied Logic Series, pp. 337–360. Kluwer Academic Publishers (1998)
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 Springer International Publishing AG
About this paper
Cite this paper
Hennicker, R., Madeira, A. (2017). Institutions for Behavioural Dynamic Logic with Binders. In: Hung, D., Kapur, D. (eds) Theoretical Aspects of Computing – ICTAC 2017. ICTAC 2017. Lecture Notes in Computer Science(), vol 10580. Springer, Cham. https://doi.org/10.1007/978-3-319-67729-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-67729-3_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-67728-6
Online ISBN: 978-3-319-67729-3
eBook Packages: Computer ScienceComputer Science (R0)