Hello,

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.

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.)

Merci,
Caroline Lemieux