Hybrid Branching-Time Logics

We introduce hybrid branching-time logics as extensions of CT L-like logics with hybrid machinery such as the downarrow-operator. Following recent work in the linear framework, we restrict to logics with only a single variable. We investigate the expressiveness of the resulting logics and prove their satisfiability problems to be 2EXPTIME-complete. The complexity gap relative to CT L is explained by a corresponding succinctness result. To prove the upper bound, the automata-theoretic approach to branching-time logics is extended to match hybrid logics, showing that non-emptiness of alternating one-pebble B¨uchi tree automata is 2EXPTIMEcomplete.

• Type: Journal
• Year: 2007
• Where: CORR
• Authors: Volker Weber
• Keywords: Branching-time Logics, CORR 2007, CT L-like Logics, Education, Logics