Efficient Completion of Weighted Automata

Johannes Waldmann

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.

In Andrea Corradini and Hans Zantema: Proceedings 9th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2016), Eindhoven, The Netherlands, April 8, 2016, Electronic Proceedings in Theoretical Computer Science 225, pp. 55–62.
Published: 10th September 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.225.8 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org