Home » Publication » 23049

Dettaglio pubblicazione

2020, IJCAI, Pages 4959-4965

Pure-Past Linear Temporal and Dynamic Logic on Finite Traces (04c Atto di convegno in rivista)

De Giacomo Giuseppe, Di Stasio Antonio, Fuggitti Francesco, Rubin Sasha

LTLf and LDLf are well-known logics on finite traces. We review PLTLf and PLDLf, their pure- past versions. These are interpreted backward from the end of the trace towards the beginning. Because of this, we can exploit a foundational result on reverse languages to get an exponential improvement, wrt LTLf /LDLf, in computing the corresponding DFA. This exponential improvement is reflected in several forms sequential decision making involving temporal specifications, such as planning and decision problems in non-deterministic and non-Markovian domains. Interestingly, PLTLf (resp. PLDLf ) has the same expressive power as LTLf (resp. LDLf ), but transforming a PLTLf (resp. PLDLf ) formula into its equivalent in LTLf (resp. LDLf ) is quite expensive. Hence, to take advantage of the exponential improvement, properties of interest must be directly expressed in PLTLf /PLTLf .
© Università degli Studi di Roma "La Sapienza" - Piazzale Aldo Moro 5, 00185 Roma