Multi-valued Logic for Static Analysis and Model Checking

Abstract

We extend Alternation-Free Least Fixed Point Logic to be based on Belnap logic, while maintaining the close correspondence between static analysis and model checking pioneered by Bernhard Steffen, and opening up for handling access control policies central to the construction of secure IT systems.

Appendices

A Proofs of Key Facts

Proof of Fact 1. There is an easy graphical proof of the interesting cases. First observe that the Hasse diagram for $\Rightarrow$ in Fig. 1 is obtained from the Hasse diagram for $\leadsto$ by rotating it 90$^\circ$ clockwise. Next observe that in the Hasse diagram for $\Rightarrow$ the operator $\otimes$ ‘moves to the left’ whereas the operator $\oplus$ ‘moves to the right’. Similarly observe that the Hasse diagram for $\leadsto$ in Fig. 1 is obtained from the Hasse diagram for $\Rightarrow$ by rotating it 90$^\circ$ anti-clockwise. Next observe that in the Hasse diagram for $\leadsto$ the operator $\wedge$ ‘moves to the right’ whereas the operator $\vee$ ‘moves to the left’.

Proof of Fact 3. The interesting cases are when $op_i\in \{\otimes ,\oplus \}$ and $op_{3-i}\in \{\wedge ,\vee \}$ (for $i\in \{1,2\}$) as the other cases follow since $(\mathsf{Four},\leadsto )$ and $(\mathsf{Four},\Rightarrow )$ are distributive lattices. It is straightforward to validate the remaining eight interesting cases.

Proof of Fact 4. There is an easy graphical proof of these laws. For the first two we observe that negation ($\lnot$) is also the dualisation operator on $(\mathsf{Four},\Rightarrow )$ where $\wedge$ is greatest lower bound and $\vee$ is least upper bound. For the next two observe that negation ($\lnot$) works ‘sideways’ on $(\mathsf{Four},\leadsto )$. The remaining four laws are analogous.

Proof of Fact 7. We first show the equation $(f_1 > f_2) = f_1\oplus (f_2\otimes {\sim }(f_1\oplus (\lnot f_1)))$ by considering two cases for the value of $f_1$. If $f_1=\bot$ we note that $(f_1\oplus (\lnot f_1))=\bot$ and hence that $f_1\oplus (f_2\otimes {\sim }(f_1\oplus (\lnot f_1))) = \bot \oplus (f_2 \otimes \top ) = f_2$ as desired. If $f_1\ne \bot$ we note that $(f_1\oplus (\lnot f_1))=\top$ and hence that $f_1\oplus (f_2\otimes {\sim }(f_1\oplus (\lnot f_1))) = f_1\oplus (f_2 \otimes \bot ) = f_1$ as desired.

For the general result, it follows from [1, Proposition 17] that all multi-argument functions over Four are expressible in terms of $\lnot$, $\oplus$, $\bot$ and $\supset$ defined by

$$ (f_1 \supset f_2) = \left\{ \begin{array}{ll} f_2&{}\hbox {if }\mathsf{t}\leadsto f_1 \\ \mathsf{t}&{}\hbox {otherwise} \end{array}\right. $$

Define $S[f] = (f\wedge \top )\otimes (\lnot (f\wedge \top ))$ and note that

$$ S[f] = \left\{ \begin{array}{ll} \top &{}\hbox {if }\mathsf{t}\leadsto f \\ \bot &{}\hbox {otherwise} \end{array}\right. = \left\{ \begin{array}{ll} \top &{}\hbox {if } f\in \{\mathsf{t},\top \} \\ \bot &{}\hbox {if } f\in \{\mathsf{f},\bot \} \end{array}\right. $$

so that is suffices to verify that $(f_1 \supset f_2) = (f_2\otimes ( S[f_1] ))\oplus ( \mathsf{t}\otimes ( {\sim }S[f_1] ))$.

B Least Fixed Point CTL Suffices for CTL

We need to show that the following CTL operators can be defined using the least fixed point fragment of CTL: $\mathbf A [\phi _{1} \mathbf U \phi _{2}]$, $\mathbf{EF }\phi$, $\mathbf{AG }\phi$ and $\mathbf{EG }\phi$. This is standard in the two-valued setting but also holds in our setting as expressed by the following facts (where we dispense with the proofs). We begin with two facts on path formulas.

Fact 8

For any M and $\pi$, $[(M,\pi ) \models ^{} \mathbf F \phi ]=[(M,\pi ) \models ^{} \mathbf{true }{} \mathbf U \phi ]$.

Fact 9

For any M and $\pi$, $[(M,\pi ) \models ^{} \mathbf G \phi ]=\lnot [(M,\pi ) \models ^{} \mathbf F \lnot \phi ]$.

We continue with four facts on state formulas. (One may check that we have the equivalence $\mathbf{AX }\phi \equiv \lnot \mathbf{EX }\lnot \phi$ but the explicit presence of $\mathbf{AX }$ in least fixed point CTL is helpful for our development.)

Fact 10

The equivalence $\mathbf{EF }\phi \equiv \mathbf E [\mathbf{true }{} \mathbf U \phi ]$ holds in three-valued CTL.

Fact 11

The equivalence $\mathbf{EG }\phi \equiv \lnot \mathbf{AF }\lnot \phi$ holds in three-valued CTL.

Fact 12

The equivalence $\mathbf{AG }\phi \equiv \lnot \mathbf{EF }\lnot \phi$ holds in three-valued CTL.

Fact 13

The equivalence $\mathbf A [\phi _{1}{} \mathbf U \phi _{2}]\equiv \lnot \mathbf E [\lnot \phi _{2}{} \mathbf U (\lnot \phi _{1}\wedge \lnot \phi _{2})]\wedge \mathbf{AF }\phi _{2}$ holds in three-valued CTL.