Bisimulations for weighted finite automata over semirings

Abstract Simulation and bisimulation relations are powerful tools used in many areas of computer science to match moves and compare the behaviour of various computational systems, such as labelled transition systems and automata, as well as to reduce the number of states of these systems. By moving from traditional boolean systems to quantitative ones, a need arise for both simulations and bisimulations to be quantitative, to be modeled with matrices whose entries should provide some quantitative measure of the relationship between the states of the considered systems. In the present paper, we introduce several types of quantitative simulations and bisimulations for weighted finite automata over semirings. For weighted finite automata over positive semirings two tipes of simulations and two types of bisimulations are defined as solutions to particular systems of matrix inequations, while for weighted finite automata over arbitrary semirings four types of bisimulations are defined as solutions to particular systems of matrix equations. Both types of simulations are proven to ensure the containment, while all types of bisimulations are proven to ensure the equivalence of weighted finite automata. Certain general properties of simulations and bisimulations are also proved.