2006 Editors: Vladimiro Sassone, Michele Bugliesi, Colin Stirling

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

In this paper, we first introduce a lower bound technique for the statecomplexity of transformations of automata. Namely we suggest first consideringthe class of full automata in lower bound analysis, and later reducing the sizeof the large alphabet via alphabet substitutions. Then we apply such techniqueto the complementation of nondeterministic \omega-automata, and obtain severallower bound results. Particularly, we prove an \omega((0.76n)^n) lower boundfor Büchi complementation, which also holds for almost every complementationor determinization transformation of nondeterministic omega-automata, and provean optimal (\omega(nk))^n lower bound for the complementation of generalizedBü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. Whilesatisfiability in several expressive fragments of the fully enrichedμ-calculus is known to be decidable and ExpTime-complete, it has recentlybeen proved that the full calculus is undecidable. In this paper, we study thefragments of the fully enriched μ-calculus that are obtained by dropping atleast one of the additional constructs. We show that, in all fragments obtainedin this way, satisfiability is decidable and ExpTime-complete. Thus, weidentify a family of decidable logics that are maximal (and incomparable) inexpressive power. Our results are obtained by introducing two new automatamodels, showing that their emptiness problems are ExpTime-complete, and thenreducing satisfiability in the relevant logics to these problems. The automatamodels we introduce are two-way graded alternating parity automata overinfinite trees (2GAPTs) and fully enriched automata (FEAs) over infiniteforests. The former are a common generalization of two incomparable automatamodels from the literature. The latter extend alternating automata in a similarway as the fully enriched μ-calculus extends the standard μ-calculus.

We study Recursive Concurrent Stochastic Games (RCSGs), extending our recentanalysis of recursive simple stochastic games to a concurrent setting where thetwo players choose moves simultaneously and independently at each state. Formulti-exit games, our earlier work already showed undecidability for basicquestions like termination, thus we focus on the important case of single-exitRCSGs (1-RCSGs). We first characterize the value of a 1-RCSG termination game as the leastfixed point solution of a system of nonlinear minimax functional equations, anduse it to show PSPACE decidability for the quantitative termination problem. Wethen 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-SMstrategies. Thus, such games are r-SM-determined. These results mirror andgeneralize in a strong sense the randomized memoryless determinacy results forfinite stochastic games, and extend the classic Hoffman-Karp strategyimprovement approach from the finite to an infinite state setting. The proofsin our infinite-state setting are very different however, relying on subtleanalytic 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, bygiving two reductions: first a P-time […]

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

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