This issue of Mathematical Structures in Computer Science contains a selection of papers presented at the 17th International Workshop on Expressiveness in Concurrency (EXPRESS'10), a satellite event of CONCUR'10, held on August 30th in Paris, France.

Systems concerned with information hiding often use randomization to obfuscate the link between the observables and the information to be protected. The degree of protection provided by a system can be expressed in terms of the probability of error associated with the inference of the secret information. We consider a probabilistic process calculus to specify such systems, and we study how the operators affect the probability of error. In particular, we characterize constructs that have the property of not decreasing the degree of protection, and that can therefore be considered safe in the modular construction of these systems. As a case study, we apply these techniques to the dining cryptographers, and we derive a generalization of Chaum's strong anonymity result.

The languages accepted by finite automata are precisely the languages denoted by regular expressions. In contrast, finite automata may exhibit behaviours that cannot be described by regular expressions up to bisimilarity. In this paper, we consider extensions of the theory of regular expressions with various forms of parallel composition and study the effect on expressiveness. First we prove that adding pure interleaving to the theory of regular expressions strictly increases its expressiveness modulo bisimilarity. Then, we prove that replacing the operation for pure interleaving by ACP-style parallel composition gives a further increase in expressiveness, still insufficient, however, to facilitate the expression of all finite automata up to bisimilarity. Finally, we prove that the theory of regular expressions with ACP-style parallel composition and encapsulation is expressive enough to express all finite automata up to bisimilarity. Our results extend the expressiveness results obtained by Bergstra, Bethke and Ponse for process algebras with (the binary variant of) Kleene's star operation.

We show that the techniques for resource control that have been developed by the so-called light logics can be fruitfully applied also to process algebras. In particular, we present a restriction of higher-order π-calculus inspired by soft linear logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.

Timed and register automata are well-known models of computation over timed and data words, respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave differently in appearance, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata with one clock or register, both with non-primitive recursive complexity. This is not by chance.

This work confirms that there is indeed a tight relationship between the two models. We show that a run of a timed automaton can be simulated by a register automaton over ordered data domain, and conversely that a run of a register automaton can be simulated by a timed automaton. These are exponential time reductions hold both in the finite and infinite words settings. Our results allow to transfer decidability results back and forth between these two kinds of models, as well complexity results modulo an exponential time reduction. We justify the usefulness of these reductions by obtaining new results on register automata.

We consider models of CSP based on recording availability information, i.e. the models record what events could have been performed instead of those that were actually performed. We present many different varieties of such models. For each, we give a compositional semantics, congruent to the operational semantics, and prove full abstraction and no-junk results. We compare the expressiveness of the different models.

A well-known result by Palamidessi tells us that πmix (the π-calculus with mixed choice) is more expressive than πsep (its subset with only separate choice). The proof of this result analyses their different expressive power concerning leader election in symmetric networks. Later on, Gorla offered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of ‘incestual’ processes (mixed choices that include both enabled senders and receivers for the same channel) when running two copies in parallel. In both proofs, the role of breaking (initial) symmetries is more or less apparent. In this paper, we shed more light on this role by re-proving the above result – based on a proper formalization of what it means to break symmetries – without referring to another problem domain like leader election.

Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from πmix into πsep. We indicate how their proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential. Moreover, by abandoning the uniformity criterion, we show that there indeed is a reasonable encoding. We emphasize its underlying principle, which highlights the difference between breaking symmetries locally instead of globally.