Probabilistic models and their analysis

The use of randomization in concurrent or distributed systems is often key to achieving certain objectives. For example, it is used in distributed algorithms to break symmetry and in cryptographic protocols to achieve semantic security. While analyzing such systems for correctness, these systems are often modeled as transition systems that have both randomized and nondeterministic transitions. It is customary to resolve the nondeterminism by a scheduler who chooses a transition based on the past sequence of states visited during the computation. When analyzing such systems for correctness, it is often necessary to restrict the set of schedulers to obtain sound and precise results. The feasibility of the analysis depends on the class of schedulers under consideration. In this talk, we survey recent results on analysis of probabilistic systems focusing on restriction of schedulers that arise a) in reactive systems and b) in security protocols.

Asymptotic analysis of tropical automata

Automata weighted over tropical semirings (min,+) and (max,+) are useful modelling tools. Tropical automata compute maps from words to non-negative integers (or infinity). Such maps are defined over a given input as the minimum/maximum over all accepting runs of the sum of weights of the transitions (each transition is weighted by a non-negative integer in our case). (min,+)-automata are naturally used to optimize computations over an input, and (max,+)-automata naturally model worst case behaviours. Another classical application of tropical automata is the approximation probablistic automata.

It is known from D. Krob in the ninetees that the problem of comparing the maps definable by such automata (toward equality or order) is not decidable. In this talk, I will present several results that circumvent this difficulty, and give precise decidable approximations of these problematic problems. Our results essentially take the form of effective asymptotic descriptions of the behaviour of the automata when their inputs become arbitrarily large.

In particular, our result concerning (max,+)-automata can be used for the analysis of the complexity of programs as a functions of the size of their inputs, thanks to the use of the size change abstraction.

These works are the subject of the PhD thesis of Laure Daviaud, defended this year, and part of them were the subject of a publication with Florian Zuleger. This research was funded by the ERC project GALE.

Well-Structured Graph Transformation Systems

Graph transformation systems (GTSs) can be seen as well-structured transition systems (WSTSs), thus obtaining decidability results for certain classes of GTSs. It was shown that well-structuredness can be obtained using the minor ordering as a well-quasi-order. We extend this idea to obtain a general framework in which several types of GTSs can be seen as (restricted) WSTSs. We instantiate this framework with the subgraph ordering and the induced subgraph ordering. Furthermore we present the tool UNCOVER and discuss runtime results.

Robustness against Relaxed Memory Models

For performance reasons, modern multiprocessors implement relaxed memory consistency models that admit out-of-program-order and non-store atomic executions. While data race-free programs are not sensitive to these relaxations, they pose a serious problem to the development of the underlying concurrency libraries. Library routines that work correctly under Sequential Consistency (SC) show undesirable effects when run under a relaxed memory model. These routines are not robust against the relaxations that the processor supports. To enforce robustness, the programmer has to add safety net instructions to the code that control the hardware --- a task that has proven to be difficult, even for experts.

We recently developed algorithms that check and, if necessary, enforce robustness against prominent relaxed memory models like TSO implemented in x86 processors and Power implemented in IBM architectures. Given a program, our algorithms decide whether the actual behavior on the processor coincides with the SC semantics. If this is not the case, they synthesize safety net instructions that enforce robustness. When built into a compiler, our algorithms thus hide the relaxed memory model from the programmer and provide the illusion of Sequential Consistency.

In this talk, we motivate the robustness problem and explain how to reduce it to a standard SC reachability query.

Multi-dimensional energy games and related problems

I shall present recent work on multi-dimensional energy games, which happen to have strong connections to several questions about vector addition systems, regarding finite-system simulations, zero-reachability games and alternating termination.

The work is joint with Marcin Jurdzinski and Sylvain Schmitz.

Walking With Data: Where Does it Stop?

Data formalisms apply to numerous settings where the reasoning in- volves explicit comparisons of object identities. Such formalisms are usually based on automata or logics that have the ability to compare data from an unbounded domain. In the realm of databases, data may take the meaning of attribute values. In program verification, data may represent identities of processes, communication channels, pointers or any other resource that can be of interest in the analysis of programs with dynamic objects.

This talk will survey several models of logics and automata with data and analyse their limits in decidability regarding fundamental questions such as non-emptiness (satisfiability) and inclusion (containment). We will focuss on recently considered data formalisms such as data-walking automata and Datalog, that are promising models regarding the above problems.

Bounded-Rate Multi-Mode Systems Based Motion Planning

Hybrid automata are a natural and expressive formalism to model systems that exhibit both discrete and continuous behavior. However, the applications of hybrid automata in analyzing cyber-physical systems have been rather limited due to undecidability of simple verification problems such as reachability. This drawback of hybrid automata has fueled the investigation of the so-called compositional methodology to design complex system by sequentially composing well-understood lower-level components. This methodology has, for example, been used in the context of the motion planning problem for mobile robots, where the task is to move a robot along a pre-specified trajectory with arbitrary precision by sequentially composing a set of well-studied simple motion primitives, such as "move left", "move right" and "go straight". In this talk, we summarize some of our recent results related to efficient solution of motion planning problem for systems whose motion primitives are given as constant-rate vectors with uncertainties.

Ideal Abstractions of Concurrent Infinite State Systems

Many concurrent infinite state systems can be seen as well-structured transition systems (WSTS). Examples include concurrent programs with shared-memory and dynamic thread creation, as well as distributed message passing systems in the actors framework. WSTS are an attractive class of systems for formal analysis because they admit generic decision procedures for important verification problems such as coverability. Unfortunately, these decision procedures often have very high complexity or provide termination guarantees only in special cases that are not of practical relevance. To obtain a practical analysis with more general termination guarantees, we propose an abstract interpretation that is inspired by decision procedures for the covering problem of WSTS. The abstract domain of our analysis builds on the ideal completion of the well-quasi-ordered state space to obtain an efficient symbolic representation of infinite sets of states. A widening operator that mimics acceleration-based forward algorithms for computing covering sets ensures termination while controlling the loss of precision of the analysis. I will present an instance of our analysis framework for the class of depth-bounded systems and its application to verifying progress properties of concurrent data structure implementations.