Efficient Completion of Weighted Automata

TL;DR

This paper introduces an efficient algorithm for querying and updating weighted automata, enabling applications like termination proofs in string rewriting with performance comparable to existing methods.

Contribution

It presents a novel algorithm for efficient automaton completion and updates, applied to matchbound certificates for termination proofs.

Findings

Achieves efficient path existence and weight queries

Supports dynamic graph updates including node and edge modifications

Performs comparably to existing algorithms in termination certificate construction

Abstract

We consider directed graphs with edge labels from a semiring. We present an algorithm that allows efficient execution of queries for existence and weights of paths, and allows updates of the graph: adding nodes and edges, and changing weights of existing edges. We apply this method in the construction of matchbound certificates for automatically proving termination of string rewriting. We re-implement the decomposition/completion algorithm of Endrullis et al. (2006) in our framework, and achieve comparable performance.