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.

, , , , ,
,
Springer
O. Bournez , I. Potapov
Lecture Notes in Computer Science
Computational Topology for Systems and Control
Workshop on Reachability Problems
Scientific Computing

Collins, P., & Zapreev, I. (2009). Computable CTL* for discrete-time and continuous-space dynamic systems. In O. Bournez & I. Potapov (Eds.), Proceedings of Workshop on Reachability Problems 2009 (WRP 3) (pp. 107–119). Springer.