Create Buchi Automata-Based Checker

[bestchai]

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]