LICS on Monday, August 14th

Invited Talk (09:00‑10:00)
Chair: Patrice Godefroid
Location: Metropolitan A

09:00‑10:00

Orna Kupferman (Hebrew University, Israel) Avoiding Determinization [ppt] Automata on infinite objects are extensively used in system specification, verification, and synthesis. While some applications of the automata-theoretic approach have been well accepted by the industry, some have not yet been reduced to practice. Applications that involve determinization of automata on infinite words have been doomed to belong to the second category. This has to do with the intricacy of Safra's optimal determinization construction, the fact that the state space that results from determinization is awfully complex and is not amenable to optimizations and a symbolic implementation, and the fact that determinization requires the introduction of acceptance conditions that are more complex than the Buchi acceptance condition. Examples of applications that involve determinization and belong to the unfortunate second category include model checking of omega-regular properties, decidability of branching temporal logics, and synthesis and control of open systems. We offer an alternative to the standard automata-theoretic approach. The crux of our approach is avoiding determinization. Our approach goes instead via universal co-Buchi automata. Like nondeterministic automata, universal automata may have several runs on every input. Here, however, an input is accepted if all of the runs are accepting. We show how the use of universal automata simplifies significantly known complementation constructions for automata on infinite words, known decision procedures for branching temporal logics, known synthesis algorithms, and other applications that are now based on determinization. Our algorithms are less difficult to implement and have practical advantages like being amenable to optimizations and a symbolic implementation. Joint work with Moshe Vardi.

Break (10:00‑10:30)

Session 7: Temporal Logics and Automata (10:30‑12:30)
Chair: Rajeev Alur
Location: Metropolitan A

10:30‑11:00	Nir Piterman (EPFL) From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata In this paper we revisit Safra's determinization constructions. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Specifically, starting from a nondeterministic Buchi automaton with $n$ states our construction yields a deterministic parity automaton with n2n+2 states and index 2n (instead of a Rabin automaton with 12nn2n states and n pairs). Starting from a nondeterministic Streett automaton with n states and k pairs our construction yields a deterministic parity automaton with nn(k+2)+2(k+1)2n(k+1) states and index 2n(k+1) (instead of a Rabin automaton with 12n(k+1)nn(k+2)(k+1)2n(k+1) states and n(k+1) pairs). The parity condition is much simpler than the Rabin condition. In applications such as solving games and emptiness of tree automata handling the Rabin condition involves an additional multiplier of n2n! (or (n(k+1))2(n(k+1))! in the case of Streett) which is saved using our construction.
11:00‑11:30	Orna Kupferman (Hebrew University) Moshe Y. Vardi (Rice University and Microsoft Research) Memoryful Branching-Time Logic Traditional branching-time logics such as CTL* are memoryless: once a path in the computation tree is quantified at a given node, the computation that led to that node is forgotten. Recent work in planning suggests that CTL* cannot easily express temporal goals that refer to whole computations. Such goals require memoryful quantification of paths. With such a memoryful quantification, $E\psi$ holds at a node $s$ of a computation tree if there is a path $\pi$ starting at the root of the tree and going through $s$ such that $\pi$ satisfies the linear-time formula $\psi$. We define the memoryful branching-time logic mCTL* and study its expressive power and algorithmic properties. We show that mCTL* is as expressive, but exponentially more succinct, than CTL*, and that the ability of mCTL* to refer to the present is essential for this equivalence. From the algorithmic point of view, while the satisfiability problem for mCTL* is 2EXPTIME-complete --- not harder than that of CTL*, its model-checking problem is EXPSPACE-complete --- exponentially harder than that of CTL*. The upper bounds are obtained by extending the automata-theoretic approach to handle memoryful quantification, and are much more efficient than these obtained by translating mCTL* to branching logics with past. The EXPSPACE lower bound for the model-checking problem applies already to formulas of restricted form (in particular, to $AGE\xi$, which is useful for specifying possibility properties), and implies that reasoning about a memoryful branching-time logic is harder than reasoning about the linear-time logic of its path formulas.
11:30‑12:00	Nir Piterman (EPFL) Amir Pnueli (New York University) Faster Solutions of Street and Rabin Games In this paper we improve the complexity of solving Rabin and Streett games to approximately the square root of previous bounds. We introduce direct Rabin and Streett ranking that are a sound and complete way to characterize the winning sets in the respective games. By computing directly and explicitly the ranking we can solve such games in time O(mnk+1kk!) and space O(nk) for Rabin and O(nkk!) for Streett where n is the number of states, m the number of transitions, and k the number of pairs in the winning condition. In order to prove completeness of the ranking method we give a recursive fixpoint characterization of the winning regions in these games. We then show that by keeping intermediate values during the fixpoint evaluation, we can solve such games symbolically in time O(nk+1k!) and space O(nk+1k!). These results improve on the current bounds of O(mn2kk!) time in the case of direct (symbolic) solution or O(m(nk2k!)k) in the case of reduction to parity games.
12:00‑12:30	Mikolaj Bojanczyk (Warsaw University) Thomas Colcombet (Cnrs) Bounds in omega-regularity We consider an extension of omega-regular expressions where two new variants of the Kleene star L^* are added: L^B and L^S. These exponents act as the standard star, but restrict the number of iterations to be bounded (in the case of B) or to tend toward infinty (for S). These expressions can define languages that are not omega-regular. We develop a theory for these languages. We study the decidability and closure questions. We also define an equivalent automaton model extending Buchi automata. This culminates with a - partial - complementation result.

Lunch break (12:30‑14:00)

Session 8: Lambda Calculus (14:00‑16:00)
Chair: Radha Jagadeesan
Location: Metropolitan A

14:00‑14:30	Soren Lassen (Google Inc) Head normal form bisimulation for pairs and the lambda-mu calculus Boehm tree equivalence up to possibly infinite eta expansion for the pure lambda calculus can be characterized as a bisimulation equivalence. We call this co-inductive syntactic theory "extensional head normal form bisimilarity" and in this paper we extend it to the lambda-pi calculus (the lambda calculus with surjective pairing) and to two untyped variants of Parigot's lambda-mu calculus. We relate the extensional head normal form bisimulation theories for the different calculi via Fujita's extensional CPS transform into the lambda-pi calculus. We prove that extensional hnf bisimilarity is fully abstract (coincides with solvable equivalence) for the pure lambda calculus by a co-inductive reformulation of Barendregt's proof for Boehm tree equivalence up to possibly infinite eta expansion. The proof uses the so-called Boehm-out technique from Boehm's proof of the Separation Property for the lambda calculus. Moreover, we extend the full abstraction result to extensional hnf bisimilarity for the lambda-pi calculus. For the "standard" lambda-mu calculus, the Separation Property fails, as shown by David and Py, and for the same reason extensional hnf bisimilarity is not fully abstract. However, an "extended" variant of the lambda-mu calculus satisfies the Separation Property, as shown by Saurin, and we show that extensional hnf bisimilarity is fully abstract for this extended lambda-mu calculus.
14:30‑15:00	Thierry Coquand (Göteborg University) Arnaud Spiwack (ENS Cachan) Proof of strong normalisation using domain theory U. Berger significantly simplified Tait's normalisation proof for bar recursion replacing Tait's introduction of infinite terms by the construction of a domain having the property that a term is strongly normalizing if its semantics is different from the bottom element. The goal of this paper is to show that, using ideas from the theory of intersection types and Martin-Löf's domain interpretation of type theory we can in turn simplify U. Berger's argument in the construction of such a domain model. We think that our domain model can be used to give modular proofs of strong normalization for various type theory. As an example, we show in some details how it can be used to prove strong normalization for Martin-Löf dependent type theory extended with bar recursion, and with some form of proof-irrelevance.
15:00‑15:30	Giulio Manzonetto (Universita' Ca'Foscari di Venezia / PPS, Université Denis Diderot, Paris) Antonino Salibra (Universita' Ca'Foscari di Venezia) Boolean algebras for lambda calculus In this paper we show that the Stone representation theorem for Boolean algebras can be generalized to combinatory algebras. In every combinatory algebra there is a Boolean algebra of central elements (playing the role of idempotent elements in rings), whose operations are defined by suitable combinators. Central elements are used to represent any combinatory algebra as a Boolean product of directly indecomposable combinatory algebras (i.e., algebras which cannot be decomposed as the Cartesian product of two other nontrivial algebras). Central elements are also used to provide applications of the representation theorem to lambda calculus. We show that the indecomposable semantics (i.e., the semantics of lambda calculus given in terms of models of lambda calculus, which are directly indecomposable as combinatory algebras) includes the continuous, stable and strongly stable semantics, and the term models of all semisensible lambda theories. In one of the main results of the paper we show that the indecomposable semantics is equationally incomplete, and this incompleteness is as wide as possible: for every recursively enumerable lambda theory T, there is a continuum of lambda theories including T which are omitted by the indecomposable semantics.
15:30‑16:00	Makoto Tatsuta (National Institute of Informatics) Mariangiola Dezani (Universita' di Torino) Normalisation is insensible to lambda-term identity or difference This paper analyses the computational behaviour of lambda terms when applied to other lambda terms. The properties we are interested in are weak normalisation (i.e. there is a terminating reduction) and strong normalisation (i.e. all reductions are terminating). If we consider only strongly normalising lambda terms we can prove that the application of a lambda term M to a fixed number n of copies of the same arbitrary lambda term is strongly normalising if and only if the application of M to n different arbitrary lambda terms is strongly normalising. I.e. we have that MX...X (n copies) is strongly normalising for an arbitrary X if and only if MX1...Xn is strongly normalising for arbitrary X1,..,Xn. The analogous property holds when restricting to weakly normalising lambda terms. The proof for weak normalisation uses a detailed analysis on how variables are replaced inside lambda terms in normal form. For strong normalisation we consider Klop's extended lambda calculus (for which it is shown that weak normalisation is equivalent to strong normalisation) and we generalise to this calculus the analysis of variable replacements. As an application of the result on strong normalisation we show that the lambda terms whose interpretation is the top element (in the environment which associates the top element to all variables) of the Honsell-Lenisa model are exactly the lambda terms which applied to an arbitrary number of strongly normalising lambda terms produce always strongly normalising lambda terms. This proof uses a finitary logical description of the model by means of intersection types. Therefore we solve an open question stated by Dezani, Honsell and Motohama.

Break (16:00‑16:30)

Keynote Session: Marking the Gödel Centenary (16:30‑18:00)
Chair: Wolfram Schulte, Moshe Vardi
Location: Metropolitan A and B

16:30‑17:15

John Dawson (Penn State, York Campus) Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science [ppt] The publication of Gödel's incompleteness theorems, seventy-five years ago, has often been portrayed as a devastating event -- one that undermined Hilbert's program for securing the foundations of mathematics and showed the axiomatic method to be incapable of yielding all truths of arithmetic -- resulting, according to one eminent critic, in an irredeemable "loss of certainty" within mathematics. On the other hand, Gödel has also been credited with having demonstrated that the human mind is inherently superior to any computer, thereby settling once and for all the long-standing debate over mind versus mechanism. In fact, both those accounts are caricatures. Gödel's impact on modern logic, and, less directly, on computer science, has been profound; but mathematical practice has hardly been affected by the incompleteness theorems, and their philosophical significance remains a subject of debate. Nor is mathematics less "secure" than it was before Gödel's work. Indeed, his proof that the axiom of choice is consistent with the other axioms of set theory put an end to one of the most contentious foundational debates of the century.

17:15‑18:00

Dana Scott (Carnegie Mellon University) The Future of Proof [pdf] ...