18 Nov
2020
18 Nov
'20
9:43 a.m.
Dear Edmond,
On Wed, Nov 18, 2020 at 8:01 AM Edmond Irani Liu <edmond.irani(a)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
--
Alexandre Duret-Lutz