References

Linear Temporal Logic on finite traces (LTL_f) and Pure-Past Linear Temporal Logic on finite traces (PLTL_f) are two compelling well-known logical formalisms employed in several contexts, such as:

• Reasoning about Actions and Planning
  • as a specification mechanism for temporally extended goals
  • as constraints on plans
  • as preferences and soft constraints
  • for specifying multi-agent systems
  • for specifying norms
• Business Process Specification and Verification
• Synthesis
• Reinforcement Learning
  • for specifying rewards

They are famous for their clarity and ease of use.

A list of recommended readings:

• Giuseppe De Giacomo, Antonio Di Stasio, Francesco Fuggitti, and Sasha Rubin. "Pure Past Linear Temporal and Dynamic Logic on Finite Traces". IJCAI, 2020
• Brafman Ronen, De Giacomo Giuseppe, and Patrizi Fabio. "LTLf/LDLf Non-Markovian Rewards". AAAI, 2018
• Giuseppe De Giacomo and Moshe Y. Vardi. "LTLf and LDLf synthesis under partial observability". IJCAI, 2016
• Giuseppe De Giacomo and Moshe Y. Vardi. "Synthesis for LTL and LDL on finite traces". IJCAI, 2015
• Giuseppe De Giacomo and Moshe Y. Vardi. "Linear Temporal Logic and Linear Dynamic Logic on Finite Traces". IJCAI, 2013