Journal of Logic, Language and Information 18 (4):593-624 (2009)
While classical temporal logics lose track of a state as soon as a temporal operator is applied, several branching-time logics able to repeatedly refer to a state have been introduced in the literature. We study such logics by introducing a new formalism, hybrid branching-time logics, subsuming the other approaches and making the ability to refer to a state more explicit by assigning a name to it. We analyze the expressive power of hybrid branching-time logics and the complexity of their satisfiability problem. As main result, the satisfiability problem for the hybrid versions of several branching-time logics is proved to be 2EXPTIME -complete. To prove the upper bound, the automata-theoretic approach to branching-time logics is extended to hybrid logics. As a result of independent interest, the nonemptiness problem for alternating one-pebble Büchi tree automata is shown to be 2EXPTIME -complete. A common property of the logics studied is that they refer to only one state. This restriction is crucial: The ability to refer to more than one state causes a nonelementary blow-up in complexity. In particular, we prove that satisfiability for NCTL * has nonelementary complexity.
|Keywords||Branching time logic Hybrid logic Temporal logic Complexity CTL Pebble automata Alternating tree automata Symmetric automata|
|Categories||categorize this paper)|
References found in this work BETA
Hybrid Logics: Characterization, Interpolation and Complexity.Carlos Areces, Patrick Blackburn & Maarten Marx - 2001 - Journal of Symbolic Logic 66 (3):977-1010.
Weakly Definable Relations and Special Automata.Michael O. Rabin - 1975 - Journal of Symbolic Logic 40 (4):622-623.
Citations of this work BETA
The Complexity of Satisfiability for Fragments of Hybrid Logic—Part I.Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas, Volker Weber & Felix Weiss - 2010 - Journal of Applied Logic 8 (4):409-421.
Similar books and articles
Moment/History Duality in Prior's Logics of Branching-Time.Alberto Zanardo - 2006 - Synthese 150 (3):483 - 507.
ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse.Linh Anh Nguyen & Andrzej Szałas - 2011 - Studia Logica 98 (3):387-428.
Criteria for Admissibility of Inference Rules. Modal and Intermediate Logics with the Branching Property.Vladimir V. Rybakov - 1994 - Studia Logica 53 (2):203 - 225.
The Complexity of Hybrid Logics Over Equivalence Relations.Martin Mundhenk & Thomas Schneider - 2009 - Journal of Logic, Language and Information 18 (4):493-514.
Hybrid Logics of Separation Axioms.Dmitry Sustretov - 2009 - Journal of Logic, Language and Information 18 (4):541-558.
Complete Axiomatizations for Reasoning About Knowledge and Branching Time.Ron van der Meyden & Ka-shu Wong - 2003 - Studia Logica 75 (1):93 - 123.
Undivided and Indistinguishable Histories in Branching-Time Logics.Alberto Zanardo - 1998 - Journal of Logic, Language and Information 7 (3):297-315.
Added to index2009-06-13
Total downloads20 ( #244,901 of 2,158,472 )
Recent downloads (6 months)1 ( #354,589 of 2,158,472 )
How can I increase my downloads?