International Andrei Ershov Memorial Conference on Perspectives of System Informatics

PSI 2015: Perspectives of System Informatics pp 276-290

Equivalence of Finite-Valued Symbolic Finite Transducers

Conference paper

DOI: 10.1007/978-3-319-41579-6_21

Volume 9609 of the book series Lecture Notes in Computer Science (LNCS)
Cite this paper as:
Veanes M., Bjørner N. (2016) Equivalence of Finite-Valued Symbolic Finite Transducers. In: Mazzara M., Voronkov A. (eds) Perspectives of System Informatics. PSI 2015. Lecture Notes in Computer Science, vol 9609. Springer, Cham


Symbolic Finite Transducers, or SFTs, is a representation of finite transducers that annotates transitions with logical formulas to denote sets of concrete transitions. This representation has practical advantages in applications for web security analysis, where it provides ways to succinctly represent web sanitizers that operate on large alphabets. More importantly, the representation is also conducive for efficient analysis using state-of-the-art theorem proving techniques. Equivalence checking plays a central role in deciding properties of SFTs such as idempotence and commutativity. We show that equivalence of finite-valued SFTs is decidable, i.e., when the number of possible outputs for a given input is bounded by a constant.

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Microsoft ResearchRedmondUSA