Computable CTL for Discrete-Time and Continuous-Space Dynamic Systems

Dynamic systems are widely applied for modelling and analysis in physiology, biology, chemistry and engineering. The high-profile and safety-critical nature of such applications has resulted in a large amount of work on formal methods for dynamic systems: mathematical logics, computational methods, formal verification, and etc. In our work, we focus on the verification approach called model checking, and its computability aspects. In this approach, a desired system property, specified using some logical formalism, is verified against the dynamic-system model via an exhaustive state-space exploration. This process typically involves computation of reachable and/or chain-reachable sets that in certain cases can not be obtained due to the continuity of state-space domain. Therefore, in this paper, we use topological approach along with the computability results of Type Two theory of Effectivity in order to construct a computable CTL semantics for discrete-time and continuous-space dynamic systems.