Bisimulations for weighted automata over an additively idempotent semiring

We show that the methodology for deciding the existence and computation of the greatest simulations and bisimulations, developed in the framework of fuzzy automata (Ćirić et al., 2012) [13] and [14], can be applied in a similar form to weighted automata over an additively idempotent semiring. We define two types of simulations and four types of bisimulations for weighted automata over an additively idempotent semiring as solutions to particular systems of matrix inequalities, and we provide polynomial-time algorithms for deciding whether there is a simulation or bisimulation of a given type between two weighted automata, and for computing the greatest one, if it exists. The algorithms are based on the concept of relative Boolean residuation for matrices over an additively idempotent semiring, that we introduce here. We also prove that two weighted automata AA and BB are forward bisimulation equivalent, i.e., there is a row and column complete forward bisimulation between them, if and only if the factor weighted automata with respect to the greatest forward bisimulation equivalence matrices on AA and BB are isomorphic. In addition, we show that the factor weighted automaton with respect to the greatest forward bisimulation equivalence matrix on a weighted automaton AA is the unique (up to an isomorphism) minimal automaton in the class of all weighted automata which are forward bisimulation equivalent to AA.