Dynamic Tangled Derivative Logic of Metric Spaces

TL;DR

This paper introduces a new decidable dynamic topological logic combining the Cantor derivative and linear temporal logic, with completeness results for key topological spaces.

Contribution

It develops a decidable, complete logic integrating topological mu-calculus with linear temporal logic for metric space structures.

Findings

The combined logic is decidable.

The logic has a natural axiomatisation.

Completeness is proven for Cantor space and rational numbers.

Abstract

Dynamical systems are abstract models of interaction between space and time. They are often used in fields such as physics and engineering to understand complex processes, but due to their general nature, they have found applications for studying computational processes, interaction in multi-agent systems, machine learning algorithms and other computer science related phenomena. In the vast majority of applications, a dynamical system consists of the action of a continuous 'transition function' on a metric space. In this work, we consider decidable formal systems for reasoning about such structures. Spatial logics can be traced back to the 1940's, but our work follows a more dynamic turn that these logics have taken due to two recent developments: the study of the topological mu-calculus, and the the integration of linear temporal logic with logics based on the Cantor derivative. In this paper, we combine dynamic topological logics based on the Cantor derivative and the 'next point in time' operators with an expressively complete fixed point operator to produce a combination of the topological mu-calculus with linear temporal logic. We show that the resulting logics are decidable and have a natural axiomatisation. Moreover, we prove that these logics are complete for interpretations on the Cantor space, the rational numbers, and subspaces thereof.