[LTL2TGBA] SPOT translation produces unexpected results
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
Hi Caroline, On Wed, Aug 13, 2014 at 8:28 AM, Caroline Lemieux <caro.lemieux@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
participants (2)
-
Alexandre Duret-Lutz -
Caroline Lemieux