Operator methods for quantitative analysis of timed and stochastic systems

Thesis co-directed by Aldric Degorre (adegorre _AT_ irif.fr) and Eugene Asarin (asarin _AT_ irif.fr)

Financed by the ANR Project MAVeriQ (ANR-ANR-20-CE25-0012).

This thesis topic is motivated by the analysis of modern software-driven systems, including in particular cyber-physical systems: consisting in both computers and physical devices interacting with the physical environment, the typical example being automotive control.

Such systems are often described by theoretical models such as hybrid automata, where the state contains both a discrete and a continuous component, and more abstract (and also more tractable) models such as timed automata or even finite automata. In this setting, uncertainty is often represented by probabilities, yielding stochastic versions of these models (Markov chains, Markov decision processes, probabilistic timed automata, …).

In this context, not only the models are quantitative, but also the properties we may want to verify on such a system: instead of answering the usual yes/no questions, we want find out “How many?”, “How safe?”, “How costly?” the behaviors of such a system are. The discipline concerned with such questions is called “Quantitative verification”.

In this field, a set of techniques consists in studying the properties of some linear operator (explicit or implicit) that describes one “step” of evolution of the system.

For instance, consider the typical work-flows for computing, respectively, probabilities of sets of runs in Markov Chains and Euclidean volumes of runs in timed automata (TA):

• First, a structure is determined for representing the state of the system with respect to the question of interest: the Euclidean space of timed locations for deterministic timed automata and a set of discrete locations in the case of Markov chains.
• Second, a space of functions from the state space to real numbers is defined: for Markov chains, probability distributions (for reaching a given state at some execution time); for deterministic TA, volume functions (volume of the language accepted from a given state).
• Then an operator (endomorphism of the function space) is written that sums up the effect of a transition of the system on a function in that space: for Markov chains, a stochastic matrix; for TA, some positive integral operator.
• The property of interest is characterized in terms of operators (e.g. computation of a steady distribution or a limit entropy rate).
• Finally, various classes of algorithms may be applied based, for instance, on finite iterations of the operator or the spectral analysis of it.

The above decomposition unifies the two examples we just mentioned, along with some other ones we know (notably: automata on semirings). We actually expect that, with the help of only a few different decomposition patterns, such unification should be possible for many other cases.

The PhD student is expected to:

• Explore such patterns while establishing, as much as possible, a common vocabulary and theory. In the context of MAVeriQ, the considered systems are timed and/or stochastic.
• Write new algorithms based on this theory.
• Promote such approaches to other researchers in the MAVeriQ: work with them on their topics and try to adapt the new theory.

The desired profile is a student in computer science with a good background in fundamental informatics, theory of automata and an interest for quantitative verification issues. Knowledge of algebra and functional analysis are also welcome.

• Eugene Asarin, Nicolas Basset, Aldric Degorre. Entropy of regular timed languages. Inf. Comput., 241:142–176, 2015.
• Eugene Asarin, Nicolas Basset, Aldric Degorre, and Dominique Perrin. Generating functions of timed languages. In MFCS, volume 7464 of Lecture Notes in Computer Science, pages 124–135. Springer, 2012.
• Nicolas Basset. A maximal entropy stochastic process for a timed automaton. Inf. Comput., 243:50–74, 2015.
• Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Größer, and Marcin Jurdziński. Stochastic timed automata. Logical Methods in Computer Science, 10(4:6), December 2014.
• Danièle Beauquier. On probabilistic timed automata. Theoretical Computer Science, 292(1):65 – 84, 2003. Selected Papers in honor of Jean Berstel.
• Einar Hille and Ralph Saul Phillips. Functional analysis and semi-groups, volume 31. American Mathematical Soc., 1996.
• M.P. Schützenberger. On the definition of a family of automata. Information and Control, 4(2):245 – 270, 1961.
• AN Kolmogorov, VM Tikhomirov. ε-entropy and ε-capacity of sets in functional spaces. In Selected works of AN Kolmogorov, pages 86–170. Springer, 1993.