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 -