Non-deterministic temporal logics for general flow systems

Jennifer M. Davoren; Vangham Coulthard; Nicolas Markey; Thomas Moor

doi:10.1007/978-3-540-24743-2_19

Non-deterministic temporal logics for general flow systems

Jennifer M. Davoren, Vangham Coulthard, Nicolas Markey, Thomas Moor

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

33 Citations (Scopus)

Abstract

In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discretetime transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL*, which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL*, but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL* and establish its soundness w.r.t. the general flow semantics.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Rajeev Alur, George J. Pappas
Publisher	Springer Verlag
Pages	280-295
Number of pages	16
ISBN (Print)	3540212590, 9783540212591
DOIs	https://doi.org/10.1007/978-3-540-24743-2_19
Publication status	Published - 2004

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2993
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-540-24743-2_19

Cite this

Davoren, J. M., Coulthard, V., Markey, N., & Moor, T. (2004). Non-deterministic temporal logics for general flow systems. In R. Alur, & G. J. Pappas (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 280-295). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2993). Springer Verlag. https://doi.org/10.1007/978-3-540-24743-2_19

Davoren, Jennifer M. ; Coulthard, Vangham ; Markey, Nicolas et al. / Non-deterministic temporal logics for general flow systems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Rajeev Alur ; George J. Pappas. Springer Verlag, 2004. pp. 280-295 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{f989eca4340343169df3a92805680d74,

title = "Non-deterministic temporal logics for general flow systems",

abstract = "In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discretetime transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL*, which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL*, but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL* and establish its soundness w.r.t. the general flow semantics.",

author = "Davoren, \{Jennifer M.\} and Vangham Coulthard and Nicolas Markey and Thomas Moor",

year = "2004",

doi = "10.1007/978-3-540-24743-2\_19",

language = "English",

isbn = "3540212590",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "280--295",

editor = "Rajeev Alur and Pappas, \{George J.\}",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

address = "Germany",

}

Davoren, JM, Coulthard, V, Markey, N & Moor, T 2004, Non-deterministic temporal logics for general flow systems. in R Alur & GJ Pappas (eds), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2993, Springer Verlag, pp. 280-295. https://doi.org/10.1007/978-3-540-24743-2_19

Non-deterministic temporal logics for general flow systems. / Davoren, Jennifer M.; Coulthard, Vangham; Markey, Nicolas et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Rajeev Alur; George J. Pappas. Springer Verlag, 2004. p. 280-295 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2993).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

TY - CHAP

T1 - Non-deterministic temporal logics for general flow systems

AU - Davoren, Jennifer M.

AU - Coulthard, Vangham

AU - Markey, Nicolas

AU - Moor, Thomas

PY - 2004

Y1 - 2004

N2 - In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discretetime transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL*, which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL*, but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL* and establish its soundness w.r.t. the general flow semantics.

AB - In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discretetime transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL*, which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL*, but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL* and establish its soundness w.r.t. the general flow semantics.

UR - http://www.scopus.com/inward/record.url?scp=33847000790&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-24743-2_19

DO - 10.1007/978-3-540-24743-2_19

M3 - Chapter

SN - 3540212590

SN - 9783540212591

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 280

EP - 295

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Alur, Rajeev

A2 - Pappas, George J.

PB - Springer Verlag

ER -

Davoren JM, Coulthard V, Markey N, Moor T. Non-deterministic temporal logics for general flow systems. In Alur R, Pappas GJ, editors, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2004. p. 280-295. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-24743-2_19

Non-deterministic temporal logics for general flow systems

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Cite this