PhD Defence: Mathieu Hilaire

Dec 13 9:00 ₂₀₂₂

Abstract: The most standard model checking approaches are limited to verifying concrete specifications, such as “can we reach a configuration with more than 10 time units elapsing ?”. Nevertheless, for certain computer programs, like embedded systems, the constraints depend on the environment. Thus arises the need for parametric specifications, such as “can we reach a configuration with more than p time units elapsing ?” where p is a parameter which takes values in the non-negative integers.

In this thesis, we study parametric pushdown, counter and timed automata and extensions thereof. In addition to expressing concrete constraints (on the stack, on the counter or on clocks), these can employ parametric constraints. The reachability problem for a parametric automaton asks for the existence of an assignment of the parameters such that there exists an accepting run in the underlying concrete automaton. In addition to the reachability problem, we consider parametric parity games, two player games where players alternate choosing assignments for each parameters, then alternate moving a token along the configurations of the concrete automaton resulting from their choice of parameter assignment. We consider the problem of deciding which player has a winning strategy.

Parametric timed automata (PTA for short) were introduced in the 90s by Alur, Henzinger and Vardi, who showed that the reachability problem for PTA was undecidable, already when only three clocks can be compared against parameters, and decidable in the case only one clock can. We call such clocks that can be compared to parameters parametric clocks. A few years ago, Bundala and Ouaknine proved that, for parametric timed automata with two parametric clocks and one parameter ((2, 1)-PTA for short), the reachability problem is decidable and also provided a PSPACE NEXP lower bound. One of the main results of this thesis states that reachability for (2, 1)-PTA is in fact EXPSPACE-complete. For the EXPSPACE lower bound, inspired by previous work by Göller, Haase, Ouaknine, and Worrell, we rely on a serializability characterization of EXPSPACE (in turn originally based on Barrington’s Theorem). We provide a programming language and we show it can simulate serializability computations. Relying on a logspace translation of numbers in Chinese Remainder Representation to binary representation due to Chiu, Davida, and Litow, we then show that small (2, 1)-PTA can simulate our programming language. For the EXPSPACE upper bound on (2, 1)-PTA, we first give a careful exponential time reduction towards a variant of parametric one-counter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. We solve the reachability problem for this parametric one-counter automata with one parameter variant, by providing a series of techniques to partition a fictitious run into several carefully chosen subruns. This allows us to prove that it is sufficient to consider a parameter value of exponential magnitude only, which in turn leads to a doubly-exponential upper bound on the value of the only parameter of the (2, 1)-PTA. We hope that extensions of our techniques lead to finally establishing decidability of the long-standing open problem of reachability in PTA with two parametric clocks and arbitrarily many parameters.

Concerning parametric pushdown automata, our main result states that deciding the winner of a parametric parity game is in (n + 1)-EXP in the case the number of parameters n is fixed, but none-elementary otherwise. We provide the nonelementary lower bound via a reduction of the FO satisfiability problem on words. For the upper bound, we reduce parametric pushdown parity games to higher-order pushdown automata parity games, which are known to be n-EXP complete in the case of stacks of level n.

Jury:

• Nathalie Bertrand, Research Director, Inria Rennes
• Véronique Bruyère, Professor, Université de Mons - Reviewer
• Joël Ouaknine, Research Director, Max Planck Institute for Software Systems Saarbrücken - Reviewer
• Étienne André, Professor, Université de Lorraine - Examiner
• Jiri Srba, Professor, Université de Aalborg- Examiner
• Stefan Göller, Professor, Universität Kassel - PhD supervisor
• Benedikt Bollig, Research Director, LMF - PhD co-supervisor