Asynchronously communicating pushdown systems (ACPS) that satisfy the empty-stack constraint (a pushdown process may receive only when its stack is empty) are a popular decidable model for recursive programs with asynchronous atomic procedure calls. We study a relaxation of the empty-stack constraint for ACPS that permits concurrency and communication actions at any stack height, called the shaped stack constraint, thus enabling a larger class of concurrent programs to be modelled. We establish a close connection between ACPS with shaped stacks and a novel extension of Petri nets: Nets with Nested Coloured Tokens (NNCTs). Tokens in NNCTs are of two types: simple and complex. Complex tokens carry an arbitrary number of coloured tokens. The rules of NNCT can synchronise complex and simple tokens, inject coloured tokens into a complex token, and eject all tokens of a specified set of colours to predefined places. We show that the coverability problem for NNCTs is Tower complete. To our knowledge, NNCT is the first extension of the class of Petri nets with an infinite set of token types that have primitive recursive coverability. This result implies Tower completeness of coverability for ACPS with shaped stacks.
(This is based on joint work with Jonathan Kochem.)
Higher-order recursive schemes (HORS) are schematic representations of functional programs. They generate possibly infinite ranked labelled trees and, in that respect, are known to be equivalent to a restricted fragment of the λY-calculus, consisting of ground-type terms whose free variables have types of the form o → ... → o (with o as a special case).
In this paper, we show that any λY-term (with no restrictions on term type or the types of free variables) can actually be represented by a HORS. That is, for any λY-term M, there exists a HORS generating a tree that faithfully represents M's Böhm tree. In particular, the HORS captures higher-order binding information contained in the Böhm tree. An analogous result holds for finitary PCF.
As a consequence, we can reduce a variety of problems related to the λY-calculus or finitary PCF to problems concerning higher-order recursive schemes. For instance, Böhm tree equivalence can be reduced to the equivalence problem for HORS. Our results also enable MSO model-checking of Böhm trees.
This is joint work with Pierre Clairambault (ENS Lyon).
This talk is about proof techniques for behavioural equivalences. One of the most studied behavioural equivalences is bisimulation, and the main reason for its success is the associated bisimulation proof method. This method can be further enhanced by means of `up-to bisimulation' techniques. In the talk, I will discuss a different proof method, based on unique solutions of equations. I will introduce contractions, special forms of inequations. I will show that the `unique solution of contraction' method is at least as powerful as the bisimulation proof method and its enhancements. I will then show that the method can be transferred onto other behavioural equivalences, possibly non-coinductive, enabling us to use to reuse the coinductive reasoning style in these equivalences.
The coordination language KLAIM is well-suited for modelling message-passing-based distributed systems. It is based on a distributed Linda-like memory model and features explicit localities as well as remote access to memory. In this work we use a rewriting-based approach to formally specify and analyze KLAIM and its semantics. In particular we: (i) specify the reduction semantics of KLAIM in Maude, (ii) extend the Maude-based specification by making messages first-class citizens, and (iii) describe a second extension that allows true distributed execution of Maude-based KLAIM specifications. We analyze the relationships between these specifications and show that the Maude implementation of KLAIM is stuttering bisimilar to the reduction semantics of KLAIM and that also the message-extension and the distributed extension (as well as their weak fair versions) are stuttering bisimilar to the Maude implementation of KLAIM. To our knowledge these Maude specifications are the first provably correct implementations of KLAIM.
(This is based on joint work with Jonas Eckhardt, Tobias Mühlbauer, José Meseguer)
I will present several challenging examples of (possibly conditional or approximate) program equivalences that arise in the context of cryptographic proofs.
In the classical Mazurkiewicz trace approach the behaviour of a concurrent system is described in terms of sequential observations that differ only with respect to their ordering of independent actions. This talk aims to determine a full generalisation of the trace model to the case that actions can be observed as occurring simultaneously. Thus observations are sequences of steps, i.e., sets of actions. This leads to an extended trace model based on three relations between events: simultaneity, serialisability, and interleaving. Whereas the underlying causal structures of traces are based on dependencies between actions leading to a partial order interpretation, more general causal orders are needed to describe the invariant relations between the action occurrences in a generalised trace. The talk presents a complete picture including extended dependence graphs and a characterisation in terms of the (most) general order structures.
TLA+ is a formal specification language based on Zermelo-Fraenkel set theory for describing data structures and linear-time temporal logic for describing system behavior. In this talk, I present the TLA+ Proof System, an interactive platform for deductive verification of TLA+ specifications. In particular, I highlight some of the main design decisions underlying TLAPS, and some of the challenges that we faced.
TLAPS is freely available from https://tla.msr-inria.inria.fr/tlaps/content/Home.html.
The talk introduces a parametric extension of Action- Restricted Computation Tree Logic. Symbolic fixed-point algorithms providing a solution for the exhaustive parameter synthesis are proposed. We show that the parametric approach allows for an in-depth system analysis and synthesis of correct parameter values. The prototype tool implementing the solution is applied to the analysis of Peterson's mutual exclusion protocol and the eficiency of the symbolic approach is estimated on scalable systems. In the experimental evaluation, we also compare the symbolic approach with a naive solution to the problem.