This paper focuses on LTL on finite traces (LTLf ) for which satisfiability is known to be PSPACE-complete. However, little is known about the computational properties of fragments of LTLf . In this paper we fill this gap and make the following contributions. First, we identify several LTLf fragments for which the complexity of satisfiability drops to NP-complete or even P, by considering restrictions on the temporal operators and Boolean connectives being allowed. Second, we study a semantic variant of LTLf , which is of interest in the domain of business processes, where models have the property that precisely one propositional variable evaluates true at each time instant. Third, we introduce a reasoner for LTLf and compare its performance with the state of the art.

The complexity of LTL on finite traces: Hard and easy fragments

FIONDA, Valeria;GRECO, Gianluigi
2016-01-01

Abstract

This paper focuses on LTL on finite traces (LTLf ) for which satisfiability is known to be PSPACE-complete. However, little is known about the computational properties of fragments of LTLf . In this paper we fill this gap and make the following contributions. First, we identify several LTLf fragments for which the complexity of satisfiability drops to NP-complete or even P, by considering restrictions on the temporal operators and Boolean connectives being allowed. Second, we study a semantic variant of LTLf , which is of interest in the domain of business processes, where models have the property that precisely one propositional variable evaluates true at each time instant. Third, we introduce a reasoner for LTLf and compare its performance with the state of the art.
2016
978-157735760-5
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/20.500.11770/167497
 Attenzione

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

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