2006

Editors: Vladimiro Sassone, Michele Bugliesi, Colin Stirling

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.

Michele Bugliesi and Vladimiro Sassone

Guest editors and ICALP 2006 Conference chairs, resp., Programme chair

**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.

Michele Bugliesi and Vladimiro Sassone

Guest editors and ICALP 2006 Conference chairs, resp., Programme chair

Guest editors and ICALP 2006 Conference chairs, resp., Programme chair

We study mechanisms that permit program components to express role constraints on clients, focusing on programmatic security mechanisms, which permit access controls to be expressed, in situ, as part of the code realizing basic functionality. In this setting, two questions immediately arise: (1) The user of a component faces the issue of safety: is a particular role sufficient to use the component? (2) The component designer faces the dual issue of protection: is a particular role demanded in all execution paths of the component? We provide a formal calculus and static analysis to answer both questions.

In this paper, we first introduce a lower bound technique for the state complexity of transformations of automata. Namely we suggest first considering the class of full automata in lower bound analysis, and later reducing the size of the large alphabet via alphabet substitutions. Then we apply such technique to the complementation of nondeterministic \omega-automata, and obtain several lower bound results. Particularly, we prove an \omega((0.76n)^n) lower bound for Büchi complementation, which also holds for almost every complementation or determinization transformation of nondeterministic omega-automata, and prove an optimal (\omega(nk))^n lower bound for the complementation of generalized Büchi automata, which holds for Streett automata as well.

The fully enriched μ-calculus is the extension of the propositional μ-calculus with inverse programs, graded modalities, and nominals. While satisfiability in several expressive fragments of the fully enriched μ-calculus is known to be decidable and ExpTime-complete, it has recently been proved that the full calculus is undecidable. In this paper, we study the fragments of the fully enriched μ-calculus that are obtained by dropping at least one of the additional constructs. We show that, in all fragments obtained in this way, satisfiability is decidable and ExpTime-complete. Thus, we identify a family of decidable logics that are maximal (and incomparable) in expressive power. Our results are obtained by introducing two new automata models, showing that their emptiness problems are ExpTime-complete, and then reducing satisfiability in the relevant logics to these problems. The automata models we introduce are two-way graded alternating parity automata over infinite trees (2GAPTs) and fully enriched automata (FEAs) over infinite forests. The former are a common generalization of two incomparable automata models from the literature. The latter extend alternating automata in a similar way as the fully enriched μ-calculus extends the standard μ-calculus.

We study Recursive Concurrent Stochastic Games (RCSGs), extending our recent analysis of recursive simple stochastic games to a concurrent setting where the two players choose moves simultaneously and independently at each state. For multi-exit games, our earlier work already showed undecidability for basic questions like termination, thus we focus on the important case of single-exit RCSGs (1-RCSGs). We first characterize the value of a 1-RCSG termination game as the least fixed point solution of a system of nonlinear minimax functional equations, and use it to show PSPACE decidability for the quantitative termination problem. We then give a strategy improvement technique, which we use to show that player 1 (maximizer) has \epsilon-optimal randomized Stackless & Memoryless (r-SM) strategies for all \epsilon > 0, while player 2 (minimizer) has optimal r-SM strategies. Thus, such games are r-SM-determined. These results mirror and generalize in a strong sense the randomized memoryless determinacy results for finite stochastic games, and extend the classic Hoffman-Karp strategy improvement approach from the finite to an infinite state setting. The proofs in our infinite-state setting are very different however, relying on subtle analytic properties of certain power series that arise from studying 1-RCSGs. We show that our upper bounds, even for qualitative (probability 1) termination, can not be improved, even to NP, without a major breakthrough, by giving two […]

We provide a complete description of the Wadge hierarchy for deterministically recognisable sets of infinite trees. In particular we give an elementary procedure to decide if one deterministic tree language is continuously reducible to another. This extends Wagner's results on the hierarchy of omega-regular languages of words to the case of trees.

We show that the higher-order matching problem is decidable using a game-theoretic argument.