APPROXIMATE SATISFIABILITY AND EQUIVALENCE

作者：Fischer Eldar^*; Magniez Frederic; de Rougemont Michel

来源：SIAM Journal on Computing, 2010, 39(6): 2251-2281.

DOI：10.1137/070703776

• equivalence testing
• approximation
• automata

Inspired by property testing, for every epsilon > 0 we relax the classical satisfiability U |= F between a finite structure U of a class K and a formula F, to a notion of epsilon-satisfiability U |=(epsilon) F, and relax the classical equivalence F-1 F-2 between two formulas F-1 and F-2 to epsilon-equivalence F-1 =(epsilon) F-2. We consider strings and trees with the norm of the edit distance with moves, and show that, unlike their exact counterparts, these approximate notions can be efficiently decided. We use a statistical embedding of words (resp., trees) into l(1), which generalizes the original Parikh mapping, obtained by sampling O(f(epsilon)) finite samples of the words (resp., trees). We give a tester for equality and membership in any regular language, in time independent of the size of the structure. Using our geometrical embedding, we can also test the equivalence between two regular properties over words, defined by regular expressions or monadic second-order formulas. Our equivalence tester has polynomial time complexity in the size of the automaton (or regular expression), for any fixed epsilon, whereas the exact version of the equivalence problem is PSPACE-complete. We also prove versions of some of these results for trees, but with worse time complexity. Last, we extend the geometric embedding, and hence the testing algorithms, to infinite regular languages and to context-free languages. For context-free languages, the equivalence tester has an exponential time complexity for any fixed epsilon, whereas the exact version is not even decidable.

• 出版日期2010