On Tue, Jun 19, 2012 at 11:48 AM, Agrawal, Akshay akshay.agrawal@vanderbilt.edu wrote:

Dear Alexandre, Thank you for a prompt reply. So I think my perception was wrong about TGBA. I did not learn about TGBA from SPOT's wiki. I learnt it from some papers and Wikipedia. But I think I formed a wrong impression. So after your explanation I believe that a TGBA for G(p->Xr) is a special case of TGBA with all transitions as accepting transitions??

Yes. Any safety formula can be translated into a TGBA without acceptance set.

Also, there was a need for me to convert these TGBA generated from SPOT to C code so I wanted to know how is Acc[r] logically read?? Because sometimes in complex TGBA's there are various such accepting sets where we may have Acc[r] and Acc[r|q] or something. So the Boolean condition in the brackets of Acc[] , how is it read/what does it exactly mean?? I think this will help me to get C code out of these TGBAs.

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.

Does SPOT give a C code or other type of executable monitor type code for generated TGBAs??

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.