References

Linear-time Temporal Logic on finite traces (LTLf) and Linear Dynamic Logic on finite traces (LDLf) are two logical formalisms that are at the centre of prolific research activity.

In particular, the simplicity and naturalness of LTL for temporal specifications is appealing for fields like:

• Reasoning about actions and planning
• Business process specification and verification

Here's a list of recommended readings:

• Giuseppe De Giacomo and Moshe Y. Vardi. "Linear Temporal Logic and Linear Dynamic Logic on Finite Traces." IJCAI (2013)
• Giuseppe De Giacomo and Moshe Y. Vardi. "Synthesis for LTL and LDL on finite traces." IJCAI (2015)
• Giuseppe De Giacomo and Moshe Y. Vardi. "LTLf and LDLf synthesis under partial observability." IJCAI (2016)
• Brafman Ronen, De Giacomo Giuseppe, AND Patrizi Fabio. "LTLf/LDLf Non-Markovian Rewards" AAAI (2018)