Resources on finite Temporal Logic


I am looking for resources on finite Temporal Logic(s). I found some resources mentioning Past-Time TL, but I can’t find any resource/paper describing it in any sort of detail and I was hoping that somebody here might be able to point me in the right direction.

The main use case is a tool that does test case generation and then uses some variant of TL to check if some propositions hold. It should be obvious that this means we have constraints on the depth (and breadth) that can be generated/searched. The current implementation basically allows for next, globally, and until. However, using eventually is problematic: what if the random generation just doesn’t get to the desired state?

So I guess I have two questions:

  • would past-time temporal logic help here? Where can I find more about them?
  • are there other temporal logic(s) which work on a finite number of states?

In case anyone’s curious, the project I’m talking about is https://docs.quickstrom.io/ (I am not the author, but I am interested in the idea). More info on the specification language used can be found here https://github.com/quickstrom/quickstrom/blob/main/docs/source/topics/specification-language.rst