13 Aug
2014
13 Aug
'14
8:28 a.m.
Hello,
I'm an undergraduate student at UBC working on a log analysis project
under Ivan
Beschastnikh <http://www.cs.ubc.ca/~bestchai/>. 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.
I've been searching the documentation, but can't find anything more
describing why this DFA would be produced. 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.
Could you direct me to any documentation on these subjects or give any
insight on why the above monitor is being produced for the response
pattern? (As defined by the specification pattern project here
<http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml>.)
Merci,
Caroline Lemieux
13 Aug
13 Aug
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
3829
days inactive
3829
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Caroline Lemieux