Exposés des semaines suivantes

Jeudi 5 mars, salle Lipari, 14h

Aline Goeminne

On Relevant Equilibria in Reachability Games

We study turn-based multiplayer reachability games played on a finite directed graph equipped with target sets, one for each player. In those reachability games, it is known that there always exists a Nash equilibrium (NE) and a subgame perfect equilibrium (SPE). But sometimes several equilibria may coexist such that: in one equilibrium, no player reaches his target set whereas in another one, several players reach it. It is thus natural to identify some kind of "relevant" equilibria. For example, we may study the following decision problem: Given a number of steps for each player, does there exists an equilibrium such that, if the players follow this equilibrium, they reach their target set within this number of steps? We have proved that this problem is NP-complete for NEs and PSPACE-complete for SPEs. To obtain these results, we show that we are able to exactly characterize the set of the outcomes of NEs (resp. SPEs) thanks to an appropriate labeling of the vertices of the game graph.

Vendredi 6 mars, 14h

Mathias Ramparison

Updatable Parametric Timed Automata: Decidability, Algorithms, and Application to Security

As cyber-physical systems become more and more complex, human debugging is not sufficient anymore to cover the huge range of possible behaviours. For costly critical systems where human lives can be endangered, formally proving the safety of a system is even more crucial. This is done by defining a formal specification for the system, and then performing the algorithmic verification that the system satisfies some formally specified properties. With this precise and exhaustive description of a system, the usual vagueness of human language is eliminated.
We focus on the verification of timed concurrent systems. Timed-dependent systems are very hard to verify, especially when the exact value of timing constants remains unknown. These unknown timing constants are called parameters. We study several subclasses of a parametric extension of the well-known formalism called Timed Automata. We mainly focus on the reachability decision problem, that asks whether there exists concrete values for these parameters such that a bug state can be reached in the system. We further address for these subclasses a computation problem that is to synthesise the set of parameter values for which a state is reachable. Finally, we apply our work to the security and safety of cyber-physical systems and infrastructure: we extend with parameters a classic formalism to model attack and failure scenarios called attack-fault trees, and propose an implementation of the translation of parametric attack-fault trees to parametric timed automata. This allows us to leverage the verification techniques and tools available for the latter for the analysis of (parametric).

Jeudi 12 mars, 14h en salle Lipari F202

Adrien Le Coënt

Guaranteed co-simulation of continuous-time dynamical systems

We tackle the problem of guaranteed simulation of continuous-time dynamical systems. The always increasing complexity of current engineering systems leads to models of higher and higher dimensions, yet typically involve multiple subsystems or even multiple physics. Given this modularity, we more precisely explore co-simulation of such dynamical systems, with the aim of reaching higher dimensions of the simulated systems. In a co-simulation setting, the global system is divided in sub-systems, for which different simulation units (and possibly schemes) are used, but exchange values of their outputs at some communication (macro) steps. In this talk, we present a guaranteed interval based approach for co-simulation of continuous time systems. Provided that a suitable decomposition of the system is given, we propose an algorithm which first proves the existence, and returns an enclosure of global solutions, using only local computations. This mitigates the curse of dimensionality faced by global (guaranteed) integration methods. Local computations are then realized with a safe estimate of the other sub-systems until the next macro step. We increase the accuracy of the approach by using an interval extrapolation of the state of the other sub-systems. We finally propose some possible further improvements including adaptive macro step size. Our method is fully guaranteed, taking into account all possible sources of error. We illustrate our approach on multiple examples of the literature, and show some possible applications in e.g. symbolic optimal control synthesis.

Jeudi 19 mars, 14h. Salle Lipari F202

François Schwarzentruber

Constraint graphs: some PSPACE-hardness proofs made easy

We will discuss a new computation model called constraint graphs (aka constraint logic), introduced by Erik Demaine and Robert Hearn. Constraint graphs have been successfully applied to games, such as sliding block puzzles, Rush Hour and Sokoban. Recently, it has been applied for proving PSPACE-hardness of multi-agent path finding with connectivity. I claim that this computation model may be useful for many reachability problems, that have a geometric flavor, whose actions are reversible. The main interest is that constraint graphs only rely on two gadgets: an AND gate and an OR gate. In this talk, we will prove that the reachability problem for constraint graphs is PSPACE-complete. The reduction from the truth of a quantified binary formulae shows the computation power of constraint graphs.

Vos propositions sont les bienvenues !