Exposés de la saison 2016-2017
jeudi 15 septembre, 11h
Raphaël Berthon
Imperfect Information in Games for Multi-Agent Systems
Problems involving agents can be met in a wide range of fields, and can be used in various ways: agents can represent robots in artificial intelligence, users in security, but also processors in architecture. A formal approach to these problems is to represent the world as a game structure, where the agents are the players, and a task involving our agents is a logical formula in a given language. In this framework, the model checking problem is to check whether our task (a formula) is satisfied on our model of the world (the graph of the game). A question that usually arises is to know if a group of agents has a strategy to reach a given goal in the game. We study this problem on logics with a great expressivity, and when agents have imperfect information about their world.
vendredi 23 septembre, 11h en salle Minquiers
Bernadette Charron-Bost (Ecole polytechnique)
Approximate Consensus in Highly Dynamic Networks: The Role of Averaging Algorithms
We investigate the approximate consensus problem in highly dynamic networks in which topology may change continually and unpredictably. We prove that in both synchronous and partially synchronous networks, approximate consensus is solvable if and only if the communication graph in each round has a rooted spanning tree. Interestingly, the class of averaging algorithms, which have the benefit of being memoryless and requiring no process identifiers, entirely captures the solvability issue of approximate consensus in that the problem is solvable if and only if it can be solved using any averaging algorithm. We develop a proof strategy which for each positive result consists in a reduction to the non-split networks. It dramatically improves the best known upper bound on the decision times of averaging algorithms. We also prove that a general upper bound on the decision times of averaging algorithms have to be exponential, shedding light on the price of memoryless algorithms. Finally we apply our results to networked systems with a fixed topology and benign fault models to show that with n processes, up to 2n−3 of link faults per round can be tolerated for approximate consensus, increasing by a factor 2 the bound of Santoro and Widmayer for exact consensus.
jeudi 13 octobre, 14h en salle Aurigny
Blaise Genest
Controlling a Population.
We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. In this talk, we will describe a sure synchronization problem for such populations: no matter how individual agents react to the actions of the controller, the controller aims at driving all agents synchronously to a goal set of states. The agents are naturally represented by a non-deterministic finite state automaton, the same for every agent, and the whole system is encoded as a 2-player game. The first player chooses actions, and the second player resolves non-determinism for each agent. The game with m agents is called the m-population game. A natural parametrized control problem, given the automaton representing the agents, is whether player one wins the m-population game for any population size m. We show that if the answer is negative, there exists a cut-off, that is, a population size m0 such that for populations of size m < m0 there exists a winning controller, and there is none for populations of size m >m0. Surprisingly, we show that this cut-off can be doubly exponential in the number of states of the NFA. While this suggests a high complexity for the parameterized control problem, we actually show that it can be solved in EXPTIME and is PSPACE-hard. Joint work with Nathalie Bertrand, Miheer Dewaskar et Hugo Gimbert.
jeudi 3 novembre 14h, en salle Minquiers
Béatrice Bérard
Preserving opacity on Interval Markov Chains under simulation.
Given a probabilistic transition system (PTS) A partially observed by an attacker, and an omega-regular predicate P over the traces of A, measuring the disclosure of the secret P in A means computing the probability that an attacker who observes a run of A can ascertain that its trace belongs to P. We consider specifications given as Interval Markov Chains (IMCs), which are underspecified Markov chains where probabilities on edges are only required to belong to intervals. Scheduling an IMC S produces a concrete implementation as a PTS and we define the worst case disclosure of secret P in S as the maximal disclosure of P over all PTSs thus produced. We compute this value for a subclass of IMCs and we prove that simulation between specifications can only improve the opacity of implementations.
jeudi 10 novembre, 14h, en salle Aurigny
Uli Schlachter
Reducing Linear Algebra in Petri Net Synthesis.
The goal in Petri net synthesis is to find a Petri net solving a given specification, or to conclude that no such net exists. More specifically, the Petri net should have a reachability graph that is isomorphic to a given labelled transition system. Petri net synthesis is based on region theory, which provides a linear-algebraic characterisation of the class of solvable transition systems by describing so-called separation problems. In this talk we will look at more direct characterisations. A purely graph-theoretical characterisation for 'state separation problems' is presented. This characterisation allows to better understand the substructures in a transition system that make state separation problems unsolvable. Another aspect will be targeted synthesis. For very special classes, such as finite, non-branching labelled transition systems having only two edge labels, linear-algebra-free characterisations can be found. We present an efficient characterisation of this class as a letter-counting criterion. This characterisation leads to a synthesis algorithm with quadratic time complexity.
jeudi 17 novembre, 14h
Thomas Chatain (LSV)
Anti-alignments in Conformance Checking - The Dark Side of Process Models
Conformance checking techniques asses the suitability of a process model in representing an underlying process, observed through a collection of real executions. These techniques su er from the well- known state space explosion problem, hence handling process models exhibiting large or even in nite state spaces remains a challenge. One important metric in conformance checking is to asses the precision of the model with respect to the observed executions, i.e., characterize the ability of the model to produce behavior unrelated to the one observed. By avoiding the computation of the full state space of a model, current techniques only provide estimations of the precision metric, which in some situations tend to be very optimistic, thus hiding real problems a process model may have. In this paper we present the notion of anti-alignment as a concept to help unveiling traces in the model that may deviate signi cantly from the observed behavior. Using anti-alignments, current estimations can be improved, e.g., in precision checking. We show how to express the problem of nding anti-alignments as the satis ability of a Boolean formula, and provide a tool which can deal with large models efficiently.
jeudi 24 novembre, 14h30 (visioconférence en salle de Direction - G103)
Thierry Coquand
Théorie cubique des types
Les travaux de Voevodsky suggèrent une extension de la théorie des types dépendants qui résout certains problèmes de modularité (égalité extensionnelle et quotients). La justification de cette extension est développée en utilisant le tiers-exclu et l’axiome du choix. Nous présentons un modèle de cette extension dans un cadre constructif, et qui peut s’écrire avec avantage directement comme une théorie des types. Cette théorie vérifie la propriété que tout terme clos de type entier se réduit sur un entier en forme canonique. Nous pouvons aussi donner une sémantique de l’opération de "troncation propositionnelle” dans ce cadre. On utilise une variation des ensembles simpliciaux (ensembles cubiques) et cette sémantique donne une structure de modèle (au sens de Quillen) sur ces ensembles cubiques de manière effective (travaux de Christian Sattler). Il n’est pas clair si une telle description effective est possible dans un cadre simplicial. Une question naturelle est si l’on peut utiliser un tel modèle pour établir des résultats d’indépendance (par exemple, de l’axiome du choix dénombrable), et nous discuterons quelques réponses partielles.
jeudi 1er Décembre, 14h salle Lipari
Serguei Lenglet
Howe's Method for Contextual Semantics.
We show how to use Howe’s method to prove that context bisimilarity is a congruence for process calculi equipped with their usual semantics. We apply the method to two extensions of HO-Pi, with passivation and with join patterns, illustrating different proof techniques.
jeudi 8 Décembre, 14h salle Aurigny
Alan Schmitt
Fully abstract encodings of lambda-calculus in HOcore through abstract machines
I will present fully abstract encodings of the call-by-name lambda-calculus into HOcore, a minimal higher-order process calculus which does not feature name restriction. We consider several equivalences on the lambda-calculus side—normal-form bisimilarity, applicative bisimilarity, and contextual equivalence—that we internalize into abstract machines in order to prove full abstraction.
jeudi 15 Décembre, 14h salle Markov
Lucca Hirschi
Partial Order Reduction for Security Protocols.
Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g., anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools. In this paper, we overcome this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.
jeudi 12 Janvier, 14h salle Sardaigne
Denis Kuperberg
Soundness in negotiations
Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. The present work investigates the complexity of deciding soundness for different classes of negotiations, as well as the design of efficient algorithms for deciding properties of sound negotiations. These algorithms can be applied for the analysis of workflow nets with data. This is joint work with Javier Esparza, Anca Muscholl and Igor Walukiewicz.
jeudi 19 Janvier, 14h salle Aurigny
Romain Brenguier
Optimal Assumptions for Synthesis
Controller synthesis is the process of constructing a correct system automatically from its specification. This often requires assumptions about the behaviour of the environment. It is difficult for the designer to identify the assumptions that ensures the existence of a correct controller, and doing so manually can lead to assumptions that are stronger than necessary. As a consequence the generated controllers are suboptimal in terms of generality and robustness. In this work, given a specification, we identify the weakest assumptions that ensures the existence of a controller. We also consider two important classes of assumptions: the ones that can be ensured by the environment and assumptions that speaks only about inputs of the systems. We show that optimal assumptions correspond to strongly winning strategies, admissible strategies and remorsefree strategies respectively. Based on this correspondence, we propose an algorithm for computing optimal assumptions that can be ensured by the environment.
jeudi 26 janvier, 14h en salle Aurigny
Mahsa Shirmohammadi
Minimal probabilistic automata have to make irrational choices
In this talk, we answer the question of whether, given a probabilistic automaton (PA) with rational transition probabilities, there always exists a minimal equivalent PA that also has rational transition probabilities. The PA and its minimal equivalent PA accept all finite words with equal probabilities. We approach this problem by exhibiting a connection with a longstanding open question concerning nonnegative matrix factorization (NMF). NMF is the problem of decomposing a given nonnegative n×m matrix M into a product of a nonnegative n×d matrix W and a nonnegative d×m matrix H. In 1993 Cohen and Rothblum posed the problem of whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries. As a corollary we obtain a negative answer to the question on rationality of minimal probabilistic automata. This talk is based on two papers in ICALP 2016 and SODA 2017.
jeudi 9 février, 14h00 en salle Aurigny
Florian Kammueller
Attack Tree Analysis for Insider Threats on the IoT using Isabelle
We illustrate and classify insider threats in relation to the Internet of Things (IoT) exhibiting attack vectors for their characterisation. To model the attacks we apply a method of formal modeling of Insider Threats in the interactive theorem prover Isabelle. On the classified IoT attack examples, we show how this logical approach can be used to make the models more precise and to analyse the previously identified Insider IoT attacks using Isabelle attack trees.
jeudi 16 février, 14h00 salle Aurigny
Christophe Chareton
Knowledge about the context and knowledge about the past, in a strategic context
In this talk, we investigate the question of mutual moves observations between agents, in a strategic context. This question is closely linked to the observance of the past for agents : an agent 'a' (partially) observes another agent's ('b') moves in a semantic game if at each time of the game she knows (something about) the strategy played by 'b' so far, Therefore, we introduce PKSL, a strategy logic with knowledge framework and backward looking time operators. We illustrate the characterization of moves observations and knowledge about the past in this setting.
jeudi 2 mars, 14h (salle à confirmer)
Ciprian Teodorov (Lab-STICC, ENSTA Bretagne)
Context-aware Verification with OBP
With an ever-increasing complexity, the verification of critical embedded systems is a challenging and expensive task. Among the available formal methods, model-checking offers a high level of automation and would thus lower the cost of this process. But, the scalability of this technique is hindered by the state-space explosion problem, which fueled the research community since its inception. To address this challenge, in the case of real size systems, the theoretical, the methodological and the algorithmic axes must be integrated. This presentation will overview the Context-aware Verification approach, which strives to do this by focusing on the identification, the isolation and the reification of the environment surrounding the studied system. It enables the use of specific algorithms with a major, positive, impact on the scalability of model-checking. http://www.obpcdl.org
jeudi 9 mars, 14h
Pierre-Yves Strub
Advanced Probabilistic Couplings for Differential Privacy
Differential Privacy is a promising formal approach to data privacy, which provides a quantitative bound on the privacy cost of an algorithm that operates on sensitive information. Several tools have been developed for the formal verification of differentially private algorithms, including program logics and type systems. However, these tools do not capture fundamental techniques that have emerged in recent years, and cannot be used for reasoning about cutting-edge differentially private algorithms. Existing techniques fail to handle three broad classes of algorithms: 1) algorithms where privacy depends on accuracy guarantees, 2) algorithms that are analyzed with the advanced composition theorem, which shows slower growth in the privacy cost, 3) algorithms that interactively accept adaptive inputs. In this talk, I will address these limitations with a new formalism extending apRHL, a relational program logic that has been used for proving differential privacy of non-interactive algorithms, and incorporating aHL, a (non-relational) program logic for accuracy properties. I will illustrate the approach through a running examples, which exemplify the three classes of algorithms and explores new variants of the Sparse Vector technique, a well-studied algorithm from the privacy literature. The logic has been implemented in EasyCrypt [1], and the examples formally verified in this tool. [1] https://www.easycrypt.info/
jeudi 16 mars, 14h, Salle Aurigny (D165)
Ocan Sankur
An Abstraction Technique for Parameterized Verification of Leader Election Protocols: Application to Flooding Time Synchronization Protocol
We consider distributed timed systems that implement leader election protocols which are at the heart of clock synchronization protocols. We develop abstraction techniques for parameterized model checking of such protocols under arbitrary network topologies, where nodes have independently evolving clocks. We implemented our technique within NuSMV and applied it to model check the root election part of the flooding time synchronisation protocol (FTSP), and obtained significantly improved results compared to previous work. We were able to verify the protocol for all topologies in which the distance to the node to be elected leader is bounded by a given parameter. Joint work with J.-P. Talpin. Paper to be presented at TACAS'17.
jeudi 30 mars, 14h, Salle Aurigny (D165)
Jérémie Chalopin
A counterexample to Thiagarajan's conjecture on regular event structures
We provide a counterexample to a conjecture by Thiagarajan (1996 and 2002) that regular prime event structures correspond exactly to finite 1-safe Petri nets. The same counterexample is used to disprove a closely related conjecture by Badouel, Darondeau, and Raoult (1999) that domains of regular event structures with bounded #-cliques are recognizable by finite trace automata. Event structures, trace automata, and Petri nets are fundamental models in concurrency theory. There exist nice interpretations of these structures as combinatorial and geometric objects and both conjectures can be reformulated in this framework. Namely, from a graph theoretical point of view, the domains of prime event structures correspond exactly to median graphs; from a geometric point of view, these domains are in bijection with CAT(0) cube complexes. A necessary condition for both conjectures to be true is that domains of respective regular event structures admit a regular nice labeling (which corresponds to a special coloring of the hyperplanes of the associated CAT(0) cube complex). To disprove these conjectures, we describe a regular event domain (with bounded #-cliques) that does not admit a regular nice labeling. Our counterexample is derived from an example by Wise (1996 and 2007) of a nonpositively curved square complex X with six squares, whose edges are colored in five colors, and whose universal cover X˜ is a CAT(0) square complex containing a particular plane with an aperiodic tiling.
jeudi 13 avril, 14h, Salle Aurigny (D165)
Didier Lime
Coverability Synthesis in Parametric Petri Nets
We introduce parameters in Petri nets, that can be used instead of the weights of some arcs or the initial marking of some places. This allows for a greater flexibility in modelling and more complete answers to model-checking questions. We focus here on two parametric extensions of the coverability property: "does there exists a value for the parameters such that some marking is coverable?" and "is some marking coverable for all possible values of the parameters?". We prove that these problems are undecidable in the general case, and therefore propose some syntactic subclasses, defined by restricting the use of parameters, for which we can obtain decidability and actually prove EXSPACE-completeness. In addition, when restricting parameters to input weights the "solution set" of all the parameter values for which some marking is coverable is downward-closed and we prove that we can in that case use an algorithm from Valk and Jantzen to effectively compute a finite basis of the solution set. We finally also provide a similar result when restricting parameters to output weights.
mercredi 26 avril, 14h en salle Aurigny
Philippe Dague
Using Incremental SAT for Testing Diagnosability of Distributed DES
We extend in this work the existing approach to analyse diagnosability in discrete event systems(DES) using satisfiability algorithms (SAT), in order to analyse the diagnosability in distributed DES (DDES) and we test this extension. For this, we handle observable and non observable communication events at the same time. We also propose an adaptation to use incremental SAT over the existing and the extended approaches to overcome some of the limitations, especially concerning the length and the distance of the cycles that witness the non diagnosability of the fault, and improve the process of dealing with the reachability limit when scaling up to large systems.
jeudi 27 avril, 14h en salle Markov
Josef Widder
Model Checking Fault-tolerant Distributed Algorithms
Distributed algorithms have numerous mission-critical applications in embedded avionic and automotive systems, cloud computing, computer networks, hardware design, and the internet of things. Although distributed algorithms exhibit complex interactions with their computing environment and are difficult to understand for human engineers, computer science has developed only very limited tool support to catch logical errors in distributed algorithms at design time. In the last two decades we have witnessed a revolutionary progress in software model checking due to the development of powerful techniques such as abstract model checking, SMT solving, and partial order reduction. Still, model checking of fault-tolerant distributed algorithms poses multiple research challenges, most notably parameterized verification: verifying an algorithm for all system sizes and different combinations of faults. I will present our recent results in this area which extend and combine abstraction, partial orders, and bounded model checking. Our results demonstrate that model checking has acquired sufficient critical mass to build the theory and the practical tools for the formal verification of fault-tolerant distributed algorithms. Joint work with Igor Konnov, Marijana Lazic, and Helmut Veith
jeudi 18 mai, 14h en salle Aurigny
Loïc Hélouët
Combining Free choice and Time in Petri Nets
Time Petri nets (TPNs) are a classical extension of Petri nets with timing constraints attached to transitions, for which most verification problems are undecidable. We consider TPNs under a strong semantics with multiple enabling of transitions. We focus on a structural subclass of unbounded TPNs, where the underlying untimed net is free choice, and show that it enjoys nice properties in the timed setting under a multi-server semantics. In particular, we show that the questions of firability (whether a chosen transition can fire), and termination (whether the net has a non-terminating run) are decidable for this class. We then consider the problem of robustness under guard enlargement, i.e., whether a given property is preserved even if the system is implemented on an architecture with imprecise time measurement. This question was studied for TPNs, and decidability of several problems was obtained for bounded classes of nets. We show that robustness of fireablity is decidable for unbounded free choice TPNs with a multi-server semantics. Joint work with S. Akshay and R. Phawade.
jeudi 1er juin, 14h en salle Aurigny
Laurie Ricker (Mount Allisson University)
Parity Architectures for Discrete-Event Systems
Existing decentralized decision-making architectures for diagnosis and control (that operate in the absence of communication between diagnosers) use either disjunction or conjuction to combine decisions of the local diagnosers or controllers in reaching an overall conclusion about whether or not a fault occurred or when to disable an event. The observational property of interest for languages in this architecture is more generally referred to as inference diagnosability or inference observability. We propose a parity-based architecture that uses XOR, which can be used for both diagnosis and control, to extend the current decision-making capabilities of decentralized agents. A new family of languages that lie beyond those that are inference-diagnosable or inference observable is defined. Finally, a verification algorithm for this new observational property is provided. This is joint work with Finn Lidbetter (Mount Allison) and Herve Marchand.
jeudi 8 juin, 14h en salle Aurigny
Simon Lunel
Compositional proofs in differential dynamic logic
Modularity and composability are essential properties to facilitate and scale the design of cyber-physical systems from the specification of hybrid, discrete and continuous, components. Modularity is essential to break down a system model into comprehensible and manageable component specifications. Composability is essential to design a system from component models while preserving their verified properties, expressed as assume-guarantee contracts. I will present our recent results which address the specification of hybrid system using Platzer's differential dynamic logic. We define a new composition operator in differential dynamic logic and prove that it is associative and commutative. Plus, we provide a theorem which characterizes necessary conditions to automate the proof that composed components satisfy the composition of their individual contracts, enabling modular and compositional verification. We case-study our composition operator by considering the modular and detailed specification of a cruise controller in KeYmaera X. (Joint work with Jean-Pierre Talpin and Benoit Boyer)
jeudi 15 juin, 14h en salle Aurigny
Béatrice Bérard
The Complexity of Diagnosability and Opacity Verification for Petri Nets
Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.
Vendredi 30 juin, 14h en salle Lipari
Abdallah Saffidine
The Parameterized Complexity of Positional Games
We study the parameterized complexity of several positional games. Our main result is that Short Generalized Hex is W[1] -complete parameterized by the number of moves. This solves an open problem from Downey and Fellows’ influential list of open problems from 1999. Previously, the problem was thought of as a natural candidate for AW[*] -completeness. Our main tool is a new fragment of first-order logic where universally quantified variables only occur in inequalities. We show that model-checking on arbitrary relational structures for a formula in this fragment is W[1] -complete when parameterized by formula size. We also consider a general framework where a positional game is represented as a hypergraph and two players alternately pick vertices. In a Maker-Maker game, the first player to have picked all the vertices of some hyperedge wins the game. In a Maker-Breaker game, the first player wins if she picks all the vertices of some hyperedge, and the second player wins otherwise. In an Enforcer-Avoider game, the first player wins if the second player picks all the vertices of some hyperedge, and the second player wins otherwise. Short Maker-Maker, Short Maker-Breaker, and Short Enforcer-Avoider are respectively AW[*] -, W[1] -, and co-W[1] -complete parameterized by the number of moves. This suggests a rough parameterized complexity categorization into positional games that are complete for the first level of the W -hierarchy when the winning condition only depends on which vertices one player has been able to pick, but AW[*] -complete when it depends on which vertices both players have picked. However, some positional games with highly structured board and winning configurations are fixed-parameter tractable. We give another example of such a game, Short k-Connect, which is fixed-parameter tractable when parameterized by the number of moves. This is joint work with Édouard Bonnet, Serge Gaspers, Antonin Lambilliotte, and Stefan Rümmele (ICALP 2017). Bio: Abdallah Saffidine is an ARC DECRA Fellow and a Research Associate at the University of New South Wales, Sydney, Australia. He works in the Artificial Intelligence and Algorithms groups. He arrived at UNSW in 2013 as a postdoc with Pr. Michael Thielscher and obtained his PhD from the Universite Paris-Dauphine, France, under the supervision of Pr. Tristan Cazenave. Abdallah has a wide range of interests from games, planning, and other areas of decision-making to logic, complexity and other areas of theory.