On Tue, Jun 19, 2012 at 11:48 AM, Agrawal, Akshay <akshay.agrawal(a)vanderbilt.edu> wrote: Yes. Any safety formula can be translated into a TGBA without acceptance set. You should regard these just as unique strings used to name the acceptance conditions. They could be numbers, it would not change the language. When evaluating an ω-word on such an automaton, you want to see each of these strings infinitely often. The fact that they denote subformulae is an implementation detail of Spot's translation. During the translation of LTL into TGBA, the string actually denotes subformulae that have been promised to hold eventually. (The transitions that don't have Acc[φ] are the transitions that promise to see φ later/) See http://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.pdf if you want more details. However you may not rely on this second meaning, because some post-processing (like degeneralization, WDBA-minimization) might introduce Acc[1]. This Acc[1] is also used during PSL translation. Obviously it makes not sense to promise "true", since it's always true :-) If you are confused, just forget about the previous two paragraphs. Unless you want to change the translation algorithm, there is no need to know what the argument of Acc[] means. Spot does not generate C. What we call monitor (in Spot at least) is a finite automaton that accepts all finite prefixes of the executions that satisfy some formula. Spot can generate a deterministic monitor for any LTL formula, and will present it as a TGBA without acceptance condition. See the "monitor" output on the online translator. -- Alexandre Duret-Lutz