Dear Edmond,
On Wed, Nov 18, 2020 at 8:01 AM Edmond Irani Liu edmond.irani@tum.de wrote:
[...] the limitations of LTL, and switched to MTL for the reason that it is able to specify timed constraints, [...]
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.
Spot has no support for timed automata however if each step in your system corresponds to 0.1 seconds and all your time constraints are multiples of that, you can probably reduce some of your MTL formulas to LTL formulas ?
Spot has the following "syntactic sugar" operators that may help: F[0..10]a = a | X(a | X(a | X(a | X(a | X(a | X(a | X(a | X(a | X(a | Xa))))))))) G[0..10]a = a & X(a & X(a & X(a & X(a & X(a & X(a & X(a & X(a & X(a & Xa)))))))))
I'm not very familiar with MTL, but in your discretized case, I suspect that an MTL formula like "a U[0..10] b", which isn't understood by Spot, can be expressed as "(a U b) && F[0..10]b", which Spot would understand?
Unfortunately Spot has now support for past operators
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.
Sorry, I'm not very familiar with this topic and tools that support MTL.
Best regards