LICS on Sunday, July 11th

08:45‑10:00 Opening. Finite Model Theory
Chair: Victor Vianu
Location: AT LT4
08:45 Opening
09:00 Vince Bárány, Georg Gottlob and Martin Otto
Querying the Guarded Fragment

In the areas of database theory and description logic, the problem of evaluating Booldean conjunctive queries (BCQs) over guarded first-order (GFO) theories has recently become of major interest. A Boolean conjunctive query is an existentially quantified conjunction of atoms. The problem of evaluating a BCQ q over a GFO theory T is equivalent to checking whether (T & not q) is unsatisfiable. However, given that q may not be guarded, well known results about the decidability, complexity, and finite-model property of the guarded fragment do not obviously carry over to conjunctive query answering over guarded theories, and had been left open. Our main results are the following: (i) T implies q iff T implies q over finite models; this extends the finite-model property of the garded fragment to a highly relevant larger fragment of FO, and (ii) answering BCQs over guarded theories is 2EXPTIME complete and thus not harder than consistency-checking for GFO. We also obtain interesting new results about hypergraph covers and finite model theory as described below.

We introduce a new explicit construction of finite covers of hypergraphs (guarded bisimilar covers of relational structures) such that the projection of any small configuration in the cover is tree decomposable in the base structure. The construction nontrivially extends Rosati's finite chase, for which we provide a new simplified correctness proof. Our finite covers are very compact, in fact, merely polynomial under reasonable restrictions. From this we obtain the above results and further results such as: (iii) the existence of polynomial-size conformal covers of arbitrary hypergraphs; (iv) a new proof of the finite model property of the clique-guarde fragment; (v) the small model property of the guarded fragment with optimal bounds; and finally (vi) a polynomial-time solution to the canonisation problem modulo guarded bisimulation, and hence a capturing result for the guarded bisimulation invariant fragment of PTIME in the sense of descriptive complexity.

09:30 Martin Otto
Highly Acyclic Groups, Hypergraph Covers and the Guarded Fragment

We construct finite groups whose Cayley graphs have large girth even w.r.t. a discounted distance measure that contracts arbitrarily long sequences of edges from the same colour class, and only counts transitions between colour classes. These groups are shown to be useful in the construction of finite bisimilar hypergraph covers that avoid any small acyclic configurations. We present two applications to the finite model theory of the guarded fragment.

10:30‑12:30 Type Theory
Chair: Herman Geuvers
Location: AT LT4
10:30 Vincent Siles and Hugo Herbelin
Equality is typable in Semi-Full Pure Type Systems

There are two usual ways to describe equality in a dependent typing system, one that uses an external notion of computation like beta-reduction, and one that introduces a typed judgement of beta-equality directly in the typing system.

After being open for some time, the general equivalence between both approaches has been solved by Adams for a large class of pure type systems (PTSs) called functional. In this paper, we relax the functionality constraint and prove the equivalence for all semi-full PTSs by combining the ideas of Adams with a study of the general shape of types in PTSs.

As one application, this result should eventually extend to systems with sub-typing, and bring closer the theory behind the proof assistant Coq to its implementation.

11:00 Andrei Popescu, Elsa Gunter and Chris Osborn
Strong normalization of System F by HOAS on top of FOAS

We present a point of view concerning HOAS (Higher-Order Abstract Syntax) and an extensive exercise in HOAS along this point of view. The point of view is that HOAS can be soundly and fruitfully regarded as a definitional extension on top of FOAS (First-Order Abstract Syntax). As such, HOAS is not only an encoding technique, but also a higher-order view of a first-order reality. A rich collection of concepts and proof principles is developed inside the standard mathematical universe to give technical life to this point of view. The exercise consists of a new proof of Strong Normalization for System F, formalized in the theorem prover Isabelle/HOL. HOAS makes our proof considerably more direct than previous proofs.

11:30 James Laird
Game Semantics for a Polymorphic Programming Language

A fully abstract game semantics for an idealized programming language with local state and higher rank polymorphism --- System F extended with general references --- is described. It quite concrete, and extends existing games models by a simple development of the existing question/answer labelling to represent ``copycat links'' between positive and negative occurrences of type variables, using a notion of scoping for question moves. It is effectively presentable, opening the possibility of extending existing model checking techniques to polymorphic types, for example. It is also a novel example of a model of System F with the genericity property. We prove definability of finite elements, and thus a full abstraction result, using a decomposition argument. This also establishes that terms are definable up to observational equivalence when instantiation is restricted to tuples of type variables.

12:00 Hugo Herbelin
An intuitionistic logic that proves Markov's principle

We design an intuitionistic predicate logic (in the sense of the disjunction and existence properties) that supports a limited amount of classical reasoning and proves Markov's principle (i.e. if "not not exists x A(x) implies exists A(x)" for A(x) quantifier-free and implication-free formula).

The extraction of an intuitionistic content from a classical one is done by resetting the surrounding continuation with a continuation delimiter, what can be seen as an internalization of Friedman's A-translation.

14:00‑15:00 FLoC Plenary Talks: tribute to Amir and Robin
Chair: Moshe Vardi
Location: George Square Lecture Theatre
14:00 David Harel (Weizmann Institute of Science)
Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's.
14:30 Gordon Plotkin (University of Edinburgh)
Robin Milner, a Craftsman of Tools for the Mind.
15:30‑17:00 Logic and Automata
Chair: David Harel
Location: AT LT4
15:30 Mark Jenkins, Joel Ouaknine, Alexander Rabinovich and James Worrell
Alternating Timed Automata over Bounded Time

Alternating timed automata are a powerful extension of classical Alur-Dill timed automata that are closed under all Boolean operations. They have played a key role, among others, in providing verification algorithms for prominent specification formalisms such as Metric Temporal Logic. Unfortunately, when interpreted over an infinite dense time domain (such as the reals), alternating timed automata have an undecidable language emptiness problem.

The main result of this paper is that, over bounded time domains, language emptiness for alternating timed automata is decidable (but non-elementary). The proof involves showing decidability of a class of parametric McNaughton games that are played over timed words and that have winning conditions expressed in monadic logic over the signature with order and the +1 function.

As a corollary, we establish the decidability of the time-bounded model-checking problem for Alur-Dill timed automata against specifications expressed as alternating timed automata.

16:00 Thomas Colcombet and Christof Loeding
Regular cost functions over finite trees

We develop the theory of regular cost functions over finite trees: a quantitative extension to the notion of regular languages of trees. Cost functions map each input (tree) to a value in $\omega+1$, and are considered modulo an equivalence relation which forgets about specific values, but preserves boundedness of functions on all subsets of the domain.

We introduce non-deterministic and alternating finite tree cost automata for describing cost functions. We show that all those forms of automata are effectively equivalent. We also provide decision procedures for them. Finally, following B\"uchi's seminal idea, we use the cost automata for providing decision procedures for cost monadic logic, a quantitative extension of monadic second-order logic.

16:30 Eryk Kopczynski and Anthony Widjaja To
Parikh Images of Grammars: Complexity and Applications

We consider Parikh images of languages accepted by non-deterministic finite automata and context-free grammars; in other words, we treat the languages in a commutative way --- we do not care about the order of letters in the accepted word, but rather how many times each one of them appears. In most cases we assume that the alphabet is of fixed size. We show tight complexity bounds for problems like membership, equality, and disjointness. In particular, we show polynomial algorithms for membership and disjointness in case of finite automata, and that inclusion and equality are Pi2P complete in case of context-free grammars.

17:15‑18:15 Complexity of CSP
Chair: Nicole Schweikardt
Location: AT LT4
17:15 Manuel Bodirsky, Martin Hils and Barnaby Martin
On the Scope of the Universal-Algebraic Approach to Constraint Satisfaction

The universal-algebraic approach has proved a powerful tool in the study of the computational complexity of constraint satisfaction problems (CSPs). This approach has previously been applied to the study of CSPs with finite or (infinite) omega-categorical templates. Our first result is an exact characterization of those CSPs that can be formulated with (a finite or) an omega-categorical template.

The universal-algebraic approach relies on the fact that in finite or omega-categorical structures A, a relation is primitive positive definable if and only if it is preserved by the polymorphisms of A. In this paper, we present results that can be used to study the computational complexity of CSPs with arbitrary infinite templates. Specifically, we prove that every CSP can be formulated with a template A such that a relation is primitive positive definable in A if and only if it is first-order definable on A and preserved by the infinitary polymorphisms of A.

We present applications of our general results to the description and analysis of the computational complexity of CSPs. In particular, we present a polymorphism-based description of those CSPs that are first-order definable (and therefore can be solved in polynomial-time), and give general hardness criteria based on the absence of polymorphisms that depend on more than one argument.

17:45 Marcin Kozik and Libor Barto
New conditions for Taylor varieties and CSP

We provide two new characterizations for finitely generated varieties with Taylor terms. The first characterization is using ``cyclic operations'' and the second one ``absorbing sets''. These new conditions allow us to reprove the conjecture of Bang-Jensen and Hell (proved by the authors, comp. STOC'08, SICOMP'09) and the characterization of locally finite Taylor varieties using weak near-unanimity operations (proved by McKenzie and Maroti, Alg.Univ. 2009) in an elementary and self-contained way. The research is closely connected to the algebraic approach to CSP and previous results obtained by authors using similar tools [comp. STOC'08, SICOMP'09, FOCS'09 etc.].