Graded Courrent PDL
Chun-Yu Lin
TL;DR
This work extends Propositional Dynamic Logic to a many-valued, concurrent setting by formulating a graded CPDL over finite Łukasiewicz chains $\textbf{L}_n$. It introduces a two-sorted semantics with graded reachability relations and a corresponding Hilbert-style system $\textbf{D\L}_n$, and proves soundness and completeness via canonical models and filtration for all $n>1$. The contributions include a rigorous semantic and proof-theoretic foundation for graded concurrency, the handling of program operators ($;$, $\cup$, $\cap$, $*$) and tests, and a pathway to algebraic semantics and broader concurrency models in future work.
Abstract
Propositional Dynamic Logic, PDL, is a modal logic designed to formalize the reasoning about programs. By extending accessibility between states to states and state sets, concurrent propositional dynamic logic CPDL, is introduced to include concurrent programs due to Peleg and Goldblatt. We study a many-valued generalization of CPDL where the satisfiability and the reachability relation between states and state sets are graded over a finite Łukasiewicz chain. Finitely-valued dynamic logic has been shown to be useful in formalizing reasoning about program behaviors under uncertainty. We obtain completeness results for all finitely valued PDL.