probabilistic automaton
nondeterministic automaton