Computable CTL* for discrete-time and continuous-space dynamic systems

The CTL* model-checking problem is thoroughly studied and is fully understood for finite and countable state spaces. Yet, in most models arising in the sciences and engineering the system’s state space is uncountable. Then, the standard computability and complexity theory is inapplicable but the semantics of CTL* has to be in some sense computable to allow for model-checking algorithms that are implementable on digital computers. To tackle this problem, we consider discrete-time continuous-space dynamic systems for which we study the computability of the standard semantics of CTL* and provide a variant thereof computable in the sense of Type-2 Theory of Effectivity.