Dynamic Logics On-demand?

Alexandre Madeira

December 10, 2019

In the last decades, dynamic logics have been used in differ­ent domains as a suitable formalism to reason about and specify a wide range of systems. On the other hand, logics with many-valued semantics are emerging as an interesting tool to handle devices and scenarios where uncertainty is a prime concern.
In order to combine these two aspects, we introduced in [3] a method for the systematic construction of many–valued dynamic logics. Technically the method is parameterised by an action lattice that defines both the computational paradigm and the truth space (corresponding to the underlying Kleene algebra and residuated lattices, respectively). This parametric principle pushed then other theoretical developments, including the a method to the generation of multi-valued epistemic logic, as reported in [1]. Recently, in [2], e extended the systematic genera­tion of dynamic logics from the propositional to the equational case, in order to capture ‘full-fledged’ imperative programs. The generation pro­cess is parametric on a structure specifying a notion of ‘weight’ assigned to programs.
We overview on this talk this line of research, by raising some lines of future work.


1. Mario R. F. Benevides, Alexandre Madeira, and Manuel A. Martins. A fam­ily of graded epistemic logics. Electr. Notes Theor. Comput. Sci., 338:45–59, 2018. URL: https://doi.org/10.1016/j.entcs.2018.10.004.

2. Leandro Gomes, Alexandre Madeira, Manisha Jain, and Luís Soares Barbosa. On the generation of equational dynamic logics for weighted imperative programs. In Formal Methods and Software Engineering -ICFEM 2019, volume 11852 of Lecture Notes in Computer Science, pages 154–169. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32409-4_10.

3. A. Madeira, R. Neves, and M. A. Martins. An exercise on the generation of many­valued dynamic logics. Journal of Logical and Algebraic Methods in Programming, 1:1–29, 2016. doi:10.1016/j.jlamp.2016.03.004.