On the construction of multi-valued concurrent dynamic logic

TL;DR

This paper introduces a novel multi-valued concurrent dynamic logic framework that incorporates uncertainty and weights into parallel program reasoning, extending traditional dynamic logic with fuzzy and multi-valued features.

Contribution

It combines concurrent dynamic logic with multi-valued propositional logic to handle weighted, uncertain parallel computations, creating a new family of logics called CGDL(A).

Findings

Defined a new multi-valued concurrent propositional dynamic logic framework.

Analyzed the validity of axioms from classical CPDL within the new logic.

Established a parametric family of logics based on an action lattice A.

Abstract

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.