Pure-Past Linear Temporal and Dynamic Logic on Finite Traces

Pure-Past Linear Temporal and Dynamic Logic on Finite Traces

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

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence
Survey track. Pages 4959-4965. https://doi.org/10.24963/ijcai.2020/690

We review PLTLf and PLDLf, the pure-past versions of the well-known logics on finite traces LTLf and LDLf, respectively. PLTLf and PLDLf are logics about the past, and so scan the trace backwards from the end towards the beginning. Because of this, we can exploit a foundational result on reverse languages to get an exponential improvement, over LTLf /LDLf , for computing the corresponding DFA. This exponential improvement is reflected in several forms of 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 LTLf (resp.,LDLf) is quite expensive. Hence, to take advantage of the exponential improvement, properties of interest must be directly expressed in PLTLf /PLDLf .
Keywords:
Planning and Scheduling: general
Knowledge Representation and Reasoning: general