This special issue of Logical Methods in Computer Science contains extended and revised versions of eight papers selected by the Guest Editors from the thirty nine presented at the 24th Annual IEEE Symposium on Logic in Computer Science (LICS 2009), which took place on 11--14 August 2009 in Los Angeles, California, USA. The submissions for the special issue underwent a new and thorough reviewing and revision process, in accordance with the usual standards of LMCS. We thank the authors and the reviewers for all their hard work producing the contents of this issue.

The article on The general vector addition system reachability problem by Presburger inductive invariants by Jerome Leroux considers the reachability problem for vector addition systems and Petri nets. The author extends the concept of semi-linear sets (of configurations) to that of semi-pseudo-linear sets. He shows that they characterize the Parikh image of the set of reachable configurations of vector addition systems. He then uses this result to show that semi-linear sets are strong enough as inductive invariants for vector addition systems. Namely, for every unreachable configuration there is a semi-linear set that is an inductive invariant of the system that excludes this configuration. This inductive invariant can provide an unreachability certificate. Such unreachability certificates provide an alternative proof to the decidability of reachability of vector addition systems.

The article on Non-deterministic Kleene coalgebras by Alexandra Silva, Marcello Bonsangue and Jan Rutten studies a generalization of regular expressions to the setting of coalgebras for so-called `non-deterministic' endofunctors on the category of sets. The authors present a generic syntax of expressions associated with each such endofunctor. They define a semantics under which every expression denotes a behaviour, that is, an element of the final coalgebra; and they give a sound and complete axiomatization of bisimilarity of expressions. The work encompasses and extends the classic results of Kleene on regular languages and deterministic finite automata and of Milner on regular behaviours and finite labelled transition systems.

The article on The complexity of global cardinality constraints by Andrei A. Bulatov and Daniel Marx describes algorithms and hardness results for a particular case of constraint satisfaction problems. The exact setting is a constraint problem with counting constraints and an additional constraint language. The result in the paper characterizes, based on certain qualities of the additional constraint language, what is the complexity of the constraint problem. It characterizes the sets of languages for which the problem is polynomial and for which the problem is NP-complete.

The article on Psi-calculi: a framework for mobile processes with nominal data and logic by Jesper Bengtson, Magnus Johansson, Joachim Parrow and Björn Victor presents a new framework for defining pi-calculus-like process calculi equipped with nominal data terms, conditions and logical assertions. The nominal data can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. The phenomena described by many existing extensions of the pi-calculus, such as the applied pi-calculus, the spi-calculus, the fusion calculus and the concurrent constraint pi-calculus, are shown to fit within the psi-calculus framework. The authors develop a notion of labelled bisimulation for psi-calculi and give fully formalized proofs of congruence and algebraic properties. The formalization is carried out using the Nominal Package of the Isabelle/HOL prover and is probably the most extensive machine-assisted formalization of process calculi to date.

The article on Model checking of continuous-time Markov chains against timed automata specifications by Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre increases the scope of algorithmic methods of analysis of continuous time Markov chains to include linear real-time specifications expressible as deterministic timed automata. The authors show that this problem can be reduced to the problem of computing reachability probabilities in piecewise deterministic Markov processes, which can be computed by solving a system of Volterra integral equations. Single-clock deterministic timed automata are shown to be amenable to standard algorithms for analysis of continuous-time Markov chains by transforming this integral equation system into a system of linear equations.

The article on Ludics with repetitions (exponentials, interactive types and completeness) by Michele Basaldella and Claudia Faggian contributes to the study of semantics for logic built on interaction. In the Ludics approach, partial proofs are interpreted as untyped strategies on a universal arena. Strategies are orthogonal if they interact appropriately, and types are biorthogonal sets of strategies. The basic Ludics framework does not provide enough tests to distinguish strategies that arise from the exponentials of linear logic, leading the authors to consider non-uniform tests that arise from the non-deterministic sum of strategies. The paper exploits this insight to extend the Ludics framework to include the exponentials of polarized linear logic.

The article on Logical step-indexed logical relations by Derek Dreyer, Amal Ahmed and Lars Birkedal concerns the use of logical relations on syntax to reason about contextual equivalence of programs. Certain programming language features (such as recursive data types, or mutable higher-order state) make it difficult to define such syntactical logical relations. The difficulty was overcome by Appel, McAllester and Ahmed's use of indexed families of relations, where the indices relate to steps of computation in the language's operational semantics. However, reasoning directly about the indices can be very tedious and error prone. Here the authors introduce a logic for binary step-indexed logical relations that sweeps most of the step-index arithmetic under the rug. A key feature of the logic is the support for recursively defined relations by means of a modal `later' operator, inspired by the work of Appel, Melliès, Richards, and Vouillon. The logic is used to develop properties of contextual equivalence for call-by-value System F extended with general recursive types.

The article on An exponential lower bound for the latest deterministic strategy iteration algorithms by Oliver Friedmann considers strategy improvement algorithms. These have been considered for many years as candidates for polynomial time algorithms for solving parity games. Alas, in this paper Oliver shows that the two most prominent approaches to strategy improvement are exponential. This is done by constructing a family of games that implement binary counters and where strategy improvements constitute increments to the counter.