Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Equivalence of Deterministic Weighted Real-time One-Counter Automata

Prince Mathew, Vincent Penelle, Prakash Saivasan, A. V. Sreejith

TL;DR

A simpler proof and a better polynomial-time algorithm for checking the equivalence of two DWROCAs are given.

Abstract

This paper introduces deterministic weighted real-time one-counter automaton (DWROCA). A DWROCA is a deterministic real-time one-counter automaton whose transitions are assigned a weight from a field. Two DWROCAs are equivalent if every word accepted by one is accepted by the other with the same weight. DWROCA is a sub-class of weighted one-counter automata with counter-determinacy. It is known that the equivalence problem for this model is in P. This paper gives a simpler proof and a better polynomial-time algorithm for checking the equivalence of two DWROCAs.

Equivalence of Deterministic Weighted Real-time One-Counter Automata

TL;DR

A simpler proof and a better polynomial-time algorithm for checking the equivalence of two DWROCAs are given.

Abstract

This paper introduces deterministic weighted real-time one-counter automaton (DWROCA). A DWROCA is a deterministic real-time one-counter automaton whose transitions are assigned a weight from a field. Two DWROCAs are equivalent if every word accepted by one is accepted by the other with the same weight. DWROCA is a sub-class of weighted one-counter automata with counter-determinacy. It is known that the equivalence problem for this model is in P. This paper gives a simpler proof and a better polynomial-time algorithm for checking the equivalence of two DWROCAs.

Paper Structure

This paper contains 11 sections, 14 theorems, 10 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Deterministic weighted real-time one-counter automata
  5. Underlying Weighted Automata
  6. Equivalence of DWROCA
  7. Proof strategy
  8. Configuration Space
  9. Bounding the counter values in unresolved configuration pairs
  10. Conclusion and Future work

Key Result

theorem 1

Given a word $w$ and two configurations $c$ and $c^\prime$, and two sequences of interval $I$ and $J$ such that: We get that $I\uplus J$ is also a "pumping" of $w$ from both $c$ and $c^\prime$, and either $f(w_I,c) \neq f(w_I,c^\prime)$, or $f(w_J,c) \neq f(w_J,c^\prime)$ or $f(w_{I\uplus J},c) \neq f(w_{I \uplus J},c^\prime)$.

Figures (4)

  • Figure 1: Configuration space wodca.
  • Figure 2: An $\rep$ repetition.
  • Figure 3: A belt visit returning to the "initial space"
  • Figure 4: A belt visit ending in a belt

Theorems & Definitions (15)

  • theorem 1
  • definition 1
  • lemma 1
  • lemma 2
  • lemma 3
  • lemma 4: small model property
  • theorem 2
  • corollary 1
  • lemma 5
  • lemma 6
  • ...and 5 more