Abstract
Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work [9] on the systematic generation of dynamic logics from the propositional to the equational case, to capture ‘full-fledged’ imperative programs. The generation process is parametric on a structure specifying a notion of ‘weight’ assigned to programs. The paper introduces also a notion of bisimilarity on models of the generated logics, which is shown to entail modal equivalence with respect to the latter.
This work was founded 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 project POCI-01-0145-FEDER-030947. The second author is supported in the scope of the framework contract foreseen in the numbers 4, 5 and 6 of the article 23, of the Decree-Law 57/2016, of August 29, changed by Portuguese Law 57/2017, of July 19 and by UID/MAT/04106/2019 at CIDMA.
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
References
Baltag, A., Smets, S.: The dynamic turn in quantum logic. Synthese 186(3), 753–773 (2012). https://doi.org/10.1007/s11229-011-9915-7
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979). https://doi.org/10.1016/0022-0000(79)90046-1
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Hennicker, R., Madeira, A., Knapp, A.: A hybrid dynamic logic for event/data-based systems. In: Hähnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 79–97. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_5
Jain, M., Madeira, A., Martins, M.A.: A fuzzy modal logic for fuzzy transition systems. Electr. Notes Theor. Comput. Sci. (in print)
Knapp, A., Mossakowski, T., Roggenbach, M., Glauer, M.: An institution for simple UML state machines. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 3–18. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46675-9_1
Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162–178 (1985). https://doi.org/10.1016/0022-0000(85)90012-1
Kozen, D.: The Design and Analysis of Algorithms. Springer, New York (1992). https://doi.org/10.1007/978-1-4612-4400-4
Madeira, A., Neves, R., Martins, M.A.: An exercise on the generation of many-valued dynamic logics. J. Log. Algebr. Methods Program. 1, 1–29 (2016). https://doi.org/10.1016/j.jlamp.2016.03.004
Peleg, D.: Concurrent dynamic logic. J. ACM 34(2), 450–479 (1987). https://doi.org/10.1145/23005.23008
Platzer, A.: Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14509-4
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Gomes, L., Madeira, A., Jain, M., Barbosa, L.S. (2019). On the Generation of Equational Dynamic Logics for Weighted Imperative Programs. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-32409-4_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32408-7
Online ISBN: 978-3-030-32409-4
eBook Packages: Computer ScienceComputer Science (R0)