implement simulation-based inclusion checks
- compute the signatures and classes of the states of both automata,
- if the initial state of A is a class implied by the class of B, then L(B) is included in L(A).
That only a sufficient condition, but it may help us avoid computing the complement of A to decide B ⊂ A