Graduate studies at Western
Journal of Logic, Language and Information 18 (4):593-624 (2009)
|Abstract||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)|
|Through your library||Configure|
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 downloads6 ( #154,793 of 739,315 )
Recent downloads (6 months)1 ( #61,243 of 739,315 )
How can I increase my downloads?