Sylvain Schmitz (Cachan, INRIA Saclay, Warwick)
Complexity upper bounds for VASS reachability
More than 30 years after their inception, the complexity of the algorithms for VASS reachability is still an open issue. By examining the decomposition techniques of Mayr, Kosaraju, and Lambert, and using recent results on the complexity of termination thanks to well quasi orders and well orders, I will show how to obtain (fast-growing) complexity upper bounds in cubic Ackermannian time.
Joint work with Jérôme Leroux; article available from http://arxiv.org/abs/1503.00745.
James Worrell (Oxford)
On termination of integer linear loops
A fundamental problem in program verification concerns the termination of simple linear loops of the form:
x := u ; while (Bx >= c) do (x := Ax+a)
where x is a vector of variables, u, a, and c are integer vectors, and A and B are integer matrices. Such a loop is said to be terminating if it halts for all initial integer vectors u.
Decidability of termination was posed over 10 years ago by Tiwari and Braverman. In this talk we describe a decision procedure under the assumption that the update matrix A is diagonalisable and we discuss obstacles to solving the general problem. The correctness of our algorithm relies on Diophantine-approximation lower bounds and on tools from real-algebraic geometry.
Joint work with Joel Ouaknine and Joao Sousa Pinto.
Nathalie Bertrand (INRIA Rennes)
Diagnosis for probabilistic systems
The diagnosis problem amounts to deciding whether some specific faulty event occurred, given the observations collected along a run of a system. The active diagnosis problem consists in controlling the system in order to ensure its diagnosability. We present here decidability and complexity results for the diagnosis and active diagnosis problems in probabilistic systems. In particular, we show that diagnosability is PSPACE-complete, and give tight bounds on the size of diagnosers. Also, we prove that the active diagnosis problem is EXPTIME-complete, and that belief-based controllers suffice. Last, we consider a safe variant of the active diagnosis problem in which additionally the controller should not force the occurrence of a fault. This problem turns out to require non belief-based strategies, and is even undecidable, unless controllers are bound to have finite memory.
This talk is based on joint works with Serge Haddad, Engel Lefaucheux, Eric Fabre, Stefan Haar and Loic Helouet.
Antonin Kucera (Brno)
Recent results about probabilistic multi-counter machines
The talk surveys recent results about probabilistic multi-counter automata and probabilistic vector additions systems with states (pVASS). A special attention is devoted to long-run average properties such as mean-payoff or limit frequency of certain events. Interestingly, for probabilistic pVASS with two or more counters, long-run average properties may take several different values with positive probability even if the underlying state space is strongly connected. This contradics the previous results about stochastic Petri nets established in 80s. For pVASS with three or more counters, it may even happen that the long-run average properties are undefined (i.e., the corresponding limits do not exist) for almost all runs, and this phenomenon is stable under small perturbations in transition probabilities. On the other hand, one can effectively approximate eligible values of long-run average properties and the corresponding probabilities for some sublasses of pVASS. These results are based on new exponential tail bounds achieved by designing and analyzing appropriate martingales. The main underlying ideas will be explained during the talk.
Davide Sangiorgi (Bologna, INRIA Sophia Antipolis)
Equations, contractions, and unique solutions
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 trasferred onto other behavioural equivalences, possibly non-coinductive, enabling us to use to reuse the coinductive reasoning style in these equivalences.
Slawomir Lasota (Warsaw)
Reachability analysis of first-order definable pushdown systems
We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are first-order definable in a fixed countably-infinite structure. We show that the reachability analysis can be addressed with the well-known saturation technique for the wide class of oligomorphic structures. Moreover, for the more restrictive homogeneous structures, we are able to give concrete complexity upper bounds. We show ample applicability of our technique by presenting several concrete examples of homogeneous structures, subsuming, with optimal complexity, known results from the literature. We show that infinitely many such examples of homogeneous structures can be obtained with the classical wreath product construction. Finally we will discuss an important example of pushdown systems over a non-oligomorphic structure that models time. This generalizes dense-timed pushdown systems.
This is a joint work with Lorenzo Clemente; article available at http://arxiv.org/abs/1504.02651.