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
|