On the Generation of Equational Dynamic Logics for Weighted Imperative Programs

  • Leandro GomesEmail author
  • Alexandre Madeira
  • Manisha Jain
  • Luis S. Barbosa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)


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.


  1. 1.
    Baltag, A., Smets, S.: The dynamic turn in quantum logic. Synthese 186(3), 753–773 (2012). Scholar
  2. 2.
    Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979). Scholar
  3. 3.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)CrossRefGoogle Scholar
  4. 4.
    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). Scholar
  5. 5.
    Jain, M., Madeira, A., Martins, M.A.: A fuzzy modal logic for fuzzy transition systems. Electr. Notes Theor. Comput. Sci. (in print)Google Scholar
  6. 6.
    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). Scholar
  7. 7.
    Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162–178 (1985). Scholar
  8. 8.
    Kozen, D.: The Design and Analysis of Algorithms. Springer, New York (1992). Scholar
  9. 9.
    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). Scholar
  10. 10.
    Peleg, D.: Concurrent dynamic logic. J. ACM 34(2), 450–479 (1987). Scholar
  11. 11.
    Platzer, A.: Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Leandro Gomes
    • 1
    Email author
  • Alexandre Madeira
    • 1
    • 2
  • Manisha Jain
    • 2
  • Luis S. Barbosa
    • 1
    • 3
  1. 1.HASLab INESC TEC - Univ. MinhoBragaPortugal
  2. 2.CIDMA - Univ. AveiroAveiroPortugal
  3. 3.QuantaLab, INLBragaPortugal

Personalised recommendations