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.

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.