Minimization of Symbolic Transducers
- Olli Saarikivi ,
- Margus Veanes
Computer Aided Verification, 29th International Conference (CAV 2017) |
Published by Springer
Symbolic transducers extend classical finite state transducers to infinite or large alphabets like Unicode, and are a popular tool in areas requiring reasoning over string transformations where traditional techniques do not scale. Here we develop the theory for and an algorithm for computing quotients of such transducers under indistinguishability preserving equivalence relations over states such as bisimulation. We show that the algorithm is a minimization algorithm in the deterministic finite state case. We evaluate the benefits of the proposed algorithm over real-world stream processing computations where symbolic transducers are formed as a result of repeated compositions.