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.

, , ,
,
University of Heidelberg
K. Ambos-Spies , B. Loewe , W. Merkle
Computability in Europe
Scientific Computing

Collins, P., & Zapreev, I. (2009). Computable CTL for Discrete-Time and Continuous-Space Dynamic Systems. In K. Ambos-Spies, B. Loewe, & W. Merkle (Eds.), Mathematical Theory and Computational Practice, Fifth Conference on Computability in Europe Abstract Booklet (pp. 99–109). University of Heidelberg.