Computer Science – Logic in Computer Science
Scientific paper
2007-08-13
Computer Science
Logic in Computer Science
An extended abstract of this paper was presented at the International Workshop on Hybrid Logics (HyLo 2007)
Scientific paper
Hybrid branching-time logics are introduced as extensions of CTL-like logics with state variables and the downarrow-binder. Following recent work in the linear framework, only logics with a single variable are considered. The expressive power and the complexity of satisfiability of the resulting logics is investigated. As main result, the satisfiability problem for the hybrid versions of several branching-time logics is proved to be 2EXPTIME-complete. These branching-time logics range from strict fragments of CTL to extensions of CTL that can talk about the past and express fairness-properties. The complexity gap relative to CTL is explained by a corresponding succinctness result. To prove the upper bound, the automata-theoretic approach to branching-time logics is extended to hybrid logics, showing that non-emptiness of alternating one-pebble Buchi tree automata is 2EXPTIME-complete.
No associations
LandOfFree
Hybrid Branching-Time Logics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Hybrid Branching-Time Logics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Hybrid Branching-Time Logics will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-23661