 |
 |
Selected Papers of the Conference ''Logic in Computer Science 2007"
2007
Editors: Andrew M Pitts, Erich Grädel, Luke Ong
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.
Guest Editors
1. Exhaustible sets in higher-type computation
We say that a set is exhaustible if it admits algorithmic universal quantification for continuous predicates in finite time, and searchable if there is an algorithm that, given any continuous predicate, either selects an element for which the predicate holds or else tells there is no example. The Cantor space of infinite sequences of binary digits is known to be searchable. Searchable sets are exhaustible, and we show that the converse also holds for sets of hereditarily total elements in the hierarchy of continuous functionals; moreover, a selection functional can be constructed uniformly from a quantification functional. We prove that searchable sets are closed under intersections with decidable sets, and under the formation of computable images and of finite and countably infinite products. This is related to the fact, established here, that exhaustible sets are topologically compact. We obtain a complete description of exhaustible total sets by developing a computational version of a topological Arzela--Ascoli type characterization of compact subsets of function spaces. We also show that, in the non-empty case, they are precisely the computable images of the Cantor space. The emphasis of this paper is on the theory of exhaustible and searchable sets, but we also briefly sketch applications.
2. Game Refinement Relations and Metrics
We consider two-player games played over finite state spaces for an infinite number of rounds. At each state, the players simultaneously choose moves; the moves determine a successor state. It is often advantageous for players to choose probability distributions over moves, rather than single moves. Given a goal, for example, reach a target state, the question of winning is thus a probabilistic one: what is the maximal probability of winning from a given state? On these game structures, two fundamental notions are those of equivalences and metrics. Given a set of winning conditions, two states are equivalent if the players can win the same games with the same probability from both states. Metrics provide a bound on the difference in the probabilities of winning across states, capturing a quantitative notion of state similarity. We introduce equivalences and metrics for two-player game structures, and we show that they characterize the difference in probability of winning games whose goals are expressed in the quantitative mu-calculus. The quantitative mu-calculus can express a large set of goals, including reachability, safety, and omega-regular properties. Thus, we claim that our relations and metrics provide the canonical extensions to games, of the classical notion of bisimulation for transition systems. We develop our results both for equivalences and metrics, which generalize bisimulation, and for asymmetrical versions, which generalize simulation.
3. Characterising Testing Preorders for Finite Probabilistic Processes
In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that have remained open throughout the years, namely to find complete axiomatisations and alternative characterisations for these preorders. This paper solves both problems for finite processes with silent moves. It characterises the may preorder in terms of simulation, and the must preorder in terms of failure simulation. It also gives a characterisation of both preorders using a modal logic. Finally it axiomatises both preorders over a probabilistic version of CSP.
4. First-Order and Temporal Logics for Nested Words
Nested words are a structured model of execution paths in procedural programs, reflecting their call and return nesting structure. Finite nested words also capture the structure of parse trees and other tree-structured data, such as XML. We provide new temporal logics for finite and infinite nested words, which are natural extensions of LTL, and prove that these logics are first-order expressively-complete. One of them is based on adding a "within" modality, evaluating a formula on a subword, to a logic CaRet previously studied in the context of verifying properties of recursive state machines (RSMs). The other logic, NWTL, is based on the notion of a summary path that uses both the linear and nesting structures. For NWTL we show that satisfiability is EXPTIME-complete, and that model-checking can be done in time polynomial in the size of the RSM model and exponential in the size of the NWTL formula (and is also EXPTIME-complete). Finally, we prove that first-order logic over nested words has the three-variable property, and we present a temporal logic for nested words which is complete for the two-variable fragment of first-order.
5. Two-Way Unary Temporal Logic over Trees
We consider a temporal logic EF+F^-1 for unranked, unordered finite trees. The logic has two operators: EF\phi, which says "in some proper descendant \phi holds", and F^-1\phi, which says "in some proper ancestor \phi holds". We present an algorithm for deciding if a regular language of unranked finite trees can be expressed in EF+F^-1. The algorithm uses a characterization expressed in terms of forest algebras.
6. Full abstraction for nominal general references
Game semantics has been used with considerable success in formulating fully abstract semantics for languages with higher-order procedures and a wide range of computational effects. Recently, nominal games have been proposed for modelling functional languages with names. These are ordinary, stateful games cast in the theory of nominal sets developed by Pitts and Gabbay. Here we take nominal games one step further, by developing a fully abstract semantics for a language with nominal general references.