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.
|Computability, Model Checking, CTL, Dynamic Systems|
|Software/Program Verification (acm D.2.4)|
|Specification and verification (program logics, model checking, etc.) (msc 68Q60)|
|Life Sciences (theme 5), Energy (theme 4)|
|Modelling, Analysis and Simulation [MAS]|
Collins, P.J, & Zapreev, I.S. (2009). Computable CTL for discrete-time and continuous-space dynamic systems. Modelling, Analysis and Simulation [MAS]. CWI.