This issue of Logical Methods in Computer Science contains six of the best contributions to track B of the 33rd edition of the "International Colloquium on Automata, Languages and Programming," ICALP 2006, held in Venice, Italy on 10-14 July 2006.

ICALP is a series of annual conferences organised by the European Association for Theoretical Computer Science (EATCS), whose first edition took place in 1972. In 2006, the ICALP programme run three parallel tracks: A, focusing on algorithms, automata, complexity and games (chaired by the late I. Wegener); B, focusing on logic, semantics and theory of programming (chaired by V. Sassone); and C, focusing on security and cryptography foundation (chaired by B. Preneel). In response to the call for papers, the Program Committee received 403 submissions, out of which 109 papers were selected for inclusion in the scientific program: 61 papers for Track A, 24 for Track B and 24 for Track C. The proceedings have appeared in Springer-Verlag's Lecture Notes in Computer Science as vol. 4051 and 4052.

We wish to thank the authors who submitted their papers to ICALP and to this special issue, the members of the Program Committee for their scholarly effort, and the referees who assisted in the evaluation process. Warm thanks go to the referees of the selected articles that appear in this volume, who have contributed a very substantial and valuable effort. They are: Krishnendu Chatterjee, Daniel Dantas, Olivier Finkel, Blaise Genest, Hugo Gimbert, Aad Mathijssen, Vincent Padovani, Julian Rathke, Sylvain Salvati, Nicole Schweikardt, Manfred Schmidt-Schauss, Peter Selinger, Victor Selivanov, Olivier Serre, Richard Statman, David Walker and Igor Walukiewicz.

We hope you will enjoy the volume.

An invitation to read

This collection of selected papers provides an excellent sample of the gamut of research topics ICALP (Track B) has to offer. We will give below a brief synopsis of each of them, as an invitation to the casual reader to read on.

The Complexity of Enriched Mu-Calculi,
Piero A. Bonatti, Carsten Lutz, Aniello Murano and Moshe Y. Vardi
The paper investigates the satisfiability problem in the full graded and in the hybrid graded extensions of the mu-calculus, which include inverse programs, nominals and graded modalities. Together with previous work in the literature, the results in this paper complete the picture of the satisfiability problem of the family of the maximal fragments of the fully enriched mu-calculus, showing that for both the considered extensions satisfiability is in EXPTIME. The authors achieve this by an automata-theoretic approach, reducing satisfiability in the extended mu-calculi to an emptyness test in two newly introduced automata models.

Recursive Concurrent Stochastic Games,
Kousha Etessami and Mihalis Yannakakis
The paper extends the authors' previous work on recursive stochastic games to a concurrent setting, focussing on the notion of (single-exit) recursive textit{concurrent} stochastic game. Such games are characterised by the fact that at each state the players choose their respective moves simultaneously and independently. The authors provide a strategy improvement technique which generalises the randomised memoryless determinacy results for finite stochastic games. Furthermore, they study both the quantitative and the qualitative (i.e., with probability 1) termination problems, and prove these are PSPACE decidable. By reduction to and from the long-standing problem of the square-root sum, the authors argue that to improve such an upper bound is hard and would require a major breakthrough.

Lambda-RBAC: Programming with Role-Based Access Control,
Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, James Riely
This paper introduces a lambda calculus enriched with primitives for access control, predicated on a lattice of roles. Key operations of the calculus concern the modulation of `rights,' including both the safe 'rights weakening' and the potentially dangerous 'rights amplification.' The authors demonstrate the expressiveness of their calculus via a series of small examples and by programming a variety of role combinators. The paper's main contribution is the development of two typing system, one to remove unnecessary roles checks for principals at sufficiently high roles, the second to track the maximal role required by a fragment of code.

The Wadge Hierarchy of Deterministic Tree Languages,
Filip Murlak
Wedge reducibility is an ordering relation that measures the complexity of omega-regular languages, organising them in what has become known as the Wedge hierarchy. The paper studies the Wadge reducibility problem for languages of (regular) infinite trees, giving a complete characterisation of the structure of Wadge reducibility on the class of deterministic tree languages, thus providing the generalisation of the Wagner hierarchy of regular omega-languages. The author develops his characterissation by first introducing the family canonical deterministic tree automata, describing the structure of Wadge reducibility on the canonical languages, and then proving that any deterministic tree language is Wadge equivalent to a unique canonical automata in the family.

Decidability of Higher-Order Matching,
Colin Stirling
The author tackles and answers in the positive the 30-years standing problem of whether higher-order matching in the lambda-calculus is decidable. Namely, the problem is whether lambda term t can be pattern-matched (up to βη-equivalence) to a closed term u. The proof presented here builds on previous attempts by reducing matching to the (dual) interpolation problem, but then it departs completely from the related literature by using an original game-theoretic argument partly inspired by model-checking games.

Lower Bounds for Complementation of ω-Automata via the full Automata Technique, Qiqi Yan
The standard approach to lower bound proofs in automata constructions is to first find a particular class of automata and then prove that transforming the class requires a large state blow-up. Identifying such automata class is usually difficult, and represents the main obstacle for the proof of lower bound results. This paper proposes a new and effective solution to this difficulty, by providing a generic family of hard automata, called full automata, that basically allows to generate any aytomaton, by embedding. The author illustrates the effectiveness of his technique on various types of nondeterministic infinite-word automata, by providing new lower bounds for complementation and determinization of various types of Büchi automata.