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!