Data di Pubblicazione:
2010
Abstract:
Full linear-time hybrid logic (HL) is a non-elementary and equally expressive extension
of standard LTL C past obtained by adding the well-known binder operators. We
investigate complexity and succinctness issues for HL in terms of the number of variables
and nesting depth of binder modalities. First,wepresent 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 <= h < k, there is a
succinctness gap between the fragments HL^k and HL^h with binder nesting depth at most k
and h, respectively, of exponential height equal to k
of standard LTL C past obtained by adding the well-known binder operators. We
investigate complexity and succinctness issues for HL in terms of the number of variables
and nesting depth of binder modalities. First,wepresent 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 <= h < k, there is a
succinctness gap between the fragments HL^k and HL^h with binder nesting depth at most k
and h, respectively, of exponential height equal to k
Tipologia CRIS:
Articolo su Rivista
Elenco autori:
Bozzelli, L.; Lanotte, Ruggero
Link alla scheda completa:
Pubblicato in: