Finite-image property of weighted tree automata over past-finite monotonic strong bimonoids

TL;DR

This paper investigates the finite-image and preimage properties of weighted tree automata over past-finite monotonic strong bimonoids, providing characterizations and decidability results, especially for semirings, with implications for weighted string automata.

Contribution

It offers the first structural characterizations and decidability results for the finite-image property of weighted tree automata over past-finite monotonic strong bimonoids.

Findings

Finite-image property characterized by structural properties.

Decidability of the finite-image property for certain bimonoids.

Preimage property proven for all automata over these bimonoids.

Abstract

We consider weighted tree automata over strong bimonoids (for short: wta). A wta $\mathcal{A}$ has the finite-image property if its recognized weighted tree language $[\![\mathcal{A}]\!]$ has finite image; moreover, $\mathcal{A}$ has the preimage property if the preimage under $[\![\mathcal{A}]\!]$ of each element of the underlying strong bimonoid is a recognizable tree language. For each wta $\mathcal{A}$ over a past-finite monotonic strong bimonoid we prove the following results. In terms of $\mathcal{A}$'s structural properties, we characterize whether it has the finite-image property. We characterize those past-finite monotonic strong bimonoids such that for each wta $\mathcal{A}$ it is decidable whether $\mathcal{A}$ has the finite-image property. In particular, the finite-image property is decidable for wta over past-finite monotonic semirings. Moreover, we prove that $\mathcal{A}$ has the preimage property. All our results also hold for weighted string automata.