Selected Papers of the Conference ''Logic in Computer Science 2006''


Editors: Wolfgang Thomas, Rajeev Alur

This special issue of Logical Methods in Computer Science is devoted to papers selected from the 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006). The meeting took place in Seattle, USA from August 12 to 15, 2006. The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic in a broad sense. The papers presented at the meeting spanned diverse topics such as nite model theory, formal verification, and type theory. This diversity is also reected in the six papers that we selected for the special issue.

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

1. From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata

Piterman, Nir.
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 […]

2. A Characterisation of First-Order Constraint Satisfaction Problems

Larose, Benoit ; Loten, Cynthia ; Tardif, Claude.
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 […]

3. Coinductive Proof Principles for Stochastic Processes

Kozen, Dexter.
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 […]

4. A proof of strong normalisation using domain theory

Coquand, Thierry ; Spiwack, Arnaud.
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 […]

5. Independence and concurrent separation logic

Hayman, Jonathan ; Winskel, Glynn.
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 […]