Jeudi 27 février, 14h en salle Markov
Toward certified quantum programming
Due to the nature of quantum computation, we believe that, in this field, formal veri cation is meant to play a role similar to that of test development in classical computing. In this seminar we present Qbricks , a core programming language for entirely verifiable quantum programming. Qbricks both provides programming functions such as in other programming languages and formal analysis means enabling to specify and verify the written programs. We believe this two layers approach is necessary for widespread verified programming methodology. We present our implementation of both the matrix and the path-sum semantics for quantum processes and the first fully verified equivalence proof between those. In addition, we implemented various further semantics artifacts for quantum circuits semantics. Thanks to Qbricks , we present a verified implementation of the phase estimation algorithm. Phase estimation constitutes the quantum part of the famous Shor algorithm for the factorization of integers. It is also at the heart of many further emblematic quantum algorithm (matrix inversion, quantum simulation etc.). Our proved implementation is, as far as we know, the first scale-invariant proof of a non-trivial quantum routine.
Exposés des semaines suivantes
Jeudi 5 mars, salle Lipari, 14h
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
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
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 !