A weighted automaton [1]} is a generalization of a
nondeterministic finite automaton where each transition and each state is
assigned a weight in a semiring \(K\) . We follow the definition in
[2]}. Formally, for a semiring \(K\) , a \(K\) -weighted
automaton (\(K\) -WA in short) with input alphabet \(A\)  is a pair \((X, \langle o,t\rangle )\)  where \(X\)  is a set of states, \(o: X \rightarrow K\)  is a output map and and \(t:X \rightarrow (K^X)^A\)  is the transition map. The state \(x\)  can make a transition to
state \(y\)  on input \(a \in A\)  with weight \(k \in K\)  iff \(t(x)(a)(y)=k\) . A weight
of zero means there is no transition. Note that the set of states \(X\)  may be
infinite in general. We often use \(X\)  to refer to the \(K\) -WA \((X, \langle o,t\rangle )\)  when the output and transition maps are clear from the context.
