13 Aug
2014
13 Aug
'14
10:02 a.m.
Hi Caroline,
On Wed, Aug 13, 2014 at 8:28 AM, Caroline Lemieux
<caro.lemieux(a)gmail.com> wrote:
I'm an undergraduate student at UBC working on a log analysis project under
Ivan Beschastnikh. I'm using SPOT in the project to parse LTL strings into
formulae, and now trying to use the translation to automata functionality.
The situation I'm dealing with would involve passing a finite sequence of states
into the automaton, and the description of the Monitor output appeared to be
what I needed. However, the monitor DFA provided for the response formula
G(a->Fb) was an all-accepting DFA: which didn't seem to align with the given
definition of monitor.
Spot's interpretation of LTL is always on infinite words, while it sounds like
you might be interested in using some finite-word semantics.
A monitor can only reject finite prefixes of infinite words. Here
there is no finite
prefixe that can invalidate G(a->Fb) as you never know if some b isn't coming
later. The same output is expected for just Fb.
I've been searching the documentation, but
can't find anything more describing
why this DFA would be produced.
The procedure is similar to the one described in
@InProceedings{ tabakov.10.rv,
author = {Deian Tabakov and Moshe Y. Vardi},
title = {Optimized Temporal Monitors for SystemC{$^*$}},
booktitle = {Proceedings of the 10th International Conferance
on Runtime Verification},
pages = {436--451},
year = 2010,
volume = {6418},
series = {Lecture Notes in Computer Science},
month = nov,
publisher = {Springer-Verlag}
}
The above reference appears only in the documentation of the
minimize_monitor() function (src/tgbaalgos/minimize.hh). I'll add a
copy to the man page of ltl2tgba in the next version.
I've also been looking for a description of
acceptance condition syntax, especially for the state-based degeneralized Buchi automaton,
where both edges and states are labeled as accepting.
Spot only handles transition-based acceptance internally. Transition
can be labeled by acceptance marks between braces, like {Acc[a],
Acc[b]}. The names used do not matter; what matters is that accepting
runs must see each name infinitely often.
When you request state-based acceptance, Spot will ensure all
transitions leaving a state have the same acceptance marks. It will
also mark the states with outgoing accepting transitions using
double-circles, but these double-circles are just decoration.
This is explained at the beginning of
http://spot.lip6.fr/userdoc/ltl2tgba.html so please let me know if it
should be clarified somehow.
Hope this helps,
--
Alexandre Duret-Lutz