Classes of NFAs which allow efficient subset testing or unambiguity conversions
here are three refs that may be helpful.


Efficient Inclusion Testing for Simple Classes of
Unambiguous $\omega$-Automata
Dimitri Isaaka, Christof Lodinga



  We show that language inclusion for languages of infinite words defined by non-
  deterministic automata can be tested in polynomial time if the automata are
  unambiguous and have simple acceptance conditions, namely safety or reachability conditions. An automaton with safety condition accepts an infinite word
  if there is a run that never visits a forbidden state, and an automaton with
  reachability condition accepts an infinite word if there is a run that visits an
  accepting state at least once.


this 2nd ref is more indirect &amp; would rely on a mapping between NFAs and tree automata.


Antichain-based
Universality and Inclusion Testing
over Nondeterministic Finite
Tree Automata
Ahmed Bouajjani, Peter Habermehl,
Luka´ˇs Hol´ık, Tayssir Touili, and
Toma´ˇs Vojnar



  We show the signiﬁcantly improved efﬁciency of this framework through a series of experiments
  with verifying various programs over dynamic linked tree-shaped data structures


the above ref also cites the following:


Antichains: A New Algorithm for Checking
Universality of Finite Automata, M. De Wulf, L. Doyen, T. A. Henzinger, and J.F. Raskin



  We show that on the difficult instances
  of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations
  of the antichain method can be used for solving the language-inclusion
  problem for nondeterministic finite automata...