Simulations of Weighted Tree Automata

TL;DR

This paper studies simulations of weighted tree automata, showing how they can be decomposed into simpler forms and establishing conditions under which equivalent automata can be connected by finite simulation chains, aiding in decidability.

Contribution

It introduces a decomposition of weighted tree automata simulations into functional forms and proves the existence of a unifying automaton for equivalent automata in various algebraic settings.

Findings

Simulations can be decomposed into forward and backward forms.

Equivalent automata can be connected by finite chains of simulations.

Decidability of equivalence is achieved for finitely presented semirings.

Abstract

Simulations of weighted tree automata (wta) are considered. It is shown how such simulations can be decomposed into simpler functional and dual functional simulations also called forward and backward simulations. In addition, it is shown in several cases (fields, commutative rings, Noetherian semirings, semiring of natural numbers) that all equivalent wta M and N can be joined by a finite chain of simulations. More precisely, in all mentioned cases there exists a single wta that simulates both M and N. Those results immediately yield decidability of equivalence provided that the semiring is finitely (and effectively) presented.