[Spot] Nondeterministic behavior of ltl2tgba tool

Tomáš Babiak xbabiak at fi.muni.cz
Sat Aug 13 21:09:27 CEST 2011


Dear SPOT developers,

I am doing a research on translation of LTL to BA and I am using the tool 
"ltl2tgba" included in the SPOT 0.7.1 distribution as a reference.
While comparing "ltl2tgba" to some other translations using the "lbtt" tool, I 
have noticed that it sometimes produces different results (regarding the size of 
produced automata) without changing any parameters. It appers that for some 
formulae it nondeterministicaly produces different automata. I attach an example 
when "ltl2tgba" was executed four times in the row always producing a different 
automaton. First three automata differs only by the names of states or the 
ordering of transitions, while the last automaton has one state less than the 
others. However, all automata seam to be correct and mutually equivalent.
After a closer examination, it seams that this behavior is caused be the -r7 
option enabling tau03 formula reductions. Similar behavior can be observed using 
-r5 or -r6 options as well. The question is whether such a nondeterminstic 
behavior is expected while using language containment formula reductions or it 
is caused by an implementation bug.

Thank you for your help.

Best regards,
Tomas Babiak
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: ltl2tgba-nondeterminism
Url: https://www.lrde.epita.fr/pipermail/spot/attachments/20110813/1c63fa43/attachment.txt 


More information about the Spot mailing list