On Tue, Sep 29, 2015 at 5:09 PM, Matthias Heizmann <heizmann(a)informatik.uni-freiburg.de> wrote: Sweet! From a semantic point of view, I suspect that you may have a problem because the HOA format assumes that the alphabet is 2^AP (i.e., each letter is an assignment of all atomic propositions), not AP. So the automaton you attached also accepts an infinite word where each letter is a&b, which somehow contradicts the name of the file. You did not overlook anything: Spot does not export such a feature. I'll add that to the todo list. Currently, you can still check acceptance of a word by representing this word as an automaton, and testing the interstection of the two automata using autfilt's --intersect option. If you can write your word as an LTL or PSL formula, is it even easier than writing an automaton. E.g. testing the word a&!b ; b&!a ; followed by a cycle of just a&b % ltl2tgba -f "(a & !b) & X(b & !a) & XXG(a & b)" -H | autfilt -q --intersect FinitelyManyAWithSink.hoa - && echo accepted || echo non-accepted accepted I guess you could restrict the FinitelyManyAWithSink.hoa to disallow a and b to be accepted at the same time. autfilt --exclusive-ap can be handy for that: % autfilt --exclusive-ap=a,b FinitelyManyAWithSink.hoa -H > F2.hoa Now you can evaluate words (via LTL) as if the alphabet was AP: % ltl2tgba -f "a & X(b) & XXG(b)" -H | autfilt -q --intersect F2.hoa - && echo accepted || echo non-accepted accepted % ltl2tgba -f "a & X(b) & XXG(a)" -H | autfilt -q --intersect F2.hoa - && echo accepted || echo non-accepted non-accepted (Note that --intersect is a filter. Without the -q option it returns the automata that interesect the reference automaton. If you want to compute the product of two automata to check the intersection by yourself, use --product instead.) HTH