For the purposes of comparision to traditional methods, we wish to create a buchi-automata style checker. This is primarily for comparision with the checker developped in Issue26.
Spot provides some ltl-to-buchi translation mechanisms. The documentation for the command line tool is here
http://spot.lip6.fr/userdoc/ltl2tgba.html
And the online version of the tool is here
http://spot.lip6.fr/ltl2tgba.html
However, the automata it produces accept infinite words, while we deal with finite traces. Overall, their Buchi Automata (degeneralized) are more suited for our purposes that the transition-based-generalized ones. However these translations are not completely deterministic for more complex formulae.
It may also be useful for our purposes to append exclusion conditions (stemming from our atomic proposition == event convention, e.g. G!(a&b) represents the two events cannot be simulatenous), as this reduces the number of transitions in the automata.
[Issue created by carolemieux: 2014-08-20]
For the purposes of comparision to traditional methods, we wish to create a buchi-automata style checker. This is primarily for comparision with the checker developped in Issue26.
Spot provides some ltl-to-buchi translation mechanisms. The documentation for the command line tool is here
http://spot.lip6.fr/userdoc/ltl2tgba.html
And the online version of the tool is here
http://spot.lip6.fr/ltl2tgba.html
However, the automata it produces accept infinite words, while we deal with finite traces. Overall, their Buchi Automata (degeneralized) are more suited for our purposes that the transition-based-generalized ones. However these translations are not completely deterministic for more complex formulae.
It may also be useful for our purposes to append exclusion conditions (stemming from our atomic proposition == event convention, e.g. G!(a&b) represents the two events cannot be simulatenous), as this reduces the number of transitions in the automata.
[Issue created by carolemieux: 2014-08-20]