Simulations and bisimulations for max-plus automata

Two types of simulations and four types of bisimulations for weighted finite automata over the complete max-plus semiring we define as solutions of particular systems of matrix inequations. We provide a procedure that either decides that there is a simulation or bisimulation of a given type between two automata, and outputs the greatest one, or decides that no simulation or bisimulation of that type exists. The procedure is iterative and does not have to end in a finite number of steps. Certain conditions under which this procedure must terminate in a finite number of steps are described in a slightly more general context in Stamenković et al. (Discrete Event Dynamic Systems, 32:1–25, 2022). We also propose a modification of this procedure which, in case there is no simulation or bisimulation of a given type between two max-plus automata, detects this in finitely many steps and faster than the original procedure. In the same case, that modification also finds a natural number such that containment or equivalence is valid for all input words of length less than that number. For max-plus automata with non-negative weights, we point out the differences that occur when the above mentioned procedure is applied over the complete max-plus semiring, and when it is applied over its non-negative part with minus infinity added.