Table of Contents
Fetching ...

Run supports and initial algebra supports of weighted automata

Manfred Droste, Heiko Vogler

TL;DR

This work investigates the question under which conditions on the strong bimonoid the support of the run semantics equals the support of the initial algebra semantics and proves a characterization of this equality in terms of strongly zero-sum-free strong bimonoids and in terms of bi-strongly zero-sum-free strong bimonoids.

Abstract

We consider weighted automata over words and over trees where the weight algebras are strong bimonoids, i.e., semirings which may lack distributivity. It is well known that, for each such weighted automaton, its run semantics and its initial algebra semantics can be different, due to the presence of nondeterminism and the absence of distributivity. Here we investigate the question under which conditions on the strong bimonoid the support of the run semantics equals the support of the initial algebra semantics. We prove a characterization of this equality in terms of strongly zero-sum-free strong bimonoids (for weighted automata over words) and in terms of bi-strongly zero-sum-free strong bimonoids (for weighted automata over trees). We also consider shortly the images of the two semantics functions.

Run supports and initial algebra supports of weighted automata

TL;DR

This work investigates the question under which conditions on the strong bimonoid the support of the run semantics equals the support of the initial algebra semantics and proves a characterization of this equality in terms of strongly zero-sum-free strong bimonoids and in terms of bi-strongly zero-sum-free strong bimonoids.

Abstract

We consider weighted automata over words and over trees where the weight algebras are strong bimonoids, i.e., semirings which may lack distributivity. It is well known that, for each such weighted automaton, its run semantics and its initial algebra semantics can be different, due to the presence of nondeterminism and the absence of distributivity. Here we investigate the question under which conditions on the strong bimonoid the support of the run semantics equals the support of the initial algebra semantics. We prove a characterization of this equality in terms of strongly zero-sum-free strong bimonoids (for weighted automata over words) and in terms of bi-strongly zero-sum-free strong bimonoids (for weighted automata over trees). We also consider shortly the images of the two semantics functions.
Paper Structure (20 sections, 19 theorems, 58 equations, 6 figures)

This paper contains 20 sections, 19 theorems, 58 equations, 6 figures.

Key Result

Lemma 4.1

drostuvog10 Let $\mathsf{B}$ be a strong bimonoid. The following two statements are equivalent:

Figures (6)

  • Figure 1: Two bounded lattices, the pentagon and the hexagon.
  • Figure 2: A tree $\xi \in \mathrm{T}_\Sigma$ and a run $\rho \in \mathrm{R}_\mathcal{A}(\xi)$ (left), and the run $\rho|_1 \in \mathrm{R}_\mathcal{A}(\xi|_1)$ induced by $\rho$ at position $w=1$ (right), fulvog22.
  • Figure 3: Some values of the form $\mathrm{h}_\mathcal{A}(\zeta)_p$ where $\mathcal{A}$ is the weighted automaton of Example \ref{['ex:A2']}, $p$ is a state of $\mathcal{A}$, and $\zeta$ is a subtree of $\xi= \sigma(\alpha,\alpha,\sigma(\alpha,\alpha,\alpha))$, i.e., $k=3$.
  • Figure 4: Runs $\rho_1$ and $\rho_2$ of $\mathcal{A}$ on $\sigma(\alpha,\alpha,\sigma(\alpha,\alpha,\alpha))$, cf. Example \ref{['ex:A2']} with $k=3$.
  • Figure 5: Tree $\xi$ with run $\rho_0$ and cut $\kappa = (11,12,13,\underline{21,22},3)$.
  • ...and 1 more figures

Theorems & Definitions (45)

  • Example 2.1
  • Example 3.1
  • Example 3.2
  • proof
  • Example 3.6
  • Example 3.7
  • proof
  • Example 3.8
  • proof
  • Example 3.9
  • ...and 35 more