This special issue of Logical Methods in Computer Science (LMCS) contains extended and revised versions of selected papers presented at the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 10-14 July 2007, Wroclaw, Poland.

LICS 2007 received 133 submissions, out of which 39 were selected for presentation at the Symposium and for publication in the proceedings. In consultation with the LICS 2007 Programme Committee, six papers presented at the Symposium were selected, and their authors invited to submit full versions to the special issue. These submissions underwent a new and thorough review process, in accordance with the usual standards of LMCS.

The issue begins with the paper, Exhaustible Sets in Higher-type Computation by Martin Escardo, which contains substantial advances in higher type computability, and solves important problems occurring at the interface of topology and computability theory. The paper develops the theory of exhaustible and searchable sets, featuring the Cantor space of infinite sequences of binary digits as a major example; it also contains a brief discussion of interesting applications of these sets.

There are two papers that study temporal logic, one over trees and the other over words. The first paper, Two-Way Unary Temporal Logic over Trees by Mikolaj Bojańczyk, considers a temporal logic EF +F^-1 for unranked, unordered finite trees. The logic has two operators: EF Φ which means "in some proper descendant Φ holds", and F^-1 Φ which means "in some proper ancestor Φ holds". Using a characterization in terms of forest algebras, the paper presents an algorithm for deciding if a regular language of unranked finite trees can be expressed in the logic.

The other temporal logic paper is First-Order and Temporal Logics for Nested Words by Rajeev Alur, Marcelo Arenas, Pablo Barcelo, Kousha Etessami, Neil Immerman and Leonid Libkin. The authors propose new temporal logics for finite and infinite nested words and prove that these logics are first-order expressively complete. They also show that first-order logic over nested words has the three-variable property, and exhibit a temporal logic for nested words which is complete for the two-variable fragment of first-order.

Another theme of the special issue is probability in concurrency theory, on which there are two papers. The first, Characterising Testing Preorders for Finite Probabilistic Processes by Yuxin Deng, Robert J. van Glabbeek, Matthew Hennessy and Carroll C. Morgan, is a contribution to probabilistic process algebra. It gives the first complete axiomatisations and alternative characterisations of the may- and must-testing preorders for finite-state probabilistic processes with silent moves, based on a probabilistic version of CSP.

The other paper on probability in concurrency theory uses games as a conceptual tool. In Game Refinement Relations and Metrics, Luca de Alfaro, Rupak Majumdar, Vishwanath Raman and Mariëlle Stoelinga investigate a version of probabilistic games played over finite state spaces for an infinite number of rounds. The authors study equivalences and metrics for these game structures, with respect to goals expressible in the quantitative modal mu- calculus. Their thesis is that the equivalence relations and metrics provide the canonical game extensions of the classical notion of bisimulation between transition systems.

The idea of game playing is yet another theme of the special issue, though it is used in a rather different way in Nikos Tzevelekos' paper, Full Abstraction for Nominal General References, which is a contribution to game semantics. His paper concerns nominal games, which are ordinary, stateful games in the style of Hyland and Ong, but cast in the theory of nominal sets developed by Pitts and Gabbay. The main result is the construction of a fully abstract semantics for a higher-order language with nominal general references.

Last but not least, we would like to thank the authors of the papers for their contributions, the members of the LICS 2007 Programme Committee and the referees for their reviews, and the managing and executive editors of LMCS for their help and guidance throughout the review process.