Catálogo de publicaciones - libros

In this paper we introduce a Prover-Verifier model for analyzing the computational complexity of a class of Constraint Satisfaction problems termed Binary Boolean Constraint Satisfaction problems (BBCSPs). BBCSPs represent an extremely general class of constraint satisfaction problems and find applications in a wide variety of domains including constraint programming, puzzle solving and program testing. We establish that each instance of a BBCSP admits a coin-flipping Turing Machine that halts in time polynomial in the size of the input. The prover in the Prover-Verifier model is endowed with very limited powers; in particular, it has no memory and it can only pose restricted queries to the verifier. The verifier on the other hand is both omniscient in that it is cognizant of all the problem details and insincere in that it does not have to decide on the intended proof. However, the verifier must stay consistent in its responses. Inasmuch as our provers will be memoryless and our verifiers will be asked for extremely simple certificates, our work establishes the existence of a simple, randomized algorithm for BBCSPs. Our model itself serves as a basis for the design of zero-knowledge machine learning algorithms in that the prover ends up learning the proof desired by the verifier.

cannot express the whole class of -regular languages and several extensions have been proposed. Among them, Quantified propositional Linear Temporal Logic (), proposed by Sistla, extends by quantifications over the atomic propositions. The expressive power of and its fragments have been made relatively clear by numerous researchers. However, there are few results on the expressive power of and its fragments (besides those of ). In this paper we get some initial results on the expressive power of . First, we show that both () (the fragment of in which “Until” is the only temporal operator used, without restriction on the use of quantifiers) and () (similar to (), with temporal operator “Until” replaced by “Future”) can express the whole class of -regular languages. Then we compare the expressive power of various fragments of in detail and get a panorama of the expressive power of fragments of . Finally, we consider the quantifier hierarchy of () and (), and show that one alternation of existential and universal quantifiers is necessary and sufficient to express the whole class of -regular languages.