On the construction of multi-valued concurrent dynamic logic

11/01/2019
by   Leandro Gomes, et al.
0

Dynamic logic is a powerful framework for reasoning about imperative programs. An extension with a concurrent operator [18] was introduced to formalise programs running in parallel. In other direction, other authors proposed a systematic method for generating multi-valued propositional dynamic logics to reason about weighted programs [14]. This paper presents the first step of combining these two frameworks to introduce uncertainty in concurrent computations. In the developed framework, a weight is assigned to each branch of the parallel execution, resulting in a (possible) asymmetric parallelism, inherent to fuzzy programming paradigm [21, 2]. By adopting such an approach, a family of logics is obtained, called multi-valued concurrent propositional dynamic logics (CGDL(A)), parametric on an action lattice A specifying a notion of "weight" assigned to program execution. Additionally, the validity of some axioms of CPDL is discussed in the new family of generated logics.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset