Nicolas Markey

Abstract

In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discrete-time 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.

@inproceedings{hscc2004-DCMM,
  author =              {Davoren, Jennifer M. and Coulthard, Vaughan and
                         Markey, Nicolas and Moor, Thomas},
  title =               {Non-deterministic Temporal Logics for General Flow
                         Systems},
  editor =              {Alur, Rajeev and Pappas, George J.},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'04)},
  acronym =             {{HSCC}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2993},
  pages =               {280-295},
  year =                {2004},
  month =               mar,
  doi =                 {10.1007/978-3-540-24743-2_19},
  abstract =            {In this paper, we use the constructs of branching
                         temporal logic to formalize reasoning about a class
                         of general flow systems, including discrete-time
                         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.},
}