COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS

被引：1

作者：

Collins, Pieter ^{[1
]}

Zapreev, Ivan S. ^{[1
]}

机构：

[1] Ctr Wiskunde & Informat, NL-1098 XG Amsterdam, Netherlands

来源：

INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE | 2011年 / 22卷 / 04期

关键词：

Computability; model checking; CTL; LTL; computable semantics; dynamic systems; TEMPORAL LOGIC; SETS;

D O I：

10.1142/S012905411100843X

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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 Buchi automaton corresponding to the verified LTL formula.

引用

页码：801 / 821

页数：21

共 17 条

[1] Artemov S. N., 1997, INT C DEC CONTR CDC, V1, P698
[2] Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
[3] BALLUCHI A, 2006, S MATH THEO IN PRESS
[4] Computability on subsets of metric spaces
Brattka, V
Presser, G
[J]. THEORETICAL COMPUTER SCIENCE, 2003, 305 (1-3) : 43 - 76
[5] AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS
CLARKE, EM
EMERSON, EA
SISTLA, AP
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02): : 244 - 263
[6] Continuity and computability of reachable sets
Collins, P
[J]. THEORETICAL COMPUTER SCIENCE, 2005, 341 (1-3) : 162 - 195
[7] Optimal semicomputable approximations to reachable and invariant sets
Collins, Pieter
[J]. THEORY OF COMPUTING SYSTEMS, 2007, 41 (01) : 33 - 48
[8] Collins Pieter J., 2009, P 3 INT WORKSH REACH, P107
[9] Collins Pieter J., 2009, COMPUTABILITY EUROPE
[10] Collins Pieter J., 2009, COMPUTABILITY EUROPE, P110

← 1 2 →