# 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.