Étienne André, Villetaneuse, France
Title: Monitoring cyber-physical systems under uncertainty
Monitoring cyber-physical systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals gathered in a log, while real behaviors are continuous-time signals, which implies some uncertainty.
In addition, the monitoring properties can themselves feature some uncertainty: e.g., a period in a property to be monitored can be uncertain or even unknown.
In this presentation, we present two ways to address uncertainty while monitoring cyber-physical systems.
First, we address timed pattern matching in the presence of an uncertain specification. We want to know for which start and end dates in a log, and for what values of the timing parameters, a property holds. For instance, we look for the minimum or maximum period (together with the corresponding start and end dates) for which the property holds.
We rely on two solutions, one based on model-checking, and the other one being ad-hoc.
Second, to mitigate the problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use a (limited) prior knowledge about the target system in order to prune interpolation candidates. We express such prior knowledge by linear hybrid automata (LHAs)—the LHAs are called bounding models. We rely on reachability techniques for linear hybrid automata using polyhedra to efficiently decide whether the property holds on a given log.
We implemented both approaches, and experiments on realistic benchmarks show that both directions are efficient and practically relevant.
This presentation is mainly based on publications at ICECCS 2018 and ACM ToCPS (2022), and are joint work with Masaki Waga (Kyoto University) and Ichiro Hasuo (NII, Tokyo, Japan).
Nathalie Bertrand, Rennes, France
Title: A CEGAR approach to parameterized verification of distributed algorithms
Distributed algorithms are central to many domains such as scientific computing, telecommunications and the blockchain. Even when they aim at performing simple tasks, their behaviour is hard to analyze, due to the presence of faults (crashes, message losses, etc.) and to the asynchrony between the processes. Parameterized verification techniques have been developed to prove correctness of distributed algorithms independently of actual setup, i.e. the number of processes and the potential failures.
In this talk, we present a CEGAR approach to checking safety and liveness properties for fault-tolerant distributed algorithms that use threshold conditions, typically on the number of received messages of a given type.
This is based on joint work with Bastien Thomas, Ocan Sankur and Josef Widder.
Igor Konnov, Vienna, Austria
Title: Threshold-guarded distributed algorithms: Verification and practical challenges
Threshold guards are a basic primitive of many fault-tolerant algorithms that solve the following classical problems of distributed computing: reliable broadcast, two-phase commit, and consensus. These algorithms have the following features: (1) up to t of processes may crash or behave Byzantine; (2) the correct processes count messages and progress when they receive sufficiently many messages, e.g., at least t+1; (3) the number n of processes in the system is a parameter, as well as t; (4) and the parameters are restricted by a resilience condition, e.g., n > 3t. In this talk, we give an overview of the techniques for parameterized verification of asynchronous threshold-guarded distributed algorithms. We further discuss the central place of thresholds in distributed algorithms for blockchains, using the Cosmos ecosystem as an example. We conclude with the challenges for parameterized verification techniques that arise from verification problems in industry.
Kim G. Larsen, Aalborg, Denmark
Title: Parameterized Weighted Systems and Properties
In this talk I will survey our work on efficient extensions of on-the-fly model checking of finite-state systems to model-checking of quantitative (weighted and weighted probabilistic) systems using appropriate symbolic extensions of so-called dependency graphs (DG). I particular I will highlight our extensions to parametric settings, where concrete weights (or rewards) in transitions of a model – or threshold values in a properties are replaced by expressions build over a set of parameters. Here parametric symbolic DG has been developed lifting the computation of fixed points from the Boolean domain to that of non-negative real-valued maps to cope with parametric weights.
As an alternative to DG we have developed an approach (for parameterized Markov reward models) based on quantifier elimination for linear real arithmetic. Differently from existing solutions for parametric Markov chains, we avoid the manipulation of rational functions in favor of a symbolic representation of the set or parameter valuations satisfying a given property in the form of a quantifier-free first-order formula in the linear theory of the reals.
Finally, I will present ongoing work on cost-optimal reachability for parametric priced timed automata, e.g. priced timed automata, where cost-rates or locations are given by expressions of a set of parameters. We will illustrate how the notion of priced zones may be extended to parametric priced zones, which equipped with a suitable well-quasi ordering will guarantee termination of a forward symbolic A* algorithm.
The presentation is partly based on ongoing work (related to the last part) and on work published in a series of papers appearing at STTT16, NFM19, QEST18, QEST19 as well as STTT22. The work has been done in collaboration with a number of colleagues including Gionvanni Bacci, Mikkel Hansen, Jiri Srba, Anders Mariegaard, Mathias Claus Jensen, Benoit Delahaye and Søren Enevoldsen.
Joël Ouaknine, Sarrebruck, Germany
Title: Holonomic Techniques
Holonomic techniques have deep roots going back to Wallis, Euler, and Gauss, and have evolved in modern times as an important subfield of computer algebra, thanks in large part to the work of Zeilberger and others over the past three decades. In this talk, I give an overview of the area, and in particular present a select survey of known and original results on decision problems for holonomic sequences and functions. I also discuss some surprising connections to the theory of periods and exponential periods, which are classical objects of study in algebraic geometry and number theory; in particular, I relate the decidability of certain decision problems for holonomic sequences to deep conjectures about periods and exponential periods, notably those due to Kontsevich and Zagier.
No prior knowledge of any of the above is expected or required.
Tali Sznajder, Paris, France
Title: Verification of Networks of Processes communicating with Non-Blocking Rendez-Vous
A vast majority of modern systems are distributed, allowing interactions between processes that are on different locations (applications include e-business, transportation systems, ad-hoc networks,…) and organized according to fixed or mobile architectures. When we want to analyze these systems, we have to face specific challenges: the type of communication, that can be synchronous or asynchronous, data, that can be shared, or of unbouded values, the number of processes involved in the system, that can be unknown, the communication graph of the system, … Formal methods have proved to be very useful for the analysis and verification of complex systems. Verification of parameterized systems aims at verifying at once a whole (infinite) family of systems : when an algorithm has been designed to work on an arbitrary number of processes, it is not enough to check its correction for a fixed number of them. We would rather provide a proof that the system is correct whatever the number of processes involved. In this talk, we will focus on networks of communicating processes, whose number is not known a priori (it is a parameter), all running the same protocol, and communicating via non-blocking rendez-vous. When a non-blocking rendez-vous occurs, the sender of the message is not blocked waiting for a process to be able to receive it, unlike in the classical rendez-vous model. This mechanism is implemented for instance in multi-threaded Java programs.
This is a joint work with Lucie Guillou and Arnaud Sangnier.
