 |
 |
Selected Papers of the Conference ''Logic in Computer Science 2009''
2009
Editors: Nir Piterman, Andrew M Pitts, Radha Jagadeesan
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.
Guest Editors
1. The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known to be decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. This decomposition is used in this paper to prove that the Parikh images of languages recognized by VASs are semi-pseudo-linear; a class that extends the semi-linear sets, a.k.a. the sets definable in Presburger arithmetic. We provide an application of this result; we prove that a final configuration is not reachable from an initial one if and only if there exists a semi-linear inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes an inductive invariant, we deduce that there exist checkable certificates of non-reachability. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas.
2. Non-Deterministic Kleene Coalgebras
In this paper, we present a systematic way of deriving (1) languages of (generalised) regular expressions, and (2) sound and complete axiomatizations thereof, for a wide variety of systems. This generalizes both the results of Kleene (on regular languages and deterministic finite automata) and Milner (on regular behaviours and finite labelled transition systems), and includes many other systems such as Mealy and Moore machines.
3. The complexity of global cardinality constraints
In a constraint satisfaction problem (CSP) the goal is to find an assignment of a given set of variables subject to specified constraints. A global cardinality constraint is an additional requirement that prescribes how many variables must be assigned a certain value. We study the complexity of the problem CCSP(G), the constraint satisfaction problem with global cardinality constraints that allows only relations from the set G. The main result of this paper characterizes sets G that give rise to problems solvable in polynomial time, and states that the remaining such problems are NP-complete.
4. Psi-calculi: a framework for mobile processes with nominal data and logic
The framework of psi-calculi extends the pi-calculus with nominal datatypes for data structures and for logical assertions and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Psi-calculi can capture the same phenomena as other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, the concurrent constraint pi-calculus, and calculi with polyadic communication channels or pattern matching. Psi-calculi can be even more general, for example by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions. We provide ample comparisons to related calculi and discuss a few significant applications. Our labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. We establish minimal requirements on the nominal data and logic in order to prove general algebraic properties of psi-calculi, all of which have been checked in the interactive theorem prover Isabelle. Expressiveness of psi-calculi significantly exceeds that of other formalisms, while the purity of the semantics is on par with the original pi-calculus.
5. Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C that are accepted by A, i.e., the likelihood that C satisfies A? It is shown that under finite acceptance criteria this equals the reachability probability in a finite piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability of terminal strongly connected components in such a PDP. Qualitative verification is shown to amount to a graph analysis of the PDP. Reachability probabilities in our PDPs are then characterized as the least solution of a system of Volterra integral equations of the second type and are shown to be approximated by the solution of a system of partial differential equations. For single-clock DTA, this integral equation system can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations. As the coefficients are in fact transient probabilities in CTMCs, this result implies that standard algorithms for CTMC analysis suffice to verify single-clock DTA specifications.
6. Ludics with repetitions (Exponentials, Interactive types and Completeness)
Ludics is peculiar in the panorama of game semantics: we first have the definition of interaction-composition and then we have semantical types, as a set of strategies which "behave well" and react in the same way to a set of tests. The semantical types which are interpretations of logical formulas enjoy a fundamental property, called internal completeness, which characterizes ludics and sets it apart also from realizability. Internal completeness entails standard full completeness as a consequence. A growing body of work start to explore the potential of this specific interactive approach. However, ludics has some limitations, which are consequence of the fact that in the original formulation, strategies are abstractions of MALL proofs. On one side, no repetitions are allowed. On the other side, the proofs tend to rely on the very specific properties of the MALL proof-like strategies, making it difficult to transfer the approach to semantical types into different settings. In this paper, we provide an extension of ludics which allows repetitions and show that one can still have interactive types and internal completeness. From this, we obtain full completeness w.r.t. a polarized version of MELL. In our extension, we use less properties than in the original formulation, which we believe is of independent interest. We hope this may open the way to applications of ludics approach to larger domains and different settings.
7. Logical Step-Indexed Logical Relations
Appel and McAllester's "step-indexed" logical relations have proven to be a simple and effective technique for reasoning about programs in languages with semantically interesting types, such as general recursive types and general reference types. However, proofs using step-indexed models typically involve tedious, error-prone, and proof-obscuring step-index arithmetic, so it is important to develop clean, high-level, equational proof principles that avoid mention of step indices. In this paper, we show how to reason about binary step-indexed logical relations in an abstract and elegant way. Specifically, we define a logic LSLR, which is inspired by Plotkin and Abadi's logic for parametricity, but also supports recursively defined relations by means of the modal "later" operator from Appel, Melliès, Richards, and Vouillon's "very modal model" paper. We encode in LSLR a logical relation for reasoning relationally about programs in call-by-value System F extended with general recursive types. Using this logical relation, we derive a set of useful rules with which we can prove contextual equivalence and approximation results without counting steps.
8. An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms
This paper presents a new exponential lower bound for the two most popular deterministic variants of the strategy improvement algorithms for solving parity, mean payoff, discounted payoff and simple stochastic games. The first variant improves every node in each step maximizing the current valuation locally, whereas the second variant computes the globally optimal improvement in each step. We outline families of games on which both variants require exponentially many strategy iterations.