Conference Proceedings
Non-deterministic temporal logics for general flow systems
JM Davoren, V Coulthard, N Markey, T Moor
Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics | SPRINGER-VERLAG BERLIN | Published : 2004
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. © Springer-Verlag 2004.