Further related work.
As for regular languages, finding a minimal non-deterministic automaton
is computationally hard, namely
ExpTime-complete for non-deterministic VPA, [1]}
(hardness follows from
the universality of non-deterministic VPA [2]}).
The paper [3]} proposes an algorithm for computing
locally minimal non-deterministic VPA, relying on a reduction
to Partial Max-SAT.
Results on the state complexity of VPA with respect to determinization,
and various language operations are reported in the survey [4]}.
