D | |
---|---|

[DCM+04] | Jennifer M. Davoren,
Vaughan Coulthard,
Nicolas Markey, and
Thomas Moor.
Non-deterministic Temporal Logics for General Flow
Systems.
In HSCC'04,
Lecture Notes in Computer Science 2993, pages 280-295. Springer-Verlag, March 2004.
- 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.}, } |

- 1
- 1
- 1
- 1