Let the input HFA be called B and the program to be
checked A.  We want to make sure that A <= B
(A is a subset of B).  This is automatic when
model checking.  But how do we check that it is
a strict subset (A < B)?  For this we need to check
whether B * !A is empty or not (there is a string
in A that is not in B), but ideally we don't create
the automaton for !A because it's very expensive.

Suppose I have an input HFA B and an output HFA A.
How do I determine if there are missing behaviors?
I can generate B * !A and do a BFS search for a
final state.
