On Interval Dynamic Logic

Abstract

The wide number of languages and programming paradigms, as well as the heterogeneity of ‘programs’ and ‘executions’ require new generalisations of propositional dynamic logic. The dynamisation method, introduced in [20], contributed on this direction with a systematic parametric way to construct Many-valued Dynamic Logics able to handle systems where the uncertainty is a prime concern. The instantiation of this method with the Lukasiewicz arithmetic lattice over [0, 1], that we derive here, supports a general setting to design and to (fuzzy-) reason about systems with uncertainty degrees in their transitions. For the verification of real systems, however, there are no de facto methods to accommodate exact truth degrees or weights. Instead, the traditional approach within scientific community is to use different kinds of approximation techniques. Following this line, the current paper presents a framework where the representation values are given by means of intervals. Technically this is achieved by considering an ‘interval version’ of the Kleene algebra based on the [0, 1] Lukasiewicz lattice. We also discuss the ‘intervalisation’ of L action lattice (in the lines reported in [28]) and how this class of algebras behaves as an (interval) semantics of many-valued dynamic logic. © Springer International Publishing AG 2016.