David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
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)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
Carlos Areces, Patrick Blackburn & Maarten Marx (2001). Hybrid Logics: Characterization, Interpolation and Complexity. Journal of Symbolic Logic 66 (3):977-1010.
Michael O. Rabin (1975). Weakly Definable Relations and Special Automata. Journal of Symbolic Logic 40 (4):622-623.
Citations of this work BETA
Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas, Volker Weber & Felix Weiss (2010). The Complexity of Satisfiability for Fragments of Hybrid Logic—Part I. Journal of Applied Logic 8 (4):409-421.
Similar books and articles
Alberto Zanardo (2006). Moment/History Duality in Prior's Logics of Branching-Time. Synthese 150 (3):483 - 507.
Linh Anh Nguyen & Andrzej Szałas (2011). ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse. Studia Logica 98 (3):387-428.
Tadeusz Litak & Frank Wolter (2005). All Finitely Axiomatizable Tense Logics of Linear Time Flows Are CoNP-Complete. Studia Logica 81 (2):153 - 165.
Vladimir V. Rybakov (1994). Criteria for Admissibility of Inference Rules. Modal and Intermediate Logics with the Branching Property. Studia Logica 53 (2):203 - 225.
Martin Mundhenk & Thomas Schneider (2009). The Complexity of Hybrid Logics Over Equivalence Relations. Journal of Logic, Language and Information 18 (4):493-514.
Dmitry Sustretov (2009). Hybrid Logics of Separation Axioms. Journal of Logic, Language and Information 18 (4):541-558.
Ron van der Meyden & Ka-shu Wong (2003). Complete Axiomatizations for Reasoning About Knowledge and Branching Time. Studia Logica 75 (1):93 - 123.
Alberto Zanardo (1998). Undivided and Indistinguishable Histories in Branching-Time Logics. Journal of Logic, Language and Information 7 (3):297-315.
Roberto Ciuni & Alberto Zanardo (2010). Completeness of a Branching-Time Logic with Possible Choices. Studia Logica 96 (3):393-420.
Added to index2009-06-13
Total downloads18 ( #206,188 of 1,907,059 )
Recent downloads (6 months)2 ( #345,104 of 1,907,059 )
How can I increase my downloads?