loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
Approximate Satisfiability and Equivalence
Seattle, Washington
August 12-August 15
ISBN: 0-7695-2631-4
Eldar Fischer, Technion, Israel
Frederic Magniez, Universite Paris-Sud, France
Michel de Rougemont, Universite Paris II, France
Inspired by Property Testing, we relax the classical satisfiability U |= F between a finite structure U of a class K and a formula F, to a notion of \varessilon-satisfiability U |=\varepsilon F, and the classical equivalence F_1 \equiv F_2 between two formulas F_1 and F_2, to \varepsilon-equivalence F1 \equiv_\varepsilon F2 for \varepsilon > 0. We consider the class of strings and trees with the edit distance with moves, and show that 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 on words, defined by Monadic Second Order formulas. Our equivalence tester has polynomial time complexity in the size of the automaton (or regular expression), for a fixed varepisolon, whereas the exact version of the equivalence problem is PSPACE-complete.

Last, we extend the geometric embedding, and hence the tester algorithms, to infinite regular languages and to context-free languages. For context-free languages, the equivalence tester has an exponential time complexity, whereas the exact version is undecidable.

% MathType!MTEF!2!1!+- % feaafiart1ev1aaatCvAUfeBSjuyZL2yd9gzLbvyNv2CaerbuLwBLn % hiov2DGi1BTfMBaeXatLxBI9gBaerbd9wDYLwzYbItLDharqqtubsr % 4rNCHbGeaGqiVu0Je9sqqrpepC0xbbL8F4rqqrFfpeea0xe9Lq-Jc9 % vqaqpepm0xbba9pwe9Q8fs0-yqaqpepae9pg0FirpepeKkFr0xfr-x % fr-xb9adbaqaaeGaciGaaiaabeqaamaabaabaaGcbaGaeyyyIOlaaa!37B6! \[ \equiv \]
Citation:
Eldar Fischer, Frederic Magniez, Michel de Rougemont, "Approximate Satisfiability and Equivalence," lics, pp.421-430, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.