Dynamic Topological Logic Interpreted over Minimal Systems

Dynamic Topological Logic (DTLmathcal{DTL}) is a modal logic which combines spatial and temporal modalities for reasoning about dynamic topological systems, which are pairs consisting of a topological space X and a continuous function f : X → X. The function f is seen as a change in one unit of time; within DTLmathcal{DTL} one can model the long-term behavior of such systems as f is iterated. One class of dynamic topological systems where the long-term behavior of f is particularly interesting is that of minimal systems; these are dynamic topological systems which admit no proper, closed, f-invariant subsystems. In such systems the orbit of every point is dense, which within DTLmathcal{DTL} translates into a non-trivial interaction between spatial and temporal modalities. This interaction, however, turns out to make the logic simpler, and while DTLmathcal{DTL}s in general tend to be undecidable, interpreted over minimal systems we obtain decidability, although not in primitive recursive time; this is the main result that we prove in this paper. We also show that DTLmathcal{DTL} interpreted over minimal systems is incomplete for interpretations on relational Kripke frames and hence does not have the finite model property; however it does have a finite non-deterministic quasimodel property. Finally, we give a set of formulas of DTLmathcal{DTL} which characterizes the class of minimal systems within the class of dynamic topological systems, although we do not offer a full axiomatization for the logic.