2009 Editors: Nir Piterman, Andrew M Pitts, Radha Jagadeesan

In this paper, we present a systematic way of deriving (1) languages of(generalised) regular expressions, and (2) sound and complete axiomatizationsthereof, for a wide variety of systems. This generalizes both the results ofKleene (on regular languages and deterministic finite automata) and Milner (onregular behaviours and finite labelled transition systems), and includes manyother systems such as Mealy and Moore machines.

The reachability problem for Vector Addition Systems (VASs) is a centralproblem of net theory. The general problem is known to be decidable byalgorithms exclusively based on the classicalKosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. This decomposition isused in this paper to prove that the Parikh images of languages recognized byVASs 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 thisresult; we prove that a final configuration is not reachable from an initialone if and only if there exists a semi-linear inductive invariant that containsthe initial configuration but not the final one. Since we can decide if aPresburger formula denotes an inductive invariant, we deduce that there existcheckable certificates of non-reachability. In particular, there exists asimple algorithm for deciding the general VAS reachability problem based on twosemi-algorithms. A first one that tries to prove the reachability byenumerating finite sequences of actions and a second one that tries to provethe non-reachability by enumerating Presburger formulas.

In a constraint satisfaction problem (CSP) the goal is to find an assignmentof a given set of variables subject to specified constraints. A globalcardinality constraint is an additional requirement that prescribes how manyvariables must be assigned a certain value. We study the complexity of theproblem CCSP(G), the constraint satisfaction problem with global cardinalityconstraints that allows only relations from the set G. The main result of thispaper characterizes sets G that give rise to problems solvable in polynomialtime, and states that the remaining such problems are NP-complete.

The framework of psi-calculi extends the pi-calculus with nominal datatypesfor data structures and for logical assertions and conditions. These can betransmitted between processes and their names can be statically scoped as inthe standard pi-calculus. Psi-calculi can capture the same phenomena as otherproposed extensions of the pi-calculus such as the applied pi-calculus, thespi-calculus, the fusion calculus, the concurrent constraint pi-calculus, andcalculi with polyadic communication channels or pattern matching. Psi-calculican be even more general, for example by allowing structured channels,higher-order formalisms such as the lambda calculus for data structures, andpredicate logic for assertions. We provide ample comparisons to related calculiand discuss a few significant applications. Our labelled operational semanticsand definition of bisimulation is straightforward, without a structuralcongruence. We establish minimal requirements on the nominal data and logic inorder to prove general algebraic properties of psi-calculi, all of which havebeen checked in the interactive theorem prover Isabelle. Expressiveness ofpsi-calculi significantly exceeds that of other formalisms, while the purity ofthe semantics is on par with the original pi-calculus.

We study the verification of a finite continuous-time Markov chain (CTMC) Cagainst a linear real-time specification given as a deterministic timedautomaton (DTA) A with finite or Muller acceptance conditions. The centralquestion that we address is: what is the probability of the set of paths of Cthat are accepted by A, i.e., the likelihood that C satisfies A? It is shownthat under finite acceptance criteria this equals the reachability probabilityin a finite piecewise deterministic Markov process (PDP), whereas for Mulleracceptance criteria it coincides with the reachability probability of terminalstrongly connected components in such a PDP. Qualitative verification is shownto amount to a graph analysis of the PDP. Reachability probabilities in ourPDPs are then characterized as the least solution of a system of Volterraintegral equations of the second type and are shown to be approximated by thesolution of a system of partial differential equations. For single-clock DTA,this integral equation system can be transformed into a system of linearequations where the coefficients are solutions of ordinary differentialequations. As the coefficients are in fact transient probabilities in CTMCs,this result implies that standard algorithms for CTMC analysis suffice toverify single-clock DTA specifications.

Ludics is peculiar in the panorama of game semantics: we first have thedefinition of interaction-composition and then we have semantical types, as aset of strategies which "behave well" and react in the same way to a set oftests. The semantical types which are interpretations of logical formulas enjoya fundamental property, called internal completeness, which characterizesludics and sets it apart also from realizability. Internal completeness entailsstandard full completeness as a consequence. A growing body of work start toexplore the potential of this specific interactive approach. However, ludicshas some limitations, which are consequence of the fact that in the originalformulation, strategies are abstractions of MALL proofs. On one side, norepetitions are allowed. On the other side, the proofs tend to rely on the veryspecific properties of the MALL proof-like strategies, making it difficult totransfer the approach to semantical types into different settings. In thispaper, we provide an extension of ludics which allows repetitions and show thatone can still have interactive types and internal completeness. From this, weobtain 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 ofindependent interest. We hope this may open the way to applications of ludicsapproach to larger domains and different settings.

Appel and McAllester's "step-indexed" logical relations have proven to be asimple and effective technique for reasoning about programs in languages withsemantically interesting types, such as general recursive types and generalreference types. However, proofs using step-indexed models typically involvetedious, error-prone, and proof-obscuring step-index arithmetic, so it isimportant to develop clean, high-level, equational proof principles that avoidmention of step indices. In this paper, we show how to reason about binarystep-indexed logical relations in an abstract and elegant way. Specifically, wedefine a logic LSLR, which is inspired by Plotkin and Abadi's logic forparametricity, but also supports recursively defined relations by means of themodal "later" operator from Appel, Melliès, Richards, and Vouillon's "verymodal model" paper. We encode in LSLR a logical relation for reasoningrelationally about programs in call-by-value System F extended with generalrecursive types. Using this logical relation, we derive a set of useful ruleswith which we can prove contextual equivalence and approximation resultswithout counting steps.

This paper presents a new exponential lower bound for the two most populardeterministic variants of the strategy improvement algorithms for solvingparity, mean payoff, discounted payoff and simple stochastic games. The firstvariant improves every node in each step maximizing the current valuationlocally, whereas the second variant computes the globally optimal improvementin each step. We outline families of games on which both variants requireexponentially many strategy iterations.