Dynamic Topological Logic Interpreted over Minimal Systems

Dynamic Topological Logic (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 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 DTL translates into a non-trivial interaction between spatial and temporal modalities. This interaction, however, turns out to make the logic simpler, and while DTLs 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 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 DTLwhich characterizes the class of minimal systems within the class of dynamic topological systems, although we do not offer a full axiomatization for the logic.