greetings. This is Edmond Irani Liu, a Ph.D student at the Cyber-Physical Systems Group, Technical University of Munich. First of all, I would say thank you for your effort in developing such a great platform and tool!

I will explain a bit about how we have used Spot in our research and then pose my questions below. We are recently working on formalization of traffic rules to further obtain traffic rule-compliant motion trajectories for automated vehicles. As a simple prototype, we have used Spot to translated some simple rules in LTL into a Büchi Automaton and later obtained its product automaton with the transition system of the discrete states of the vehicle. We could obtain some nice results with it : ) We are now trying to take one step further and to formalize more traffic rules, but came across the limitations of LTL, and switched to MTL for the reason that it is able to specify timed constraints, e.g. Always keep a safe distance to a leading vehicle if it did not perform a cut-in maneuver for the last 3 seconds.

My questions are as follows:

By any chance, is there some kind of workaround in Spot with which one can incorporate the mentioned timed constraints? (Last x seconds, future x seconds, ..) Of course our system state is also discrete with a 0.1 seconds step in time.

If it is not possible with Spot, do you know some related model checker which can potentially handle this situation? I have been looking around but so far did not come across a tool which handles MTL/timed-automaton as nicely as Spot handles LTL.

Thank you very much for your time reading this mail. I appreciate in advance for any feedback regarding the content.