In this paper we look into the assumption of interpreting LTL over finite traces. In particular we show that LTLf, i.e., LTL under this assumption, is less expressive than what might appear at first sight, and that at essentially no computational cost one can make a significant increase in expressiveness while maintaining the same intuitiveness of LTLf. Indeed, we propose a logic, LDLf for Linear Dynamic Logic over finite traces, which borrows the syntax from Propositional Dynamic Logic (PDL), but is interpreted over finite traces. Satisfiability, validity and logical implication (as well as model checking) for LDLf are PSPACE-complete as for LTLf (and LTL).

Linear temporal logic and Linear Dynamic Logic on finite traces / DE GIACOMO, Giuseppe; Moshe Y., Vardi. - In: IJCAI. - ISSN 1045-0823. - STAMPA. - (2013), pp. 854-860. (Intervento presentato al convegno 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013 tenutosi a Beijing nel 3 August 2013 through 9 August 2013).

Linear temporal logic and Linear Dynamic Logic on finite traces

DE GIACOMO, Giuseppe;
2013

Abstract

In this paper we look into the assumption of interpreting LTL over finite traces. In particular we show that LTLf, i.e., LTL under this assumption, is less expressive than what might appear at first sight, and that at essentially no computational cost one can make a significant increase in expressiveness while maintaining the same intuitiveness of LTLf. Indeed, we propose a logic, LDLf for Linear Dynamic Logic over finite traces, which borrows the syntax from Propositional Dynamic Logic (PDL), but is interpreted over finite traces. Satisfiability, validity and logical implication (as well as model checking) for LDLf are PSPACE-complete as for LTLf (and LTL).
2013
23rd International Joint Conference on Artificial Intelligence, IJCAI 2013
finite traces; knowledge representation; temporal logics; vertification
04 Pubblicazione in atti di convegno::04c Atto di convegno in rivista
Linear temporal logic and Linear Dynamic Logic on finite traces / DE GIACOMO, Giuseppe; Moshe Y., Vardi. - In: IJCAI. - ISSN 1045-0823. - STAMPA. - (2013), pp. 854-860. (Intervento presentato al convegno 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013 tenutosi a Beijing nel 3 August 2013 through 9 August 2013).
File allegati a questo prodotto
File Dimensione Formato  
VE_2013_11573-516163.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 548.21 kB
Formato Adobe PDF
548.21 kB Adobe PDF   Contatta l'autore

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/11573/516163
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 415
  • ???jsp.display-item.citation.isi??? ND
social impact