[Spot] Re: Regarding LTL with past

David Lidell lidelld@chalmers.se writes:

I'm wondering whether there have been any discussions on extending Spot to support them, and if the developers have any idea of how difficult that would be?

Yes, supporting the past would be helpful. The main issue would be to be able to translate those into automata. I'm not very familiar with translation of past operators; but unless there are tricks that can be use to translate the past and the future separately, I don't think our current translations would be easy to extend.