The intuitionistic temporal logic of dynamical systems

TL;DR

This paper introduces a decidable intuitionistic temporal logic, ${ m ITL^c}$, for dynamical systems, capable of expressing complex asymptotic behaviors like minimality and recurrence.

Contribution

It presents a new variant of Kremer's logic, ${ m ITL^c}$, which is decidable and expressive enough to capture significant dynamical properties.

Findings

${ m ITL^c}$ is decidable.

${ m ITL^c}$ can express minimality.

${ m ITL^c}$ can express Poincaré recurrence.

Abstract

A dynamical system is a pair $(X,f)$, where $X$ is a topological space and $f\colon X\to X$ is continuous. Kremer observed that the language of propositional linear temporal logic can be interpreted over the class of dynamical systems, giving rise to a natural intuitionistic temporal logic. We introduce a variant of Kremer's logic, which we denote ${\sf ITL^c}$, and show that it is decidable. We also show that minimality and Poincar\'e recurrence are both expressible in the language of ${\sf ITL^c}$, thus providing a decidable logic expressive enough to reason about non-trivial asymptotic behavior in dynamical systems.