Non-deterministic semantics for dynamic topological logic

AbstractDynamic Topological Logic (DTL) is a combination of S4, under its topological interpretation, and the temporal logic LTL interpreted over the natural numbers. DTL is used to reason about properties of dynamical systems based on topological spaces. Semantics are given by dynamic topological models, which are tuples <X,T,f,V>, where <X,T> is a topological space, f a function on X and V a truth valuation assigning subsets of X to propositional variables.Our main result is that the set of valid formulas of DTL over spaces with continuous functions is recursively enumerable. We show this by defining alternative semantics for DTL. Under standard semantics, DTL is not complete for Kripke frames. However, we introduce the notion of a non-deterministic quasimodel, where the function f is replaced by a binary relation g assigning to each world multiple temporal successors. We place restrictions on the successors so that the logic remains unchanged; under these alternative semantics, DTL becomes Kripke-complete. We then apply model-search techniques to enumerate the set of all valid formulas