Computable semantics for CTL* on discrete time and continuous space dynamic systems

Pieter Collins; Ivan S. Zapreev

doi:10.1142/S012905411100843X

Computable semantics for CTL* on discrete time and continuous space dynamic systems

Pieter Collins, Ivan S. Zapreev^*

^*Corresponding author for this work

BioMathematics and BioInformatics

Research output: Contribution to journal › Article › Academic › peer-review

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

Original language	English
Pages (from-to)	801-821
Number of pages	21
Journal	Int. J. Found. Comput. Sci.
Volume	22
Issue number	4
DOIs	https://doi.org/10.1142/S012905411100843X
Publication status	Published - 2011

Access to Document

10.1142/S012905411100843X

Cite this

@article{dccb7aa24b214015811f105b23bc165f,

title = "Computable semantics for CTL* on discrete time and continuous space dynamic systems",

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

author = "Pieter Collins and Zapreev, {Ivan S.}",

year = "2011",

doi = "10.1142/S012905411100843X",

language = "English",

volume = "22",

pages = "801--821",

journal = "Int. J. Found. Comput. Sci.",

publisher = "World Scientific Publishing Company",

number = "4",

}

TY - JOUR

T1 - Computable semantics for CTL* on discrete time and continuous space dynamic systems

AU - Collins, Pieter

AU - Zapreev, Ivan S.

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

U2 - 10.1142/S012905411100843X

DO - 10.1142/S012905411100843X

M3 - Article

VL - 22

SP - 801

EP - 821

JO - Int. J. Found. Comput. Sci.

JF - Int. J. Found. Comput. Sci.

IS - 4

ER -