LICS on Sunday, August 13th

Invited Talk (09:00‑10:00)
Chair: Phokion Kolaitis
Location: Grand Ballroom C

09:00‑10:00

Andreas Blass (University of Michigan, Ann Arbor) Adapting Logics [pdf] I plan to survey some of the adaptations and variations of logic that have been introduced for various purposes. For obvious reasons, I shall concentrate mainly on purposes related to computer science and on adaptations that have played a role in my own research. Along the way, I shall touch on some open problems.

Break (10:00‑10:30)

Session 4: Logics of Programs (10:30‑12:30)
Chair: Patrice Godefroid
Location: Grand Ballroom C

10:30‑11:00	Adam Barth (Stanford University) John C. Mitchell (Stanford University) Managing Digital Rights using Linear Logic The owners of digital music players can download protected songs and licenses that convey specific rights for individual songs or groups of songs. A content player supporting Digital Rights Management (DRM) is trusted to ensure use of the songs conforms to the terms of the licenses. For licenses used in industry, we show that deciding whether a license authorizes a sequence of actions is NP-complete, with a restricted version of the problem solvable efficiently using a reduction to maximum network flow. The authorization algorithm used in industry is online, deciding which rights to exercise as actions occur, but we show that all online algorithms are necessarily \emph{non-monotonic}: each allows actions under one license that it does not allow under a more flexible license. In one approach to achieving monotonicity, we investigate approximation algorithms based on replacing each license with the closest approximation from a set of well-behaved licenses. In a second approach, we consider allowing the player to revise its past decisions about which rights to exercise while still ensuring compliance with the license. We propose an efficient algorithm based on linear logic, with linear negation used to revise past decisions. We prove our algorithm monotonic, live, and sound with respect to the semantics of licenses.
11:00‑11:30	Matthew Parkinson (School of Computing, Middlesex University) Richard Bornat (School of Computing, Middlesex University) Cristiano Calcagno (Imperial College) Variables as Resource in Hoare Logics Hoare logic is bedevilled by complex but coarse side con- ditions on the use of variables. We define a logic, free of side conditions, which permits more precise statements of a program’s use of variables. We show that it admits trans- lations of proofs in Hoare logic, thereby showing that noth- ing is lost, and also that it admits proofs of some programs outside the scope of Hoare logic. We include a treatment of reference parameters and global variables in procedure call (though not of parameter aliasing). Our work draws on ideas from separation logic: program variables are treated as resource rather than as logical variables in disguise. For clarity we exclude a treatment of the heap.
11:30‑12:00	Jonathan Hayman (University of Cambridge) Glynn Winskel (University of Cambridge) Independence and Concurrent Separation Logic A compositional Petri net based semantics is given to a simple pointer-manipulating language. The model is then applied to give a notion of validity to the judgements made by concurrent separation logic that emphasizes the process-environment duality inherent in such rely-guarantee reasoning. Soundness of the rules of concurrent separation logic with respect to this definition of validity is shown. The independence information retained by the Petri net model is then exploited to characterize the independence of parallel processes enforced by the logic. This is shown to permit a refinement operation capable of changing the granularity of atomic actions.
12:00‑12:30	Daniel Leivant (Indiana University) Matching explicit and modal reasoning about programs: a proof theoretic delineation of dynamic logic We establish two matches between programming and logic. The first is a descriptive match between programming languages L and syntactic classes F of second-order formulas, of the form: the semantics of every program P in L is explicitly definable (uniformly over all relational structures) by a formula in F; and for every formula A in F there a program in L whose termination is equivalent (uniformly in all structures) to A. In particular, we consider second-order formulas that are "computational sequential", and establish their match with Pratt's regular programs with random assignments.We also show that regular programs (without random assignments) match with computational sequential formulas that are, in addition, "definite". Our second (and by far more challenging) match is a correspondence between two approaches to reasoning about programs: modal reasoning within dynamic logics of programs, and explicit reasoning in higher-order logic. We show that Pratt-Segerberg's first-order dynamic logic DL for regular programsproves precisely those properties of regular programs that are provable in second-order logic with set-existence restricted to computational formulas that are both definite and sequential, that is, for those formulas we show to correspond descriptively to such programs. The extension of DL to regular programs with random assignments matches set-existence for sequential formulas.

Lunch break (12:30‑14:00)

Session 5: Proof Theory (14:00‑15:30)
Chair: Christel Baier
Location: Grand Ballroom C

14:00‑14:30	Ugo Dal Lago (Université Paris 13) Context Semantics, Linear Logic and Computational Complexity We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in linear logic. In particular, context semantics lets us define the weight of a proof-net as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the number of rewriting steps to normal form (for certain reduction strategies). Weights are then exploited in proving strong soundness theorems for various subsystems of linear logic, namely elementary linear logic, soft linear logic and light affine logic.
14:30‑15:00	Olivier Laurent (CNRS - Universite Paris 7) Lorenzo Tortora de Falco (Universita Roma Tre) Obsessional cliques: a semantic characterization of bounded time complexity We give a semantic characterization of bounded complexity proofs. We introduce the notion of obsessional clique in the relational model of linear logic and show that restricting the morphisms of the category REL to obsessional cliques yields models of ELL and SLL. Conversely, we prove that these models are relatively complete: an LL proof whose interpretation is an obsessional clique is always an ELL/SLL proof. These results are achieved by introducing a system of ELL/SLL untyped proof-nets, which is both correct and complete with respect to elementary/polynomial time complexity.
15:00‑15:30	Alexis Maciel (Clarkson University) Toniann Pitassi (University of Toronto) A Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives It is known that constant-depth Frege proofs of some tautologies require exponential size. No such lower bound result is known for more general proof systems. We consider Sequent Calculus proofs in which formulas can contain modular connectives and only the cut formulas are restricted to be of constant depth. Under a plausible hardness assumption concerning small-depth Boolean circuits, we prove an exponential lower bound for such proofs. We prove this lower bound directly from the computational hardness assumption. By using the same approach, we obtain the following additional results. We provide a much simpler proof of a known (unconditional) lower bound in the case where only conjunctions and disjunctions are allowed. We establish a conditional exponential separation between the power of constant-depth proofs that use different modular connectives. Finally, under a plausible hardness assumption concerning the polynomial-time hierarchy, we show that the hierarchy Gi* of quantified propositional proof systems does not collapse.

Break (15:30‑16:00)

Session 6: Model Theory (16:00‑18:00)
Chair: Moshe Vardi
Location: Grand Ballroom C

16:00‑16:30	Benoit Larose (Concordia University) Cynthia Loten (Royal Military College of Canada) Claude Tardif (Royal Military College of Canada) A Characterisation of First-Order Constraint Satisfaction Problems We characterise finite relational core structures admitting finitely many obstructions, in terms of special near-unanimity functions, and in terms of dismantling properties of their square. As a consequence, we show that it is decidable to determine whether a constraint satisfaction problem is first-order definable: we show the general problem to be NP-complete, and give a polynomial time algorithm in the case of cores.
16:30‑17:00	Laura Chaubard (LIAFA, University Paris VII and CNRS) Jean-Eric Pin (LIAFA, CNRS and University Paris 7) Howard Straubing (Boston College) First order formulas with modular predicates Let A be a finite alphabet. We view a word w over A as a relational structure whose universe is {0,1,...,|w|-1}, with the usual order relation < on the universe, and, for each a in A, a unary relation a where a(x) is interpreted to mean "the letter in position x is a." A first-order sentence using these relation symbols consequently defines a language over A. It is known (McNaughton and Papert, 1971) that the first-order definable languages are precisely the star-free regular languages over A. We denote this family of languages by FO[<]. There is a semigroup-theoretic method for deciding membership of a language in FO[<] (Schutzenberger, 1965). The decision problem for the levels of the hierarchy within FO[<] based on quantifier alternation is largely open, apart from some results (most of them quite difficult) concerning the first few levels. Let us adjoin to our language unary predicate symbols MODr,d and Dr,d, where 0 <= rr,dx is interpreted to mean that x is congruent to r modulo d, and Dr,d to mean that the length of the string is congruent to r modulo d. We denote the family of languages over A* definable in this extended logic by FO(<+MOD). This is precisely the family of regular languages in the circuit complexity class AC0, and once again, membership is decidable by a semigroup-theoretic criterion (Barrington, Compton, Straubing and Therien, 1992). In the present paper, we study the decision problem for the levels of the hierarchy in FO[<+MOD] based on quantifier alternation. Our main results are that membership in Sigma1[<+MOD], the family of languages definable by Sigma1 sentences, as well as membership in the boolean closure BSigma1[<+MOD]$ of this family, are both decidable. For the first of these families, we obtain a simple criterion based on the minimal automaton of the language. However for the second problem, both the formulation of the criterion and its proof require sophisticated methods of finite semigroup theory.
17:00‑17:30	Emil Kiss (Eotvos University) Matthew Valeriote (McMaster University) On tractability and congruence distributivity Bulatov, Jeavons, and Krohkin have shown how to associate a finite algebra A(G) with a given constraint language G so that the tractability of G is reflected in the algebra A(G). They conjecture that G is tractable if and only if the algebra A(G) has a term operation that satisfies some rather weak equations. The constraint languages G with the property that the collection of instances in CSP(G) that fail to have a solution is definable in Datalog form an important class. Equivalently, they are the languages that exhibit a certain type of local consistency property. Larose and Zadori have conjectured that this property of a constraint language G is equivalent to the existence of special term operations of the algebra A(G) that force the local structure of A(G) to be rather simple. One version of local consistency, developed by Bulatov and Jeavons, and known as bounded relational width, has a definite algebraic flavour that we exploit to establish the tractability of certain types of constraint languages. Our result provides some partial support for the Larose-Zadori conjecture by showing that if G is any constraint language whose associated algebra A(G) has a short sequence of terms that imply congruence distributivity, then G is of bounded relational width and hence is tractable. More precisely, we show that if A(G) has two term operations p(x,y,z) and q(x,y,z) that satisfy the equations: p(x,y,x) = p(x,x,y) = q(x,y,x) = q(y,y,x) = x, p(x,y,y) = q(x,y,y) then the relational clone generated by G, considered as a constraint language, has bounded relational width and hence is tractable.
17:30‑18:00	Lutz Schröder (Dept. of Comput. Sci., University of Bremen, and DFKI-Lab Bremen) Dirk Pattinson (Department of Computer Science, University of Leicester) PSPACE bounds for rank-1 modal logics For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatization, in PSPACE. This leads not only to a unified derivation of (known) tight PSPACE-bounds for a number of logics including K, coalition logic, and graded modal logic (and to a new algorithm in the latter case), but also to a previously unknown tight PSPACE-bound for probabilistic modal logic, with rational probabilities coded in binary. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.

LICS-SAT-RTA Joint Banquet (19:00‑22:00)
Location: Grand Ballroom B