Verification and Synthesis of Algebraic Models – VeSyAM

Two celebrated results in the theory of automata and formal languages are the existence of polynomial-time algorithms for detecting equality of compressed strings and Angluin's procedure for learning deterministic automata with membership and equivalence queries. By now, these two classical results have a multitude of applications, ranging from data compression to automated verification. However two fundamental and closely related questions remain stubbornly open, namely whether compressed-string equality admits fast parallel algorithms (that is, whether the problem lies in the complexity class NC) and whether finite-state string-to-string transducers can be learned with polynomial query complexity.

In this proposal we take a novel approach to the above two open problems, using algebra and number theory. Specifically, we translate the problem of testing equality of compressed strings into a particular variant of circuit identity testing in the ring of cyclotomic integers, while we model string transducers as certain types of polynomial register machines. Our approach is partly inspired by recent breakthroughs in automata theory that have been achieved using algebraic techniques (such as the result of Seidl, Maneth, and Kemper, showing decidability of equivalence of deterministic top-down tree-to-string transducers). Solutions to these problems will significantly enhance the toolkit of those developing algorithms for manipulating compressed strings (e.g., in genome data bases and XML processing) as well as those working in program analysis. Our work program represents an ambitious extension of recent research of the principal investigator and her collaborators. The methodology involves a wide range of techniques, ranging from automata theory on the one hand to algebraic number theory and algebraic geometry on the other hand.