2006

Editors: Wolfgang Thomas, Rajeev Alur

The paper Boundedness in Languages of Infinite Words by Mikolaj Bojanczyk and Thomas Colcombet develops the theory of languages of omega-words which extend regular languages by incorporating boundedness and unboundedness conditions for finite parts of the word.

The paper A Proof of Strong Normalization using Domain Theory by Thierry Coquand and Arnaud Spiwack, gives a very clear and greatly simplified account of semantics-based proofs of strong normalization commonly used in type theory.

The paper Independence and Concurrent Separation Logic by Jonathan Hayman and Glynn Winskel develops a true-concurrency model based on Petri nets to formalize the intuitions of independence that underlie concurrent separation logic.

The paper Coinductive Proof Principles for Stochastic Processes by Dexter Kozen gives an explicit coinduction principle for recursively-defined stochastic processes and demonstrates how it enables algebraic reasoning to replace analytic arguments.

The paper A Characterization of First-Order Constraint Satisfaction Problems by Benoit Larose, Cynthia Loten, and Claude Tardif studies algebraic and combinatorial properties of the class of constraint satisfaction problems that are definable in first-order logic.

The paper From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata by Nir Piterman presents new insights and improved upper bounds for the classical and well-studied problem of determinization of automata over in finite words.

We thank the authors for their contributions, and the reviewers for timely and valuable feedback.

Rajeev Alur, Radha Jagadeesan and Leonid Libkin

Guest Editors and LICS 2006 Acting Program Chairs

Guest Editors and LICS 2006 Acting Program Chairs

In this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization is used in numerous applications, such as reasoning about tree automata, satisfiability of CTL*, and realizability and synthesis of logical specifications. The upper bounds for all these applications are reduced by using the smaller deterministic automata produced by our construction. In addition, the parity acceptance conditions allows to use more efficient algorithms (when compared to handling Rabin or Streett acceptance conditions).

We describe simple algebraic and combinatorial characterisations of finite relational core structures admitting finitely many obstructions. 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. A slight modification of this algorithm provides, for first-order definable CSP's, a simple poly-time algorithm to produce a solution when one exists. As an application of our algebraic characterisation of first order CSP's, we describe a large family of L-complete CSP's.

We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. The rule encapsulates low-level analytic arguments, allowing reasoning about such processes at a higher algebraic level. We illustrate the use of the rule in deriving properties of a simple coin-flip process.

Ulrich Berger presented a powerful proof of strong normalisation using domains, in particular it simplifies significantly Tait's proof of strong normalisation of Spector's bar recursion. The main contribution of this paper is to show that, using ideas from intersection types and Martin-Lof's domain interpretation of type theory one can in turn simplify further U. Berger's argument. We build a domain model for an untyped programming language where U. Berger has an interpretation only for typed terms or alternatively has an interpretation for untyped terms but need an extra condition to deduce strong normalisation. As a main application, we show that Martin-Löf dependent type theory extended with a program for Spector double negation shift.

A compositional Petri net-based semantics is given to a simple language allowing pointer manipulation and parallelism. 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.

We define a new class of languages of $\omega$-words, strictly extending $\omega$-regular languages. One way to present this new class is by a type of regular expressions. The new expressions are an extension of $\omega$-regular expressions where two new variants of the Kleene star $L^*$ are added: $L^B$ and $L^S$. These new exponents are used to say that parts of the input word have bounded size, and that parts of the input can have arbitrarily large sizes, respectively. For instance, the expression $(a^Bb)^\omega$ represents the language of infinite words over the letters $a,b$ where there is a common bound on the number of consecutive letters $a$. The expression $(a^Sb)^\omega$ represents a similar language, but this time the distance between consecutive $b$'s is required to tend toward the infinite. We develop a theory for these languages, with a focus on decidability and closure. We define an equivalent automaton model, extending Büchi automata. The main technical result is a complementation lemma that works for languages where only one type of exponent---either $L^B$ or $L^S$---is used. We use the closure and decidability results to obtain partial decidability results for the logic MSOLB, a logic obtained by extending monadic second-order logic with new quantifiers that speak about the size of sets.