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

 

Dr. Ivan Zapreev (CWI, NL)

 

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.