Academic
Publications
Complexity and succinctness issues for linear-time hybrid logics

Complexity and succinctness issues for linear-time hybrid logics,10.1016/j.tcs.2009.08.009,Theoretical Computer Science,Laura Bozzelli,Ruggero Lanotte

Complexity and succinctness issues for linear-time hybrid logics  
BibTex | RIS | RefWorks Download
Full linear-time hybrid logic (HL) is a non-elementary and equally expressive extension of standard LTL + past obtained by adding the well-known binder operators ↓ and ∃. We investigate complexity and succinctness issues for HL in terms of the number of variables and nesting depth of binder modalities. First, we present direct automata-theoretic decision procedures for satisfiability and model-checking of HL, which require space of exponential height equal to the nesting depth of the binder modalities. The proposed algorithms are proved to be asymptotically optimal by providing matching lower bounds. Second, we show that, for the one-variable fragment of HL, the considered problems are elementary and, precisely, Expspace-complete. Finally, we show that, for all 0≤hk, there is a succinctness gap between the fragments HLk and HLh with binder nesting depth at most k and h, respectively, of exponential height equal to k−h.
Journal: Theoretical Computer Science - TCS , vol. 411, no. 2, pp. 454-469, 2010
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.