Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
Margus Veanes, Dávid Molnár, Benjamin Livshits · 2011
Finite automata model a wide array of applications in software engineering, from regular expressions to specification languages. Finite transducers are an extension of finite automata tomodel functions on lists ofelements, which in turn haveusesinfieldsas diverseas computationallinguistics and model-based testing. Symbolic finite transducers are a furthergeneralization offinitetransducerswheretransitionsare labeled with formulas in a given background theory. Compared to classical finite transducers, symbolic transducers are far more succinct in the case of finite alphabets, because they have no need to enumerate all cases of a transition; symbolic transducers can also use theories, such as the theory of linear arithmetic over integers or reals, with infinite alphabets.