Seminars

Many natural computational problems, such as satisfiability and
systems of equations, can be expressed in a unified way as constraint
satisfaction problems (CSPs). In this talk I will show that the usual
reductions preserving the complexity of the constraint satisfaction
problem preserve also its proof complexity. As an application, I will
present two gap theorems, which say that CSPs that admit small size
refutations in some classical proof systems are exactly the constraint
satisfaction problems which can be solved by Datalog.

This is joint work with Albert Atserias.

As an extension of word transformations, tree transformations have numerous applications in computer science : XSLT transformations, Unix packages installation and removal, databases queries... Likewise, there are many formal models to describe these transformations. However, the proof of formal properies on these models is often difficult, or even undecidable.
In this talk, I will be interested in one of the simplest model for tree transformations, namely deterministic top-down tree transducers (DTOP). It has been known for a while that the equivalence problem of DTOPs can be solved via an earliest normal form comparison algorithm, that is in 2EXPTIME. However, when applying this algorithm to practical cases, it seemed that the worst case was not bound to happen often, if ever.
I will present a new algorithm for the problem, based on the search of counterexamples via the expansion and unification of a set of rules over states of DTOPs. The most interesting feature of this algorithm is that it runs in exponential time, thus proving that the equivalence problem of DTOPs is in fact EXPTIME-complete.

Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking.
Since then, it has been applied to many different problems. It is especially proved to be a highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both CEGAR and RECAR approaches for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered.

In database management, one of the principal task is to optimize the queries to evaluate them efficiently. It is in particular the case for recursive queries for which their evaluation can lead to crawl all the database. In particular, one of the main question is to minimize the queries in order to avoid to evaluate useless parts of the query. The core theoretical question around this line of work is the problem of inclusion of a query in another. Interestedly, this question is related to an important question in IA which is to answer a query when the data is incomplete but rules are given to derive new information. This problem is called certain query answering. In both context, if both problem are undecidable in general, there are fragments based on guardedness that are decidable due to the fact there exists witness of the problems that have a bounded tree width and that their encoding in trees is regular. Furthermore, the queries can be translated in MSO. In both contexts, Courcelle’s Theorems imply the decidability of both problems. I will present to the different results on the translation of logic class of formula for our problems into tree automata to obtain tight bounds to the problems of inclusion of recursive queries or certain query answering.

Abstract:

We show that equivalence of deterministic top-down tree-to-string transducers is decidable,
thus solving a long standing open problem in formal language theory.
We also present efficient algorithms for subclasses:
polynomial time for total transducers with unary output alphabet (over a given top-down regular domain language),
and co-randomized polynomial time for linear transducers, these results are obtained using techniques from multi-linear algebra.
For our main result, we prove that equivalence can be certified by means of inductive invariants using polynomial ideals.
This allows us to construct two semi-algorithms, one searching for a proof of equivalence, one for a witness of non-equivalence.