Hi David, The following one might be helpful. http://ltlf2dfa.diag.uniroma1.it/ Best, Shufang On Sat, May 14, 2022 at 11:16 PM David Lidell <lidelld@chalmers.se> wrote:

Hi!

I am a PhD student from the University of Gothenburg, and I am currently working a lot with LTL extended with the past operators Y and S. Spot is a fantastic tool, but it unfortunately doesn't support these operators.

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?

Thanks! _______________________________________________ Spot mailing list -- spot@lrde.epita.fr To unsubscribe send an email to spot-leave@lrde.epita.fr

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.