The Epistemology of Nondeterminism

TL;DR

This paper introduces a new epistemic semantics for nondeterministic programs, modeling nondeterminism as an agent's knowledge limitation within a deterministic framework using topology and dynamic topological logic.

Contribution

It develops a novel topological semantics for propositional dynamic logic where nondeterminism is epistemic, and extends the framework to include knowledge and public announcements.

Findings

Dynamic topological logic captures nondeterminism as epistemic uncertainty.

Continuous functions correspond to deterministic processes.

Soundness and completeness of PDL axiomatizations are preserved in the new semantics.

Abstract

This paper proposes new semantics for nondeterministic program execution, replacing the standard relational semantics for propositional dynamic logic (PDL). 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). 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, and show that the topological interpretation of public announcements coincides exactly with a natural interpretation of test programs.