On the Generation of Equational Dynamic Logics for Weighted Imperative Programs
Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work  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.
- 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