Equivalence of Finite-Valued Symbolic Finite Transducers

Conference paper

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

Part of the Lecture Notes in Computer Science book series (LNCS, volume 9609)
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

Abstract

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

Personalised recommendations