On Graded Concurrent PDL

Propositional dynamic logic, $\mathsf{PDL}$, has been introduced as a logic of imperative computer programs [5], but it has found many applications in formalizing reasoning about actions in general. Many-valued versions of $\mathsf{PDL}$ aim at formalizing reasoning about action in contexts where imprecise concepts are involved (e.g., [12]). For example, goals may be specified using vague notions, or weights may be attached to actions depending on the amount of resources their execution consumes. The concurrent propositional dynamic logic $\mathsf{CPDL}$ [6, 10] extends $\mathsf{PDL}$ with an operator representing the parallel execution of two actions: $\scalebox{0.9}{{[}}\alpha\cap\beta\scalebox{0.9}{{]}}\varphi$ means that a successful parallel execution of action $\alpha$ and $\beta$ is guaranteed to make $\varphi$ true.

In this paper, we outline a version with many values of $\mathsf{CPDL}$. Our logic is based on propositional dynamic models in which formulas and accessibility relations are evaluated in finite Łukasiewicz chains; therefore, we extend the framework of [12] with the parallel execution operator. Our main technical result is a soundness and completeness theorem for logic.

Let $\Pi$ be a countable set of program variables $\pi_{0},\pi_{1}.\ldots$ which are used to denote the atomic programs. The intrinsic meaning of atomic programs is not examined further. Instead, we concentrate on the complex programs generated by operations on the given ones. Let P be a countable set of propositional variables. Let Ł_n be a finite Łukasiewicz chain. The language $\mathcal{L}_{n}$ for concurrent propositional dynamic logic can be separated into two categories-the set of programs $\Pi_{n}$ and formulas $\Phi_{n}$ defined mutually recursively in Barckus-Naur form as follows:

• •

  $\Pi_{n}$ $\pi\coloneqq\bar{\pi}\;|\;\pi_{0}\cup\pi_{1}\;|\;\pi_{0}\cap\pi_{1}\;|\;\pi_{0};\pi_{1}\;|\;\pi^{*}\;|\;\varphi?$

• •

  $\Phi_{n}$ $\varphi\coloneqq p\;|\;\bar{c}\;|\;\varphi_{0}\vee\varphi_{1}\;|\;\varphi_{0}\wedge\varphi_{1}\;|\;\varphi_{0}\to\varphi_{1}\;|\;[\pi]\varphi\;|\;\langle\pi\rangle\varphi$

where $\bar{\pi}\in\Pi$, $p\in\textbf{P}$ and $c\in$ Ł_n. From [7], we know that two modal operators $[\pi]$ and $\langle\pi\rangle$ are not interdefinable via $\neg$ in concurrent PDL.

The intended meanings for the operations on the programs are as follows.

• •

  $\pi_{0};\pi_{1}$ execute $\pi_{0}$ then $\pi_{1}$,

• •

  $\pi_{0}\cup\pi_{1}$ execute $\pi_{0}$ or $\pi_{1}$ non-deterministically,

• •

  $\pi_{0}\cap\pi_{1}$ execute $\pi_{0}$ and $\pi_{1}$ concurrently,

• •

  $\pi^{*}$ execute $\pi$ for some finite number of times,

• •

  $\varphi?$ test $\varphi$ : if $\varphi$ is true, then continue; otherwise fail.

In the context of concurrency, the results of execution of an initial state $s$ will be a set of states $T$ rather than a single state. Therefore, the accessibility relation on a set $S$ in Kripke semantics of propositional dynamic logic should be generalized to a set of pair $\langle s,T\rangle$, with $s\in S$ and $T\subseteq S$. We then call the graded accessibility relation as a reachable $\textbf{\L}_{n}$-relation. \theorem@notefont

The operations on reachable $\textbf{\L}_{n}$-relation are defined as another reachable $\textbf{\L}_{n}$-relations in the following paragraph. \theorem@notefont

A $\textbf{\L}_{n}$-valuation $\nu$ is any non-modal homomorphism from $\mathcal{L}_{n}$ to $\textbf{\L}_{n}$, i.e. $\nu:\mathcal{L}_{n}\to\textbf{\L}_{n}$ such that $\nu(\bar{c})=c,$ and $\nu(\varphi\star\psi)=\nu(\varphi)\ast\nu(\psi)$ where $\star,\ast\in\{\wedge,\vee,\to\}$ denote the Boolean operations and $\textbf{L}_{n}$-operations respectively. \theorem@notefont

We then introduce the world semantics for concurrent PDL.

Clearly, fixed an $s\in S$, a $M$-interpretation is a $\textbf{\L}_{n}$-valuation. A formula $\varphi$ is called valid in a $\textbf{\L}_{n}$-model $M$ if $\mathcal{I}_{M}(\varphi,s)=1$ for all $s\in S$.

We briefly introduce the definitions and basic properties of finite MV-chains in this section. From more detailed introduction, we refer to the handbooks[4]. \theorem@notefont

The above definition is an abstract formulation. According to Corollary 3.5.4 in [3], any finite MV-chain $\text{\L}_{n}$ is isomorphic to the following more concrete finite MV-chains $\textbf{\L}_{n}$ for any $n\geq 2$.

where $a\odot b\coloneqq max\{0,a+b-1\}$, $a\to b\coloneqq min\{1,1-a+b\}$, and $\sim a\coloneqq 1-a$ for any $a,b\in\{\frac{0}{n-1},\frac{1}{n-1},\ldots,\frac{n-1}{n-1}\}$. Note that $a\vee b\coloneqq(a\to b)\to b(=max\{a,b\})$ and $a\wedge b\coloneqq a\odot(a\to b)(=min\{a,b\})$. The truncated addition $\odot$ is the Łukasiewicz t-norm. In this article, we will use $\textbf{\L}_{n}$ as our definition of finite MV-chain.

For each $n\geq 2$, the axiomatic system $\textbf{P\L}_{n}$ is a Hilbert-style proof system consists the following axiom schemata and rule :

• •

  $\varphi\to(\psi\to\varphi)$,

• •

  $(\varphi\to\psi)\to((\psi\to\chi)\to(\varphi\to\chi))$,

• •

  $((\varphi\to\psi)\to\psi)\to((\psi\to\varphi)\to\varphi)$,

• •

  $(\neg\psi\to\neg\varphi)\to(\varphi\to\psi)$,

• •

  $\overline{c\ast d}\leftrightarrow\bar{c}\star\bar{d}$ where $\star,\ast\in\{\wedge,\vee,\to\}$ denote the boolean operations and $\textbf{L}_{n}$-operations respectively,

• •

  (MP): from $\varphi$ and $\varphi\to\psi$ infer $\psi$.

We give the definition of a formula $\varphi$ being derivable in $\textbf{P\L}_{n}$ from a set of formulas $\Theta$. \theorem@notefont

We use $\Theta\vdash_{\textbf{P\L}_{n}}\varphi$ to denote that $\varphi$ is derivable in $\textbf{P\L}_{n}$ from a set of formulas $\Theta$.

A slight modification of the proof of Proposition 6.4.5 in [4] gives the following theorem. \theorem@notefont

Extend $\textbf{P\L}_{n}$ with axiom schemata and rules for modal formulas, we get another Hilbert-style proof system called $\textbf{D\L}_{n}$. \theorem@notefont

The first four axioms and monotonicity rule are adopted from [13] which characterizes the minimum many-valued bimodal logics over finite residuated lattices. The rest is the standard axiomatization of concurrent PDL [7]. We let $Thm_{n}$ to be the set of theorems of $\textbf{D\L}_{n}$, i.e.

In this section, we introduce the canonical models and filtration technique for connecting finite models and typical models. For $n\in\mathbb{N}$, $\mathcal{F}_{n}=\langle S^{n},\mathcal{I}^{n}\rangle$ consists of the set

and

such that $\mathcal{I}^{n}(\varphi,s)=s(\varphi)$ for all $s\in S^{n}$,

The canonical model in is $\mathcal{M}^{n}_{c}=\langle S^{n},E^{n},V^{n}\rangle$ where $E^{n}(\pi)(s,T)=\mathcal{I}^{n}(\pi,s,T)$ and $V^{n}(p)(s)=s(p)$ \theorem@notefont

The closure of a set $\Gamma$ of formulas is the smallest closed set containing $\Gamma$ as a subset. Also, we write $FL(\varphi)$ as the closure of the set $\{\varphi\}$. Given any $S^{n}$ and $s,t\in S^{n}$, we define a relation $\sim_{\Gamma}$ with respect to a $\Gamma$ as follows :

The equivalence class of $s$ under $\sim_{\Gamma}$ is defined as $|s|_{\Gamma}=\{t\in S^{n}\;|\;s\sim_{\Gamma}t\}$. \theorem@notefont

In this section, we demonstrate that for each $n>1$, the proof system $\textbf{D\L}_{n}$ is sound and complete with respect to the filtraion models. To prove completeness, we need to show that for all $\varphi$ and all $s\in S^{n}$, $\mathcal{I}^{n}(\varphi,s)=\mathcal{I}^{n}_{\Gamma}(\varphi,|s|_{\Gamma})$. To achieve this goal, we define $\Pi_{\Gamma,n}$ as the smallest set of program commands that includes all atomic programs, test occurring in members of $\Gamma$, and is closed under program operations $;,\cup,\cap,$ and $*$. Then we define $\mathcal{I}^{n}_{\Gamma}:\Pi_{\Gamma,n}\times S^{n}_{\Gamma}\times P(S^{n})\cup\Gamma\times S^{n}_{\Gamma}\to\text{\L}_{n}$ as for $\textbf{\L}_{n}$-models. \theorem@notefont

Now, we are ready to the soundness and completeness theorem. \theorem@notefont

We studied many-valued concurrent propositional dynamic logics through relational models where both statisfaction of formulas and accessibility relations are evaluated in finite MV-chains. We provides a sound and weakly complete axiomatization based on extending the framework from many-valued bimodal logics in [13] and classical concurrent PDL in [7]. We believe this research direction lays the groundwork for future investigations.

For the future research directions, let us mention two here. Firstly, the revision and extension of PDL toward modeling concurrency have been studied in various models such as $\pi$-calculus [2], Petri nets [9], and operational semantics [1]. It would be interesting to study the PDL in the setting of concurrency with imprecise concepts. Secondly, in light of [11] to use the finitely weighted Kleene algebra with tests as an algebraic semantic for graded PDL, it is interesting to explore the algebraic framework of graded concurrent PDL. A first step of this goal would be expanding the concurrent Kleene algebras with tests proposed in [8].