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.

Additional Metadata
Keywords Computability, Model Checking, CTL*Abstract. The CT L&#8727, model-checking problem is thoroughly studied and is fully understood for &#64257, nite and countable state spaces. Yet, in most models arising in the sciences and engineering the system’s sate s
THEME Life Sciences (theme 5), Energy (theme 4)
Publisher Springer
Editor O. Bournez , I. Potapov
Series Lecture Notes in Computer Science
Project Computational Topology for Systems and Control
Conference Workshop on Reachability Problems
Citation
Collins, P.J, & Zapreev, I.S. (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.