| LCC'06 | 8th International Workshop on Logic and Computational Complexity Seattle, August 10 - 11, 2006 |
LCC on Thursday, August 10th
Welcome to LCC06 (09:25‑09:30)
Session 1: Invited Talk (09:30‑10:30)
| 09:30‑10:30 | Toniann Pitassi (Department of Computer Science, University of Toronto) TBA |
Break (10:30‑11:00)
Session 2 (11:00‑12:30)
| 11:00‑11:45 | Patrick Baillot
(LIPN, CNRS / University Paris 13) Ugo Dal Lago (Université Paris 13) Jean-Yves Moyen (LIPN -- CNRS) On Quasi-Interpretations, Blind Abstractions and Implicit Complexity Quasi-interpretations are a technique to guarantee complexity bounds on first-order functional programs: with termination orderings they give in particular a sufficient condition for a program to be executable in polynomial time, called here the P-criterion. We study properties of the programs satisfying the P-criterion, in order to better understand its intensional expressive power. Given a program on binary lists, its blind abstraction is the nondeterministic program obtained by replacing lists by their lengths (natural numbers). A program is blindly polynomial if its blind abstraction terminates in polynomial time. We show that all programs satisfying a variant of the P-criterion are in fact blindly polynomial. Then we give two extensions of the P-criterion: one by relaxing the termination ordering condition, and the other one (the bounded value property) giving a necessary and sufficient condition for a program to be polynomial time executable, with memoisation. |
| 11:45‑12:30 | Marion Jean-Yves (LORIA) Pechoux Romain (LORIA) Quasi-friendly sup-interpretations In a previous paper, the sup-interpretation method was proposed as a new tool to control memory resources of first order functional programs with pattern matching by static analysis. Basically, a sup-interpretation provides an upper bound on the size of function outputs. In this former work, a criteria, which can be applied to terminating as well as non-terminating programs, was developped in order to bound polynomially the stack frame size. In this paper, we suggest a new criteria which captures more algorithms. Since this work is related to quasi-interpretations, we compare the two notions obtaining two main features. The first one is that the problem of finding a sup-interpretation is decidable for the polynomials of bounded degree. The other one consists in the characterizations of the set of function computable in polynomial time and in polynomial space. |
Lunch break (12:30‑14:00)
Session 3 (14:00‑15:30)
| 14:00‑14:45 | Antonina Kolokolova (Simon Fraser University) Yongmei Liu (Simon Fraser University) David Mitchell (Simon Fraser University) Eugenia Ternovska (Simon Fraser University) Complexity of Expanding a Finite Structure and Related Tasks The authors of [MT05] proposed a declarative constraint programming framework based on classical logic extended with non-monotone inductive definitions. In the framework, a problem instance is a finite structure, and a problem specification is a formula defining the relationship between an instance and it's solutions. Thus, problem solving amounts to expanding a finite structure with new relations, to satisfy the formula. We present here the complexities of model expansion for a number of logics, alongside those of satisfiability and model checking. As the task is equivalent to witnessing the existential quantifiers in existential SO model checking, the paper is in large part of a survey of this area, together with some new results. In particular, we describe the combined and data complexity of FO(ID), first-order logic extended with inductive definitions [DT04] and the guarded and k-guarded logics of [ABN98] and [GLS01]. |
| 14:45‑15:30 | Murray Patterson
(Simon Fraser University) Yongmei Liu (Simon Fraser University) Eugenia Ternovska (Simon Fraser University) Arvind Gupta (Simon Fraser University) Grounding for Model Expansion in $k$-Guarded Formulas In~\cite{Mitchell/Ternovska:2005:LCC, Mitchell/Ternovska:2005:AAAI}, the authors propose a constraint programming framework based on classical logic extended with inductive definitions. They formulate a search problem as the problem of model expansion (MX), which is model checking for $\exists$SO where the goal is to find a witness for $\exists$. Their long-term goal is to produce practical tools to solve combinatorial search problems, especially those in {\bf NP}. In this framework, the problem is encoded in a logic, an instance of the problem is represented by a finite structure, and a solver generates solutions to the problem. This approach relies on propositionalisation of high-level specifications, and on the efficiency of modern SAT solvers. Here, we propose an efficient algorithm which combines grounding with partial evaluation. Since the MX framework is based on classical logic, we are able to take advantage of known results for the so-called guarded fragments. In the case of guarded formulas, the algorithm performs much better than naive grounding by relying on connections between k-guarded formulas and tree decompositions. |
Break (15:30‑16:00)
Session 4: Invited Talk (16:00‑17:00)
