We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS.
- Authors
COLLINS, PIETER; ZAPREEV, IVAN S.; Bournez, Oliver; Potapov, Igor
- Abstract
In this work, we consider Discrete-Time Continuous-Space Dynamic Systems for which we study the computability of the standard semantics of CTL* (CTL, 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 Büchi automaton corresponding to the verified LTL formula.
- Subjects
PROGRAMMING language semantics; DISCRETE-time systems; MACHINE theory; COMPUTABLE functions; MATHEMATICAL models; PROBLEM solving; COMPUTER science
- Publication
International Journal of Foundations of Computer Science, 2011, Vol 22, Issue 4, p801
- ISSN
0129-0541
- Publication type
Article
- DOI
10.1142/S012905411100843X