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 veriﬁcation, and etc. In our work, we focus on the veriﬁcation 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.
|Keywords||Computability, Model Checking, CTL, Dynamic Systems|
|THEME||Life Sciences (theme 5), Energy (theme 4)|
|Publisher||University of Heidelberg|
|Editor||K. Ambos-Spies , B. Loewe , W. Merkle|
|Conference||Computability in Europe|
Collins, P.J, & Zapreev, I.S. (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.