Event Detail

Propositional dynamic logic (PDL) is a framework for reasoning about nondeterministic program executions (or, more generally, nondeterministic actions). In this setting, nondeterminism is taken as a primitive: a program is nondeterministic iff it has multiple possible outcomes. But what does “possible” mean, here? This talk explores an epistemic interpretation: working in an enriched logical setting, we represent nondeterminism as a relationship between a program and an agent deriving from the agent’s (in)ability to adequately measure the dynamics of the program execution. More precisely, using topology and the framework of dynamic topological logic, we show that dynamic topological models 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 prove that certain axiomatizations of PDL remain sound and complete with respect to corresponding classes of dynamic topological models. We also 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. Finally, we sketch a generalization of the topological paradigm in which the distinction between action and measurement (i.e, between functions and opens) is erased, highlighting some preliminary results in this direction.