Non-deterministic Semantics for Dynamic Topological Logic

TL;DR

This paper introduces a non-deterministic semantics for Dynamic Topological Logic, enhancing the reasoning framework for properties of dynamical systems with topological and temporal components.

Contribution

It proposes a novel non-deterministic semantic approach for DTL, improving its expressive power and applicability to complex dynamical systems.

Findings

Non-deterministic semantics provide greater flexibility in modeling dynamical systems.

The new semantics preserve key logical properties of DTL.

Enhanced reasoning capabilities for topological and temporal properties.

Abstract

Dynamic Topological Logic ($\mathcal{DTL}$) is a combination of $\mathcal{S}${\em 4}, under its topological interpretation, and the temporal logic $\mathcal{LTL}$ interpreted over the natural numbers. $\mathcal{DTL}$ is used to reason about properties of dynamical systems based on topological spaces. Semantics are given by dynamic topological models, which are tuples $\left <X,\mathcal{T},f,V\right >$, where $\left <X,\mathcal{T}\right >$ is a topological space, $f$ a function on $X$ and $V$ a truth valuation assigning subsets of $X$ to propositional variables.