Crisp-determinization of weighted tree automata over strong bimonoids
arXiv:1912.02660 · doi:10.46298/dmtcs.5943
Abstract
We consider weighted tree automata (wta) over strong bimonoids and their initial algebra semantics and their run semantics. There are wta for which these semantics are different; however, for bottom-up deterministic wta and for wta over semirings, the difference vanishes. A wta is crisp-deterministic if it is bottom-up deterministic and each transition is weighted by one of the unit elements of the strong bimonoid. We prove that the class of weighted tree languages recognized by crisp-deterministic wta is the same as the class of recognizable step mappings. Moreover, we investigate the following two crisp-determinization problems: for a given wta , (a) does there exist a crisp-deterministic wta which computes the initial algebra semantics of and (b) does there exist a crisp-deterministic wta which computes the run semantics of ? We show that the finiteness of the Nerode algebra of implies a positive answer for (a), and that the finite order property of implies a positive answer for (b). We show a sufficient condition which guarantees the finiteness of and a sufficient condition which guarantees the finite order property of . Also, we provide an algorithm for the construction of the crisp-deterministic wta according to (a) if is finite, and similarly for (b) if has finite order property. We prove that it is undecidable whether an arbitrary wta is crisp-determinizable. We also prove that both, the finiteness of and the finite order property of are undecidable.