Advertisement

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)

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.

References

  1. 1.
    Baltag, A., Smets, S.: The dynamic turn in quantum logic. Synthese 186(3), 753–773 (2012).  https://doi.org/10.1007/s11229-011-9915-7MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    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-1MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-030-16722-6_5CrossRefGoogle 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).  https://doi.org/10.1007/978-3-662-46675-9_1CrossRefGoogle Scholar
  7. 7.
    Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162–178 (1985).  https://doi.org/10.1016/0022-0000(85)90012-1MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Kozen, D.: The Design and Analysis of Algorithms. Springer, New York (1992).  https://doi.org/10.1007/978-1-4612-4400-4CrossRefzbMATHGoogle 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).  https://doi.org/10.1016/j.jlamp.2016.03.004MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Peleg, D.: Concurrent dynamic logic. J. ACM 34(2), 450–479 (1987).  https://doi.org/10.1145/23005.23008MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Platzer, A.: Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14509-4CrossRefzbMATHGoogle 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