Alexandre Madeira
CIDMA-UA
December 10, 2019
In the last decades, dynamic logics have been used in different 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 manyvalued 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 generation of dynamic logics from the propositional to the equational case, in order to capture full-fledged imperative programs. The generation process 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.
References
1. Mario R. F. Benevides, Alexandre Madeira, and Manuel A. Martins. A family of graded epistemic logics. Electr. Notes Theor. Comput. Sci., 338:4559, 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 154169. 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 manyvalued dynamic logics. Journal of Logical and Algebraic Methods in Programming, 1:129, 2016. doi:10.1016/j.jlamp.2016.03.004.