KR2023Proceedings of the 20th International Conference on Principles of Knowledge Representation and ReasoningProceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning

Rhodes, Greece. September 2-8, 2023.

Edited by

ISSN: 2334-1033
ISBN: 978-1-956792-02-7

Sponsored by
Published by

Copyright © 2023 International Joint Conferences on Artificial Intelligence Organization

A Singly Exponential Transformation of LTL[X, F] into Pure Past LTL

  1. Alessandro Artale(Free University of Bozen-Bolzano)
  2. Luca Geatti(University of Udine)
  3. Nicola Gigante(Free University of Bozen-Bolzano, Italy)
  4. Andrea Mazzullo(Free University of Bozen-Bolzano, Italy)
  5. Angelo Montanari(University of Udine)


  1. Computational aspects of knowledge representation
  2. Geometric, spatial, and temporal reasoning
  3. Reasoning with time, space and perceptions


Confronting the past can be hard. This is true even in Linear Temporal Logic (LTL), interpreted on either infinite or finite traces, when faced with the problem of transforming a temporally future formula into an equivalent one that contains past temporal modalities only. To our knowledge, the best among the available pastification procedures for full LTL, as well as for expressive enough fragments of it (that is, containing at least one temporal modality other than tomorrow), are triply exponential in the size of the input. In this paper, we focus on the fragment of LTL that features the tomorrow and eventually modalities, and provide a singly exponential pastification algorithm for it. The transformation is based on a normalisation procedure that requires a non-trivial complexity analysis, and on the subsequent generation of a pure past formula from suitably-defined dependency tree structures. Moreover, leveraging its purely syntactic nature, we present an implementation of our procedure in a temporal satisfiability checking tool that deals with both future and past modalities.