Approximations in Model Checking and Testing
Year: 2013

ion can also be used when the target structure does not follow the original source signature. In this case, some specific new predicates define the target structure and the technique has been called predicate abstraction by Graf et al. [Graf and Saidi 1997] The analysis of the small abstract structure may suffice to prove a property of the concrete model. A notion of under approximation has been used in Bounded Model Checking where paths are restricted to some finite lengths, as in section 4.1. In [Matsliah and Strichman 2007] another approach is taken, considering restrictions on some k universal inputs. A k universal circuit C with m inputs and n outputs connects to the n inputs of the model, with m n. For any assignment s of a subset of size k of the n input variables of the model, there is some assignment on the restricted m variables such that C provides an assignment on the n variables, compatible with s. The Model Checking of the new model including the circuit C may be easier than the original Model Checking as fewer input variables are considered. 3.3 Statistics based Approximation 3.3.1 Property Testing. 3.3.1.1 Generalities. Property Testing is a statistics based approximation technique to decide if either an input satisfies a given property, or is far to any input satisfying the property, using only few samples of the input. It is later used in section 4.2. The idea of moving the approximation to the input was implicit in Program Checking [Blum and Kannan 1995; Blum et al. 1993; Rubinfeld and Sudan 1996] and in PCP [Arora and Safra 1998] and explicitly studied for graph properties under the context of Property Testing [Goldreich et al. 1998] Property Testing is a part of the more general class of sublinear algorithms: given a massive input, a sublinear algorithm can approximately decide a property by sampling a tiny fraction of the input. The design of sublinear algorithms is motivated by the recent considerable growth of the size of the data that algorithms are called upon to process in everyday real time applications, for example in bioinformatics for genome decoding or in Web databases for the search of documents. Linear time, even polynomial time, algorithms were considered to be efficient for a long time, but this is no longer the case, as inputs are vastly too large to be read in their entirety. Given a distance between objects, an e tester for a property P accepts all inputs which satisfy the property and rejects with high probability all inputs which are e far from inputs that satisfies the property. Inputs which are e close to the property determine a gray area where no guarantees exists. These restrictions allow for sublinear algorithms and even O(1) time algorithms, whose complexity only depends on e. There is a strong connection between Property Testing, approximation schemes for optimization problems and learning methods. Let K be a class of finite structures with a distance dist between structures. Since property testing is an approximate notion for relative distances, we require dist to lie in [0, 1] In other words, dist is a normalized distance. For any e 0, we say that U,U K are e close if their distance is at most e. They are e far if they are not e close. In the classical setting, satisfiability is the decision problem whether U P for a structure U K and a formula P K. When P is defined by a formula F we extend this notation to F A structure U K e satisfies P or U =e P for short, if U is e close to some U K such that U P Definition 6 Property Tester [Goldreich et al. 1998] Let e 0. An e tester for a property P K is a randomized algorithm A such that, for any structure U K as input: (1) If U P then A accepts; (2) If U 6|=e P then A rejects with probability at least 2/3. 2 The constant 2/3 can be replaced by any other constant 0 g 1 by iterating O(log(1/g) the e tester and accepting iff all the executions accept ACM Journal Name, Vol. V, No. N, Month 20YY. Approximations in Model Checking and Testing 15 A query to an input structure U depends on the model for accessing the structure. For a word w, a query asks for the value of w[i] for some i. For a tree T a query asks for the value of the label of i, for some i, and potentially for the index of its parent and its j th successor, for some j. For a graph a query asks if there exists an edge between nodes i and j. We also assume that the algorithm may query the input size. The query complexity is the number of queries made to the structure. The time complexity is the usual definition, where we assume that the following operations are performed in constant time: arithmetic operations, a uniform random choice of an integer from any finite range not larger than the input size, and a query to the input. Definition 7. A property P K is testable, if there exists a randomized algorithm A such that, for every real e 0 as input, A(e) is an e tester of P whose query and time complexities depend only on e (and not on the input size) 3.3.1.2 Graphs. In the context of undirected graphs [Goldreich et al. 1998] the distance is the (normalized) edit distance on edges: the distance between two graphs on n nodes is the minimal number of edge insertions and edge deletions needed to modify one graph into the other one, divided by n. Let us consider the adjacency matrix model. Therefore, a graph G (V,E) is said to be e close to another graph G, if G is at distance at most en from G, that is if G differs from G in at most en edges. In several cases, the proof of testability of a graph property on the initial graph is based on a reduction to a graph property on constant size but random subgraphs. This was generalized for every testable graph properties by [Goldreich and Trevisan 2003] The notion of e reducibility highlights this idea. For every graph G (V,E) and integer k 1, let P denote the set of all subsets p V of size k. Denote by Gp the vertex induced subgraph of G on p. Definition 8. Let e 0 be a real, k 1 an integer, and ph, ps two graph properties. Then ph is (e, k)reducible to ps if and only if for every graph G, G ph p P, Gp ps, G 6|=e ph Pr pP [Gp 6| ps] 2/3. It is clear that reducibility implies testability using the following generic tester: Generic Test(ps, e, k) (1) Input: A graph G (V,E) (2) Generate uniformly a random subset p V of size k (3) Accept if Gp ps and reject otherwise Proposition 1. If for every e 0, there exists ke such that ph is (e, ke) reducible to ps, then the property ph is testable. Moreover, for every e 0, Generic Test(ps, e, ke) is an e tester for ph whose query and time complexities are in (ke) In fact, there is a converse of that result, and for instance we can recast the testability of c colorability [Goldreich et al. 1998; Alon and Krivelevich 2002] in terms of e reducibility. Note that this result is quite surprising since c colorability is an and NP complete problem for c 3. Theorem 3 [Alon and Krivelevich 2002] For all c 2, e 0, c colorability is (e,O((c ln c)/e))reducible to c colorability. 3.3.1.3 Words and Trees. Property testing of regular languages was first considered in [Alon et al. 2000] for the Hamming distance, and then extended to languages recognizable by bounded width read once branching programs [Newman 2002] where the Hamming distance between two words is the minimal number of character substitutions required to transform one word into the other. The (normalized) edit distance between two words (resp. trees) of size n is the minimal number of insertions, deletions and substitutions of a letter (resp. node) required to transform one word (resp. tree) into the other, divided by n. When words are infinite, the distance is defined as the superior limit of the distance of the respective prefixes.  considered the testability of regular languages on words and trees under the edit distance with moves, that considers one additional operation: Moving one arbitrary substring (resp. subtree) to another position in one step. This distance seems to be more adapted in the context of property testing, since their tester is more efficient and simpler than the one of [Alon et al. 2000] and can be generalized to tree regular languages. [Fischer et al. 2006] developed a statistical embedding of words (into `1) which has similarities with the Parikh mapping [Parikh 1966] This embedding associate to every word a sketch of constant size (for fixed e) which allows to decide any property given by some regular grammar or even some context free grammar. This embedding has other implications that we will develop further in Section 4.2.2. 3.3.1.4 Tools based on Property Testing. We have seen that Property Testing gives an approximation on the input that allows to: (1) Reduce the decision of some global properties to the decision of local properties by sampling; (2) Compress a structure to a constant size sketch on which a class of properties can be approximated. 3.3.2 Uniform Generation and Counting. In this section we describe the link between generating elements of a set S and counting the size of S. It is later used in section 4.4. Let Sn be a set of combinatorial objects of size n. There is a close connection between having an explicit formula for Sn and a uniform generator for objects in Sn. Two major approaches have been developed for counting and drawing uniformly at random combinatorial structures The Markov Chain Monte Carlo approach (see e.g. the survey [Jerrum and Sinclair 1996] and the so called recursive method, as described in [Flajolet et al. 1994] and implemented in [Thiery 2004] Although the former is more general in its applications, the latter is particularly efficient for dealing with a very large class of structures, namely those formed of atoms combined