In this work, we consider discrete-time continuous-space dynamic systems for which we study the computability of the standard semantics of CTL* (CTL and LTL) and provide a variant thereof computable in the sense of Type-2 Theory of Effectivity. In particular, we show how the computable model checking of existentially and universally quantified path formulae of LTL can be reduced to solving, respectively, repeated reachability and persistence problems on a model obtained as a parallel composition of the original one and a non-deterministic Buchi automaton corresponding to the verified LTL formula.
Additional Metadata
Keywords Computability, Model Checking, CTL, LTL, CTL*, Computable semantics, Dynamic Systems
ACM Performance Analysis and Design Aids (acm B.2.2)
MSC Computability and recursion theory on ordinals, admissible sets, etc. (msc 03D60)
THEME Life Sciences (theme 5), Energy (theme 4)
Publisher CWI
Series CWI. Department of Modelling, Analysis and Computing [MAC]
Project Computational Topology for Systems and Control
Note This research was supported by the Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO) Vidi grant 639.032.408.
Citation
Collins, P.J, & Zapreev, I.S. (2010). Computable Semantics for CTL* on Discrete-Time and Continuous-Space Dynamic Systems. CWI. Department of Modelling, Analysis and Computing [MAC]. CWI.