Up-To Techniques for Weighted Systems (Extended Version)

TL;DR

This paper extends up-to techniques for bisimilarity to weighted automata, introducing algorithms for congruence closure over semirings and demonstrating their effectiveness in language equivalence and inclusion problems.

Contribution

It develops novel up-to techniques for weighted systems, including a rewriting algorithm for congruence closure over semirings, with applications to weighted automata.

Findings

Rewriting algorithm for congruence closure over l-monoids

Confluence and termination of the algorithm

Improved runtime performance in weighted automata problems

Abstract

We show how up-to techniques for (bi-)similarity can be used in the setting of weighted systems. The problems we consider are language equivalence, language inclusion and the threshold problem (also known as universality problem) for weighted automata. We build a bisimulation relation on the fly and work up-to congruence and up-to similarity. This requires to determine whether a pair of vectors (over a semiring) is in the congruence closure of a given relation of vectors. This problem is considered for rings and l-monoids, for the latter we provide a rewriting algorithm and show its confluence and termination. We then explain how to apply these up-to techniques to weighted automata and provide runtime results.