Main objectives of EQUAVE

The main objective of this project is to study efficient techniques for quantitative verification of cyber-physical systems, and develop efficient algorithms for models of such systems that involve time and/or randomness. A first and immediate challenge is to have good models for such systems that would capture the necessary features while remaining tractable. In this project, we plan to focus on classical as well as new models including Markov decision processes, stochastic timed games, and different variants of timed and concurrent systems. Indeed one objective of the project is to classify the problems and models of cyber-physical systems in terms of tractability. The project is organized along three main research directions: The first direction is dedicated to timed systems, with an emphasis on efficiency of algorithms for the verification of timed properties of concurrent systems. The second line of research will consider the control of stochastic models. The third line of research will focus on models with both characteristics

R1: Timed Systems

In the untimed setting, a usual solution to master complexity of distributed systems is to consider models with restricted use of concurrency, such as Free-choice Petri nets [EsparzaD95] where algorithms are often polynomial, or more recently negotiations [EsparzaD13], for which termination can be reduced to efficient application of reduction rules [EsparzaMW16, EsparzaMW17] leading to polynomial algorithms. So far, time in negotiations has not been considered and our first target would be towards extending the model with timing information in a sensible manner. We plan to work on it in the first year, starting with our recent work, timed concurrency models with free choice [Joint14]. Another topic that we plan to address in year 2 and 3 is recoverability in a timed but unstable world: consider systems with a correct idealized behavior. The behavior of the real system is perturbed by random noise (delay, etc). In real systems such as metro rail networks, a system does not stay in a degraded situation, and often tries to get back to the ideal behavior through corrective mechanisms. For models including recovery mechanisms, a key question is the time needed to return to a normal behavior, and the divergence that occurred since disruption. Modeling and verification of such phenomena would complete this objective.

R2: Control of Stochastic models

Quantitative analysis of stochastic systems is known to be extremely hard. Indeed, [I4] showed that checking whether the trajectory of a Markov Chain (representing e.g. a given plan for robots) satisfies that the probability to be in a given (bad) state is never higher than a given threshold is as hard as a long-standing open problem on linear recurrence sequences, called the Skolem problem. The decidability of this question has been opened for more than 40 years. On the other hand, there exists a PTIME algorithm [Tiwari04] to check the same question provided that the initial distribution is not fixed but allowed to vary in the given space (a kind of typing result for stochastic systems). In the first year of the project, we plan to extend this typing approach to handle Markov Decision Processes (MDPs), that is, to control stochastic systems. In the year 2 and 3, we will consider another approach to obtain efficient algorithms, through the use of approximations. In this respect, we plan to extend the efficient algorithm for the isolation problem in Markov Chains [ChadhaKV14], which approximates its quantitative verification, towards MDPs.

R3: Efficent algorithms for timed stochastic models

The equave project plans to build on the results from axes 1 and 2 to study stochastic models with time, possibly under the unifying approach of timed and stochastic games. Time and probabilities are two natural quantitative features. They are present in models such as probabilistic timed automata and their game extensions, for which verification algorithms exist, and are implemented, e.g. in the prominent tool PRISM. However, when time and probabilities are genuinely mixed, i.e. when delays are randomized, the models become more complex from an analysis viewpoint. Several contributions aim at defining large classes of stochastic timed games for which verification problems are decidable [BF-icalp09, R5]. So far, the complexity picture is still open. Recent advances on the understanding of the purely stochastic model (with no players involved) [R4] should help to progress on stochastic timed games. However, while this model is the closest to what may be needed in reality, it is quite challenging as even basic theoretical questions are hard to tackle. Our goal is to identify where the decidability frontier lies for timed stochastic 2 player games. Recent results [R4, BBBC-RR17] indicate that quantitative questions can be decided for stochastic timed models. Our objective is to explore whether these positive results extend to the game setting. In the first year, we will consider the restricted case of stochastic timed games where player 1 has no choice. For the general case, we will need new techniques as the existing ones are unlikely to extend. Developing these new analysis techniques is the plan for the years 2 and 3.

Applications:

This project will consider practical application in the domain of networks of automotive systems (metros and multi-modal transport systems), that are by nature distributed, timed, and subject to random perturbations (delays, incidents), and of biological systems, that are stochastic and distributed systems where quantities and parameters such as the size of a population of cells plays an important role in the dynamics of the system.