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.