Table of Contents
Fetching ...

A Nivat Theorem for Weighted Alternating Automata over Commutative Semirings

Gustav Grabolle

TL;DR

This work develops a comprehensive bridge between WAFA, WFTA, and PA by establishing a Nivat-like decomposition of WAFA via tree automata and tree homomorphisms, and by providing a logical srMSO-based characterization. It proves that WAFA languages can be realized as WFTA behaviors on images of words under word-to-tree homomorphisms, and that WAFA enjoy closure under inverses of homomorphisms but not under homomorphisms, enabling a WAFA-specific Nivat theorem. A parallel Nivat-style result for WFTA is established, alongside a logical link to weighted srMSO formulas, and a precise condition under which WFTA are closed under inverses of homomorphisms (local finiteness of the semiring). The paper also strengthens the connection to PA through reversal, showing decidability of ZERONESS and EQUALITY for rational weights, thus grounding WAFA in a spectrum of established formalisms and enabling transfer of decidability results.

Abstract

This paper connects the classes of weighted alternating finite automata (WAFA), weighted finite tree automata (WFTA), and polynomial automata (PA). First, we investigate the use of trees in the run semantics for weighted alternating automata and prove that the behavior of a weighted alternating automaton can be characterized as the composition of the behavior of a weighted finite tree automaton and a specific tree homomorphism, if weights are taken from a commutative semiring. Based on this, we give a Nivat-like characterization for weighted alternating automata. Moreover, we show that the class of series recognized by weighted alternating automata is closed under inverses of homomorphisms, but not under homomorphisms. Additionally, we give a logical characterization of weighted alternating automata, which uses weighted MSO logic for trees. Finally, we investigate the strong connection between weighted alternating automata and polynomial automata. We prove: A weighted language is recognized by a weighted alternating automaton iff its reversal in recognized by a polynomial automaton. Using the corresponding result for polynomial automata, we are able to prove that the ZERONESS problem for weighted alternating automata with weights taken from the rational numbers decidable.

A Nivat Theorem for Weighted Alternating Automata over Commutative Semirings

TL;DR

This work develops a comprehensive bridge between WAFA, WFTA, and PA by establishing a Nivat-like decomposition of WAFA via tree automata and tree homomorphisms, and by providing a logical srMSO-based characterization. It proves that WAFA languages can be realized as WFTA behaviors on images of words under word-to-tree homomorphisms, and that WAFA enjoy closure under inverses of homomorphisms but not under homomorphisms, enabling a WAFA-specific Nivat theorem. A parallel Nivat-style result for WFTA is established, alongside a logical link to weighted srMSO formulas, and a precise condition under which WFTA are closed under inverses of homomorphisms (local finiteness of the semiring). The paper also strengthens the connection to PA through reversal, showing decidability of ZERONESS and EQUALITY for rational weights, thus grounding WAFA in a spectrum of established formalisms and enabling transfer of decidability results.

Abstract

This paper connects the classes of weighted alternating finite automata (WAFA), weighted finite tree automata (WFTA), and polynomial automata (PA). First, we investigate the use of trees in the run semantics for weighted alternating automata and prove that the behavior of a weighted alternating automaton can be characterized as the composition of the behavior of a weighted finite tree automaton and a specific tree homomorphism, if weights are taken from a commutative semiring. Based on this, we give a Nivat-like characterization for weighted alternating automata. Moreover, we show that the class of series recognized by weighted alternating automata is closed under inverses of homomorphisms, but not under homomorphisms. Additionally, we give a logical characterization of weighted alternating automata, which uses weighted MSO logic for trees. Finally, we investigate the strong connection between weighted alternating automata and polynomial automata. We prove: A weighted language is recognized by a weighted alternating automaton iff its reversal in recognized by a polynomial automaton. Using the corresponding result for polynomial automata, we are able to prove that the ZERONESS problem for weighted alternating automata with weights taken from the rational numbers decidable.
Paper Structure (11 sections, 20 theorems, 42 equations, 5 figures)

This paper contains 11 sections, 20 theorems, 42 equations, 5 figures.

Key Result

Lemma 3.1

For each WAFA$\mathcal{A}$ there exists an equivalent WAFA$\mathcal{A}'$ such that (i)-(iv) hold for $\mathcal{A}'$. The construction of $\mathcal{A}'$ is effective.

Figures (5)

  • Figure 1: Representation of $\mathcal{A}$
  • Figure 2: Representation of equalized, nice $\mathcal{A}$
  • Figure 3: A non-universal WAFA
  • Figure 4: Runs of WAFA from Figure \ref{['fig:nonDetWAFA']} on $aba$
  • Figure 5: Run of translated WFTA on $t^2_{ab}$

Theorems & Definitions (41)

  • Lemma 3.1
  • proof
  • Lemma 3.2
  • proof
  • Example 3.3
  • Example 3.4
  • Theorem 3.5: KOSTOLANYI20181
  • Lemma 4.1
  • proof
  • Example 4.2
  • ...and 31 more