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
Question 1. Would past-time temporal logic help here? Where can I find more about them?
In terms of expressivity, no. By a theorem of [1], every linear temporal formula (including past operators) is equivalent to a future formula if one is only interested in defining properties of time structures with a starting point.
[1] Dov M. Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. On the temporal analysis of fairness, POPL 1980: 163-173, 1980.
Question 2. Are there other temporal logic(s) which work on a finite number of states?
Yes, for instance modular temporal logic [2], which makes use of a temporal operator able to count modulo $q$ or the extensions proposed by in [3, 4].
[2] A. Baziramwabo, P. McKenzie, D. Thérien: Modular Temporal Logic, LICS 1999, 344-351.
[3] Z. Ésik, Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators, Developments in Language Theory 2002, LNCS 2450, Springer (2003) 43-58.
[4] P. Wolper, Temporal logic can be more expressive, Information and Control 56 (1983), 72–99.