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

We consider weighted tree automata over strong bimonoids (for short: wta). A wta A has the finite-image property if its recognized weighted tree language [A] has finite image; moreover, A has the preimage property if the preimage under [A] of each element of the underlying strong bimonoid is a recognizable tree language. For each wta A over a past-finite monotonic strong bimonoid we prove the following results. In terms of 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 A it is decidable whether 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 A has the preimage property. All our results also hold for weighted string automata. (C) 2022 Elsevier B.V. All rights reserved.