The Epistemology of Nondeterminism

Abstract

This paper proposes new semantics for propositional dynamic logic (PDL), replacing the standard relational semantics. Under these new semantics, program execution is represented as fundamentally deterministic (i.e., functional), while nondeterminism emerges as an epistemic relationship between the agent and the system: intuitively, the nondeterministic outcomes of a given process are precisely those that cannot be ruled out in advance. We formalize these notions using topology and the framework of dynamic topological logic (DTL) [1]. We show that DTL can be used to interpret the language of PDL in a manner that captures the intuition above, and moreover that continuous functions in this setting correspond exactly to deterministic processes. We also prove that certain axiomatizations of PDL remain sound and complete with respect to the corresponding classes of dynamic topological models. Finally, we extend the framework to incorporate knowledge using the machinery of subset space logic [2], and show that the topological interpretation of public announcements as given in [3] coincides exactly with a natural interpretation of test programs.

A Proofs and Details

1.1 A.1 Characterizing Continuity

A dynamic topological frame (over $\Pi$) is a tuple $F = (X, \mathcal {T}, \{f_{\pi }\}_{\pi \in \Pi })$ where $(X,\mathcal {T})$ is a topological space and each $f_{\pi }: X \rightarrow X$. In other words, a frame is simply a dynamic topological model without a valuation function. A frame F is said to validate a formula $\varphi$ just in case $\varphi$ is true at every point of every model of the form (F, v).

Proposition 1

The formula scheme $\Circle _{\pi } \Box \varphi \rightarrow \Box \Circle _{\pi } \varphi$ defines the class of dynamic topological frames in which $f_{\pi }$ is continuous: that is, for every dynamic topological frame F, F validates every instance of $\Circle _{\pi } \Box \varphi \rightarrow \Box \Circle _{\pi } \varphi$ iff $f_{\pi }$ is continuous.

Proof

First suppose that M is a dynamic topological model in which $f_{\pi }$ is continuous, and let x be a point in this model satisfying $\Circle _{\pi } \Box \varphi$. Then $f_{\pi }(x) \in int ([\![ \varphi ]\!])$. By continuity, the set $U = f_{\pi }^{-1}( int ([\![ \varphi ]\!]))$ is open. Moreover, it is easy to see that $x \in U$ and $U \subseteq [\![ \Circle _{\pi }\varphi ]\!]$, from which it follows that $x \models \Box \Circle _{\pi } \varphi$.

Conversely, suppose that F is a dynamic topological frame in which $f_{\pi }$ is not continuous. Let U be an open subset of X such that $A = f_{\pi }^{-1}(U)$ is not open, and let ; consider a valuation v such that $v(p) = U$. In the resulting model, since $f_{\pi }(x) \in U = int (U)$, we have $x \models \Circle _{\pi } \Box p$. On the other hand, since by definition $x \notin int (f_{\pi }^{-1}(U))$, we have $x \not \models \Box \Circle _{\pi } p$.    $\square$

1.2 A.2 Model Transformation

Our task in this section is to transform an arbitrary serial PDL model into a dynamic topological model in a truth-preserving manner. The intuition for this transformation is fairly straightforward: in a serial PDL model, each state may be nondeterministically compatible with many possible execution paths corresponding to all the possible ways of successively traversing $R_{\pi }$-edges. In a dynamic topological model, by contrast, all such execution paths must be differentiated by state—roughly speaking, this means we need to create a new state for each possible execution path in the standard model. Then, to preserve the original notion of nondeterminism, we overlay a topological structure that “remembers” which new states originated from the same state in the standard model by rendering them topologically indistinguishable.

Let $M = (X, (R_{\pi })_{\pi \in \Pi }, v)$ be a serial PDL model. Let $\Pi ^{*}$ denote the set of all finite sequences from $\Pi$. A map $\alpha : \Pi ^{*} \rightarrow X$ is called a network (through M ) provided $(\forall \mathbf {\pi } \in \Pi ^{*})(\forall \pi \in \Pi )(\alpha (\mathbf {\pi })R_{\pi }\alpha (\mathbf {\pi }, \pi ))$. In other words, a network $\alpha$ must respect $R_{\pi }$-edges in the sense that it associates with each sequence $(\pi _{1}, \ldots , \pi _{n})$ a path $(x_{1}, \ldots , x_{n+1})$ through X such that, for each i, $x_{i}R_{\pi _{i}}x_{i+1}$.¹² Networks through M constitute the points of the dynamic topological model we are building:

$$ \tilde{X} = \{\alpha \,{:} \, \alpha \text { is a network through } M.\}. $$

The topology we equip $\tilde{X}$ with is particularly simple: for each $x \in X$, let $U_{x} = \{\alpha \in \tilde{X} \,{:} \, \alpha (\emptyset ) = x\}$. Clearly the sets $U_{x}$ partition X and so form a topological basis; let $\mathcal {T}$ be the topology they generate.

Next we define the functions $f_{\pi }: \tilde{X} \rightarrow \tilde{X}$. Intuitively, $\alpha \in \tilde{X}$ is a complete record of what paths will be traversed in the original state space X for every sequence of program executions. Therefore, after executing $\pi$, the updated record $f_{\pi }(\alpha )$ should simply consist in those paths determined by $\alpha$ that start with an execution of $\pi$:

$$ f_{\pi }(\alpha )(\mathbf {\pi }) = \alpha (\pi ,\mathbf {\pi }). $$

Finally, define $\tilde{v}: \textsc {prop} \rightarrow 2^{\tilde{X}}$ by

$$ \tilde{v}(p) = \{\alpha \in \tilde{X} \,{:} \, \alpha (\emptyset ) \in v(p)\}. $$

Let $\tilde{M} = (\tilde{X}, \mathcal {T}, (f_{\pi })_{\pi \in \Pi }, \tilde{v})$.

Proposition 2

For every $\varphi \in \mathcal {L}_{PDL}$, for every $\alpha \in \tilde{X}$, $(\tilde{M},\alpha ) \models \varphi \text { iff } (M,\alpha (\emptyset )) \models \varphi$.

Proof

We proceed by induction on the structure of $\varphi$. The base case when $\varphi = p \in \textsc {prop}$ follows directly from the definition of $\tilde{v}$:

$$\begin{aligned} (\tilde{M},\alpha ) \models p&\text {iff}&\alpha \in \tilde{v}(p)\\&\text {iff}&\alpha (\emptyset ) \in v(p)\\&\text {iff}&(M, \alpha (\emptyset )) \models p. \end{aligned}$$

The inductive steps for the Boolean connectives are straightforward. So suppose inductively that the result holds for $\varphi$; we wish to show it holds for $\langle \pi \rangle \varphi$.

Let $\alpha \in \tilde{X}$ and $x = \alpha (\emptyset )$. By definition, $(\tilde{M},\alpha ) \models \langle \pi \rangle \varphi$ iff $\alpha \in cl (f_{\pi }^{-1}([\![ \varphi ]\!]_{\tilde{M}}))$. Since the topology is generated by a partition, we know that $U_{x}$ is a minimal neighbourhood of $\alpha$, and therefore the preceding condition is equivalent to:

$$ U_{x} \cap f_{\pi }^{-1}([\![ \varphi ]\!]_{\tilde{M}}) \ne \emptyset . $$

This intersection is nonempty just in case there exists an $\alpha ' \in \tilde{X}$ such that $\alpha '(\emptyset ) = x$ and $f_{\pi }(\alpha ') \in [\![ \varphi ]\!]_{\tilde{M}}$. By the induction hypothesis,

$$\begin{aligned} f_{\pi }(\alpha ') \in [\![ \varphi ]\!]_{\tilde{M}}&\text {iff}&(\tilde{M}, f_{\pi }(\alpha ') ) \models \varphi \\&\text {iff}&(M, f_{\pi }(\alpha ')(\emptyset )) \models \varphi \\&\text {iff}&(M, \alpha '(\pi )) \models \varphi . \end{aligned}$$

So to summarize, we have shown that $(\tilde{M},\alpha ) \models \langle \pi \rangle \varphi$ iff there exists an $\alpha ' \in \tilde{X}$ such that $\alpha '(\emptyset ) = x$ and $(M, \alpha '(\pi )) \models \varphi$. Since we know that $\alpha '(\emptyset ) R_{\pi } \alpha '(\pi )$, this is in turn equivalent to $(M,x) \models \langle \pi \rangle \varphi$, which completes the induction.    $\square$

1.3 A.3 Sequencing

Lemma 1

Let $(X, \mathcal {T}, \{f_{\pi }\}_{\pi \in \Pi }, v)$ be a dynamic topological model. If $f_{\pi _{1}}$ is open, then

$$ {\langle \pi _{1};\pi _{2}\rangle \varphi } = [\![ \langle \pi _{1}\rangle \langle \pi _{2}\rangle \varphi ]\!]. $$

Proof

It suffices to show that $[\![ \langle \pi _{1};\pi _{2}\rangle \varphi ]\!] \supseteq [\![ \langle \pi _{1}\rangle \langle \pi _{2}\rangle \varphi ]\!]$. So let

$$ x \in [\![ \langle \pi _{1}\rangle \langle \pi _{2}\rangle \varphi ]\!] = cl(f_{\pi _{1}}^{-1}(cl(f_{\pi _{2}}^{-1}([\![ \varphi ]\!])))); $$

then for every open neighbourhood U containing x, we know that $U \cap f_{\pi _{1}}^{-1}(cl(f_{\pi _{2}}^{-1}([\![ \varphi ]\!]))) \ne \emptyset$. This implies that $f_{\pi _{1}}(U) \cap cl(f_{\pi _{2}}^{-1}([\![ \varphi ]\!])) \ne \emptyset$; since $f_{\pi _{1}}(U)$ is open, it follows that $f_{\pi _{1}}(U) \cap f_{\pi _{2}}^{-1}([\![ \varphi ]\!]) \ne \emptyset$ as well. This then implies that $U \cap f_{\pi _{1}}^{-1}(f_{\pi _{2}}^{-1}([\![ \varphi ]\!])) \ne \emptyset$, and therefore

$$ x \in cl (f_{\pi _{1}}^{-1}(f_{\pi _{2}}^{-1}([\![ \varphi ]\!]))) = [\![ \langle \pi _{1};\pi _{2}\rangle \varphi ]\!], $$

as desired.    $\square$

Say that a dynamic topological model is open if each $f_{\pi }$ is open.

Theorem 3

SPDL$_{0}$ + (Seq) is a sound and complete axiomatization of the language $\mathcal {L}_{PDL}$ with respect to the class of all open dynamic topological models.

Proof

Lemma 1 shows that (Seq) is valid in the class of all open dynamic topological models. For completeness, it suffices to observe that the dynamic topological model $\tilde{M}$ constructed in Appendix A.2 is itself open: indeed, for each basic open $U_{x}$, we have

$$\begin{aligned} f_{\pi }(U_{x})= & {} \{\alpha \in \tilde{X} \,{:} \, xR_{\pi }\alpha (\emptyset )\}\\= & {} \bigcup _{y \in R(x)} U_{y}, \end{aligned}$$

which of course is open.    $\square$

Proposition 3

The formula scheme $\Box \Circle _{\pi } \varphi \rightarrow \Circle _{\pi } \Box \varphi$ defines the class of dynamic topological frames in which $f_{\pi }$ is open: that is, for every dynamic topological frame F, F validates every instance of $\Box \Circle _{\pi } \varphi \rightarrow \Circle _{\pi } \Box \varphi$ iff $f_{\pi }$ is open.

Proof

First suppose that M is a dynamic topological model in which $f_{\pi }$ is open, and let x be a point in this model satisfying $\Box \Circle _{\pi } \varphi$. Then $x \in int (f_{\pi }^{-1}([\![ \varphi ]\!]))$. By openness, the set $V = f( int (f_{\pi }^{-1}([\![ \varphi ]\!])))$ is open. Moreover, it is easy to see that $f_{\pi }(x) \in V$ and $V \subseteq [\![ \varphi ]\!]$, from which it follows that $x \models \Circle _{\pi } \Box \varphi$.

Conversely, suppose that F is a dynamic topological frame in which $f_{\pi }$ is not open. Let U be an open subset of X such that $A = f_{\pi }(U)$ is not open, and let $x \in U$ be such that ; consider a valuation v such that $v(p) = A$. In the resulting model, since $x \in U$ and $f_{\pi }(U) \subseteq [\![ p ]\!]$, we have $x \models \Box \Circle _{\pi } p$. On the other hand, since by definition $f_{\pi }(x) \notin int ([\![ p ]\!])$, we have $x \not \models \Circle _{\pi } \Box p$.    $\square$

1.4 A.4 Dynamic Topological Epistemic Logic

We provide a sound and complete axiomatization of the language $\mathcal {L}_{K,\Box ,{\Circle }}$ with respect to the class of all dynamic topological subset models.

Let $\mathsf {CPL}$ denote the axioms and rules of classical propositional logic, let $\mathsf {S5}_{K}$ denote the $\mathsf {S5}$ axioms and rules for the K modality, and let $\mathsf {S4}_{\Box }$ denote the $\mathsf {S4}$ axioms and rules for the $\Box$ modality (see, e.g., [11]). Let $\mathrm {(KI)}$ denote the axiom scheme $K \varphi \rightarrow \Box \varphi$, and set

$$ \mathsf {EL}_{K,\Box } := \mathsf {CPL} + \mathsf {S5}_{K} + \mathsf {S4}_{\Box } + \mathrm {(KI)}. $$

Theorem 4

([3, Theorem 1]). $\mathsf {EL}_{K,\Box }$ is a sound and complete axiomatization of $\mathcal {L}_{K,\Box }$ with respect to the class of all dynamic topological subset models.

Let $\mathsf {DTEL}$ denote the axiom system $\mathsf {EL}_{K, \Box }$ together with the axiom schemes and rules of inference given in Table 2.

Table 2. Additional axioms and rules of inference for DTEL

Theorem 5

DTEL is a sound and complete axiomatization of $\mathcal {L}_{K,\Box ,{\Circle }}$ with respect to the class of all dynamic topological subset models.

Proof

Soundness of $\mathsf {EL}_{K,\Box }$ follows as in the proof given in [3, Theorem 1], while soundness of the additions presented in Table 2 is easy to check. The presence of $\Circle _{\pi }\top$ in ($\lnot$-PC$_{\pi }$) accounts for the fact that $f_{\pi }$ can be partial (since both $\lnot \Circle _{\pi } \varphi$ and $\lnot \Circle _{\pi } \lnot \varphi$ are true at states where $f_{\pi }$ is undefined), and plays an analogous role in (K-PC$_{\pi }$) and (O$_{\pi }$). Similarly, the usual “necessitation” rule for $\Circle _{\pi }$ is not valid, since even if $\varphi$ is a theorem, $\Circle _{\pi } \varphi$ still fails at states where $f_{\pi }$ is undefined.

Completeness is proved by a canonical model construction. Let X denote the set of all maximal $\mathsf {DTEL}$-consistent subsets of $\mathcal {L}_{K,\Box ,{\Circle }}$. Define a binary relation $\sim$ on X by

$$ x \sim y \; \Leftrightarrow \; (\forall \varphi \in \mathcal {L}_{K,\Box ,{\Circle }})(K \varphi \in x \Leftrightarrow K \varphi \in y). $$

Clearly $\sim$ is an equivalence relation; let [x] denote the equivalence class of x under $\sim$. For each $x \in X$, define

$$ R(x) = \{y \in X \,{:} \, (\forall \varphi \in \mathcal {L}_{K,\Box ,{\Circle }})(\Box \varphi \in x \Rightarrow \varphi \in y)\}. $$

Let $\mathcal {B}= \{R(x) \,{:}\, x \in X\}$, and let $\mathcal {T}$ be the topology generated by $\mathcal {B}$. It is easy to check that $\mathcal {B}$ is a basis for $\mathcal {T}$, and each R(x) is a minimal neighbourhood about x (see, e.g., [16]). Given $x \in X$, define

$$ f_{\pi }(x) = \left\{ \begin{array}{ll} \{\varphi \,{:}\, \Circle _{\pi }\varphi \in x\} &{} \; \text {if } \Circle _{\pi }\top \in x\\ \text {undefined} &{} \; \text {otherwise.} \end{array} \right. $$

Lemma 2

Each $f_{\pi }$ is a partial, open function $X \rightharpoonup X$.

For each $p \in \textsc {prop}$, set $v(p) := \{x \in X \,{:} \, p \in x\}$. Let $\mathcal {X}= (X, \mathcal {T}, \{f_{\pi }\}_{\pi \in \Pi }, v)$. Clearly $\mathcal {X}$ is a dynamic topological subset model.

Lemma 3

(Truth Lemma). For every $\varphi \in \mathcal {L}_{K,\Box ,{\Circle }}$, for all $x \in X$, $\varphi \in x$ iff $(\mathcal {X}, x, [x]) \models \varphi$.

Completeness is an easy consequence: if $\varphi$ is not a theorem of DTEL, then $\{\lnot \varphi \}$ is consistent and so can be extended by Lindenbaum’s lemma to some $x \in X$; by Lemma 3, we have $(\mathcal {X},x,[x]) \not \models \varphi$.    $\square$