David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jonathan Jenkins Ichikawa
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 downloads19 ( #214,392 of 1,938,536 )
Recent downloads (6 months)3 ( #214,500 of 1,938,536 )
How can I increase my downloads?