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

Complexity and succinctness issues for linear-time hybrid logics

LANOTTE, RUGGERO
2010-01-01

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
Bozzelli, L.; Lanotte, Ruggero
File in questo prodotto:
File Dimensione Formato  
lanotteTheor.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: DRM non definito
Dimensione 1.16 MB
Formato Adobe PDF
1.16 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/1717401
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 2
social impact