Self-verifying finite automaton

In automata theory, a self-verifying finite automaton (SVFA)
is a special kind of a nondeterministic finite automaton (NFA)
with a symmetric kind of nondeterminism
introduced by Hromkovič and Schnitger.
Generally, in self-verifying nondeterminism,
each computation path is concluded with any of the three possible answers:
"yes", "no", and "I do not know".
For each input string, no two paths
may give contradictory answers,
namely both answers "yes" and "no" on the same input are not possible.
At least one path must give answer "yes" or "no",
and if it is "yes" then the string is considered accepted.
SVFA accept the same class of languages as deterministic finite automata (DFA)
and NFA but have different state complexity.
Formal definition.
An SVFA is represented formally by a 6-tuple,
"A"=("Q", Σ, Δ, "q0", "Fa", "Fr")
such that ("Q", Σ, Δ, "q0", "Fa")
is an "NFA",
and "Fa", "Fr" are disjoint subsets of "Q".
For each word "w = a1a2 … an",
a "computation" is a sequence of states
"r0,r1, …, rn", in "Q" with the following conditions:
If rn ∈ Fa then the computation is accepting,
and if rn ∈ Fr then the computation is rejecting.
There is a requirement that for each "w"
there is at least one accepting computation
or at least one rejecting computation
but not both.
Results.
Each DFA is a SVFA, but not vice versa.
Jirásková and Pighizzini
proved that 
for every SVFA of "n" states,
there exists an equivalent DFA
of formula_1 states.
Furthermore, for each positive integer "n", there exists an "n"-state SVFA
such that the minimal equivalent DFA has exactly formula_2 states.
Other results on the state complexity of SVFA
were obtained by Jirásková and her colleagues.