Equivalence of Deterministic Weighted Real-time One-Counter Automata

TL;DR

This paper studies deterministic weighted real-time one-counter automata, providing a simpler proof and improved polynomial-time algorithm for their equivalence problem, which is crucial for verifying automata behavior.

Contribution

It offers a simplified proof and a more efficient algorithm for checking equivalence of DWROCA, enhancing understanding and verification of this automaton class.

Findings

Equivalence problem for DWROCA is in P

Provided a simpler proof of the problem's complexity

Developed a better polynomial-time algorithm

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.