Groupe de Travail

Les séances du groupe de travail ont habituellement lieu à Luminy, en salle salle de réunion du LIF (6ième étage de TPR1), tous les jeudis à 10h00.

Contacter le coordinateur (gt-move (at) lif univ-mrs fr) pour recevoir les annonces.

Sessions usually take place at Luminy, meeting room of LIF (floor 6th of building TPR1) on thursday, at 10h00. Write to the coordinator (gt-move (at) lif univ-mrs fr) to be on the announcement list.

Mai 2013

Serge Haddad : The steady-state control problem for Markov decision processes

 Date : Jeudi 30 mai à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Serge Haddad (LSV, ENS Cachan)

We address a control problem for probabilistic models in the setting of Markov decision processes (MDP). We are interested in the steady-state control problem which asks, given an ergodic MDP M and a distribution delta, whether there exists a (history-dependent randomized) policy pi ensuring that the steady-state distribution of M under pi is exactly delta. We first show that stationary randomized policies suffice to achieve a given steady-state distribution. Then we infer that the steady-state control problem is decidable for MDP, and can be represented as a linear program which is solvable in PTIME. This decidability result extends to labeled MDP (LMDP) where the objective is a steady-state distribution on labels carried by the states, and we provide a PSPACE algorithm. We also show that a related steady-state language inclusion problem is decidable in EXPTIME for LMDP. Finally, we prove that if we consider MDP under partial observation (POMDP), the steady-state control problem becomes undecidable.

Joint work with S. Akshay (IIT Bombay), Nathalie Bertrand and Loïc Hélouët (INRIA Rennes)

Jérôme Fortier : La règle de coupure dans les preuves circulaires

 Date : Jeudi 23 mai à 14h00, Amphi 12 (Bâtiment B), Luminy.

 Orateur : Jérôme Fortier (Doctorant, LIF)

Les preuves circulaires, dans lesquelles certaines conclusions peuvent être démontrées à partir d’elles-mêmes, furent introduites dans [1] pour étudier la calculabilité dans les modèles du mu-calcul, soit avec les opérations suivantes : produits et coproduits finis, algèbres initiales et coalgèbres terminales. Le calcul en question, sans règle de coupure, était correct et complet, mais pas plein, c’est-à-dire qu’il ne représentait pas toute la structure des modèles catégoriques visés.

On remplit donc le système de preuves circulaires en introduisant la règle de coupure. La nouvelle syntaxe permet une procédure d’élimination des coupures qui produit un arbre infini, modélisant ainsi le calcul recherché.

Plusieurs directions de recherche en découlent, qui sauront, on l’espère, intéresser autant les logiciens que les informaticiens !

[1] L. Santocanale, A calculus of circular proofs and its categorical semantics, in : M. Nielsen, U. Engberg (eds.), FOSSACS 2002, No. 2303 in LNCS, Springer, 2002.

Arnaud Labourel : Progress and challenges for labeling schemes

 Date : Jeudi 16 mai à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Arnaud Labourel (LIF)

A fundamental question in Distributed Computing is to understand how localized and how much information are required to solve a task on a network. Typically, if the distance between any pair x,y of nodes in a network is asked, we would like to know which minimal information about x and y in the network are needed. The goal in labeling schemes is precisely to understand how much information must be attached to the nodes (formalized as labels) to solve a graph problem assuming the answer can be determined solely on the basis of the labels of the nodes invoked in the query. In this talk, I give a survey on labeling schemes, present some results with their techniques, and highlight new challenges.

Nathanaël Fijalkow : Boundedness games

 Date : Jeudi 2 mai à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Nathanaël Fijalkow (Doctorant, LIAFA)

In this talk, I will discuss some recent developments about boundedness games, which appear in different contexts, for instance in the study of regular cost-functions as defined by Thomas Colcombet.

They are two-player games featuring counters that can be incremented, reset of left unchanged, and where the first player’s objective is that the counters remain bounded along the play. They can be played over finite graphs or infinite graphs, for instance over pushdown graphs. I am interested in the following questions : deciding the winner, proving the existence of finite-memory strategies, and constructing such strategies.

Based on joint works with Krishnendu Chatterjee, Thomas Colcombet, Florian Horn and Martin Zimmermann.

Mars 2013

Pierre-Alain Reynier : From Two-Way to One-Way Finite State Transducers

 Date : Jeudi 21 mars à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Pierre-Alain Reynier (MCF, LIF)

Any two-way finite state automaton is equivalent to some one-way finite state automaton. This well-known result, shown by Rabin and Scott and independently by Shepherdson, states that two-way finite state automata (even non-deterministic) characterize the class of regular languages. It is also known that this result does not extend to finite string transductions : (deterministic) two-way finite state transducers strictly extend the expressive power of (functional) one-way transducers. In particular deterministic two-way transducers capture exactly the class of MSO-transductions of finite strings. In this paper, we address the following definability problem : given a function defined by a two-way finite state transducer, is it definable by a one-way finite state transducer ? By extending Rabin and Scott’s proof to transductions, we show that this problem is decidable. Our procedure builds a one-way transducer, which is equivalent to the two-way transducer, whenever one exists.

Joint work with Emmanuel Filiot, Olivier Gauwin and Frédéric Servais

Février 2013

Adrien Boiret : Learning Rational Functions using Transducers with Lookahead

 Date : Jeudi 21 février à 10h00, Amphi 1 (1er étage du bâtiment A), Luminy.

 Orateur : Adrien Boiret (Doctorant, INRIA Lille)

The learning problem on transducers consist of guessing a transducer when given a set of examples of its behavior (input/output pairs). If solved on tree transducers, it can be used to understand XML queries from users without requiring them to know XQL.

However, this problem remains unsolved even for some classes of string transducers.

Rational functions are transformations from words to words that can be de-fined by string transducers. Rational functions are also captured by deterministic string transducers with lookahead. We show that the class of rational functions can be learned in the limit with polynomial time and data, when represented by string transducers with lookahead in a normal form that we introduce.

Luigi Santocanale : Permutohèdres et associahèdres, tous ce que vous voulez savoir (deuxième partie)

 Date : Jeudi 14 février à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Luigi Santocanale (Prof., LIF)

Dans le premier exposé, je vous ai présenté l’ordre faible de Bruhat sur les permutations, et l’ordre sur les arbres binaires. J’ai expliqué quel est leur lien strict de parenté.

L’objectif principal de la séance dernière était la découverte de l’OD-graph de ces deux treillis. Il s’agit d’un outil fondamental pour les résultats concernant les plongeabilité des treillis dans un permutohèdre/associahèdre, que j’exposerai cette semaine.

Luigi Santocanale : permutohèdres et associahèdres, tous ce que vous voulez savoir (et que je sais)

 Date : Jeudi 7 février à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Luigi Santocanale (Prof., LIF)

Dans ce premier exposé, je vous présenterai l’ordre faible de Bruhat sur les permutations, et l’ordre sur les arbres binaires. J’expliquerai quel est leur lien strict de parenté.

L’objectif principal de cette séance sera la découverte de l’OD-graph de ces deux treillis ; il s’agit d’un outil fondamental pour les résultats concernant les plongeabilité des treillis dans un permutohèdre/associahèdre, que j’exposerai la semaine suivante (ou jeudi, s’il y aura le temps).

Janvier 2013

Youssouf Oualhadj : Deciding the Value 1 Problem for Probabilistic Leaktight automata

 Date : Jeudi 31 janvier à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateurs : Youssouf Oualhadj (Postdoc, LIF)

The value 1 problem is a decision problem for probabilistic automata over finite words : given a probabilistic automaton A, are there words accepted by A with probability arbitrarily close to 1 ?

This problem was proved undecidable recently. We sharpen this result, showing that the undecidability holds even if the probabilistic automata have only one probabilistic transition.

Our main contribution is to introduce a new class of probabilistic automata, called leaktight automata, for which the value 1 problem is shown decidable (and PSPACE-complete). We construct an algorithm based on the computation of a monoid abstracting the behaviors of the automaton, and rely on algebraic techniques developed by Simon for the correctness proof. The class of leaktight automata is decidable in PSPACE, subsumes all subclasses of probabilistic automata whose value 1 problem is known to be decidable (in particular deterministic automata), and is closed under two natural composition operators.

Séverine Fratani : Langages reconnaissables de niveau k

 Date : Jeudi 24 janvier à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Séverine Fratani (MCF, LIF)

Les ensembles reconnaissables par automates finis sont également les langages définissables en MSO, et les ensembles de piles (vus comme des mots) générés par des automates à pile. On propose une notion de langages reconnaissables de niveau k. Ces langages sont une généralisation du langage de Dyck, ils admettent trois caractérisations généralisant celle des langages reconnaissables : ce sont les langages reconnus par automates finis utilisant un certain type d’oracle, les langages définissables en MSO dans un arbre particulier, les ensembles de piles de niveau k (vus comme des mots) générés par des automates à pile de niveau k.

Novembre 2012

Janusz Malinowski : Répétition de thèse, Algorithmes pour la Synthèse et le Model Checking

 Date : Jeudi 22 novembre à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Janusz Malinowski (Doctorant, LIF)

Cette thèse a pour objet l’étude d’algorithmes permettant l’exploration de systèmes de grande taille tant dans le domaine de la synthèse de contrôleur que de la vérification. Nous avons étudié une approche discrète de la synthèse de contrôleurs pour les systèmes hybrides permettant la manipulation de dynamiques non-linéaires. Dans cette approche, les états sont regroupés dans une partition finie au prix d’une sur-approximation non déterministe de la relation de transition. Nous avons développé des algorithmes permettant de réduire drastiquement l’explosion du nombre d’états générée par la discrétisation en exploitant des propriétés structurelles des systèmes ODE. Ces algorithmes sont basés sur une approche hiérarchique du problème de la synthèse en le résolvant pour des sous problèmes et en utilisant ces résultats pour réduire l’espace d’états du problème global. Dans avons aussi combiné des objectifs de contrôle de sécurité et de vivacité pour s’approcher d’une stabilisation. Des résultats implémentés sur un prototype viennent montrer l’intérêt de cette approche.

Pour la vérification, nous avons étudié le problème du modèle checking d’automates temporisés basé sur la résolution SAT. Nous avons exploré des solutions alternatives pour le codage des réductions SAT basées sur des exécutions parallèles de transitions indépendantes. Alors qu’une telle optimisation a déjà été étudiée pour les systèmes discrets, sa transposition aux automates temporisés interroge sur ce que signifie d’exécuter des transitions temporisées "en parallèle". Une approche intuitive serait de considérer que des transitions en parallèle ont lieu au même instant (synchrones). Toutefois il est possible de relâcher cette condition et nous avons montré trois sémantiques différentes pour les séquences temporisées avec des transitions parallèles. Nous montrons la correction des sémantiques et décrivons des résultats expérimentaux réalisés avec notre prototype.

Florent Avellaneda : Vérifier la terminaison structurelle d’un VASS

 Date : Jeudi 15 novembre à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Florent Avellaneda (Doctorant, LIF)

Un Vector Addition System with State (VASS) est un graphe orienté où chaque arc est pondéré par un vecteur d’entiers. Généralement considéré comme équivalant à un réseau de Petri, nous verrons que cela n’est pas vrai pour les propriétés structurelles. Nous verrons un algorithme permettant de résoudre la terminaison structurelle d’un VASS en temps polynômial.

Octobre 2012

Matteo Mio : Probabilistic modal mu-calculus with independent product

 Date : Lundi 29 octobre à 14h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateur : Matteo Mio (INRIA, LIX)

The modal µ-calculus (Lµ) is the logic obtained by extending standard propositional modal logic with least and greatest fixed points operators. This logic was intensively studied in the last 20 years, as it allows the expression of many interesting properties of labeled transition systems. The probabilistic modal µ-calculus (pLµ) is a generalization of Lµ, designed for expressing properties of probabilistic labeled transition systems. In this talk I will discuss an extension of pLµ, called probabilistic modal µ-calculus with independent product, which can express more complex properties of practical interest. We provide two semantics for this extended logic : one denotational and one based on a new kind of games which we call Tree games. The main result is the equivalence of the two semantics. The proof is carried out in ZFC set theory extended with Martin’s Axiom at the first uncountable cardinal.

David Ilcinkas : Connaissance initiale et résultats d’impossibilité en algorithmique distribuée

 Date : Mercredi 24 octobre à 14h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateurs : David Ilcinkas (CNRS, LaBRI)

Dans le cadre de l’algorithmique distribuée, un processus ne connaît généralement pas exactement l’instance du problème lorsqu’il démarre son exécution. Ainsi de nombreux algorithmes distribuées supposent que chaque processus dispose initialement d’une certaine connaissance sur l’instance, par exemple une borne supérieure sur la taille du réseau. Pour certains problèmes, il semble que l’absence d’un certain type de connaissance initiale rende le problème impossible à résoudre. Nous nous intéresserons dans cet exposé à des formalisations possibles du concept de connaissance initiale qui permettraient de pouvoir prouver de tels résultats d’impossibilité.

Youssouf Oualhadj : Computing Optimal Strategies for Markov Decision Processes with Parity and Positive-Average Conditions

 Date : Jeudi 4 octobre à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateurs : Youssouf Oualhadj (LIF)

We study Markov decision processes (one-player stochastic games) equipped with parity and positive-average conditions. In these games, the goal of the player is to maximize the probability that both the parity and the positive-average conditions are fulfilled. We show that the values of these games are computable in polynomial time. We also show that optimal strategies exist, require only finite memory and can be effectively computed. Joint work with Hugo Gimbert and Soumya Paul.

Septembre 2012

Nicolas Baudru : On the treewidth of book embeddings

 Date : Jeudi 27 septembre à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateurs : Nicolas Baudru (LIF)

Dans cet exposé, je présenterai des résultats obtenus dernièrement avec Séverine. On y entendra parler principalement de "treewidth" et de "book embedding".

La treewidth d’un graphe est une valeur indiquant à quel point un graphe est proche d’un arbre. Un n-book est un espace topologique consistant en une ligne (appelée "spine") et n demi-plans (appelés "pages") collés à la ligne par leur frontière. Un n-book embedding, lorsqu’il existe, représente le dessin d’un graphe dans un book de n pages de telle sorte que chaque sommet est dessiné sur la "spine", chaque arête est entièrement dessinée sur une page, et les arêtes ne se coupent pas.

Un résultat de V. Dujmovic et D.R. Wood (2007) énonce que tout graphe de treewidth n peut être dessiné dans un book de n+1 pages. La réciproque est généralement fausse. Un autre résultat de H.L. Bodlaender dans les graphes planaires montre qu’un "k-outerplanar embedding" a une treewidth bornée par 3k-1 (*).

S’inspirant de (*), nous transposons la notion de k-outerplanar vers les books pour définir les k-outerforest book embeddings. Nous montrons alors que tout k-outerforest book embedding a une treewidth exponentielle en k. Nous présentons enfin comment ce résultat peut être utilisé pour décider du vide pour des classes de multi-pushdown automata.

Laurent Braud : Ordinaux dans la hiérarchie à pile

 Date : Jeudi 13 septembre à 10h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateurs : Laurent Braud (LIF)

La hiérarchie à pile est un ensemble de graphes aux propriétés intéressantes, notamment parce qu’elle s’exprime de façons très différentes et que la théorie MSO de chaque graphe est décidable. Je présenterai les résultats principaux de ma thèse, à savoir la caractérisation des ordinaux (vus comme des graphes) dans cette hiérarchie, ce qui donne une idée de sa "complexité". Le même résultat s’applique également à des structures un peu plus générales, les ordres linéaires dispersés.

Juillet 2012

Arnaud Labourel : Collecting information by power-aware mobile agents

 Date : Jeudi 12 juillet à 13h30, salle de réunion du LIF (6ième étage de TPR1), Luminy.

 Orateurs : Arnaud Labourel (LIF)

In this talk, we consider mobile agents inside a weighted network. At the beginning, each agent has its initial information. The goal of the agents is to gather all the information into one agent. We focus on one quality benchmark for this problem : the maximal distance traveled by an agent. We study the question in the centralized and the distributed setting. We give a linear-time centralized algorithm for line networks. We also give a 2-competitive distributed algorithm achieving convergecast for tree networks. The competitive ratio of 2 is proved to be the best possible for this problem. We show that already for the case of tree networks the centralized problem is strongly NP-complete. We give a 2-approximation centralized algorithm for general graphs.

Juin 2012

Amélie Stainer : Emptiness and Universality Problems in Timed Automata with Positive Frequency

 Date : Jeudi 7 juin à 13h30, salle de séminaire (R163), CMI.
 Orateurs : Amélie Stainer (INRIA Rennes)

The languages of infinite timed words accepted by timed automata are traditionally defined using Büchi-like conditions. These acceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the proportion of time spent in the accepting states. We study various properties of timed languages accepted with positive frequency, and in particular the emptiness and universality problems.

Mai 2012

Nabil Layaida et Pierre Geneves : Analyse statique de feuille css

 Date : Jeudi 31 mai à 13h30, salle de séminaire (R163), CMI.
 Orateurs : Nabil Layaida (INRIA, LIG) et Pierre Geneves (CNRS, LIG)

In this talk, I will introduce a topic that has been terribly under-researched, yet being the focus of one of the most widely used web standard everyday : cascading style sheets (CSS). Developing and maintaining style sheets is an important issue to web developers as they suffer from the lack of rigorous methods. Most existing means rely on validators that check syntactic rules, and on runtime debuggers that check the behavior of a CSS style sheet on a particular document instance. However, the aim of most style sheets is to be applied to an entire set of web pages, usually defined by some schema. While usual debugging tools help reducing the number of bugs, they do not ultimately allow to prove properties over the whole set of documents to which the style sheet is intended to be applied. In this talk, I will present a novel approach that we propose to fill this lack. We introduce ideas borrowed from the fields of logic and compile-time verification for the analysis of CSS style sheets. We present an original method and a tool based on recent advances in tree logics. Specifically, I will show how sophisticated styling information can be captured by the mean of mu-calculus sentences. The tool is capable of statically detecting a wide range of errors (such as empty CSS selectors and semantically equivalent selectors), as well as proving properties related to sets of documents (such as coverage of styling information). This new tool has several applications ranging from ensuring a higher level of quality of CSS style sheets to verifying accessibility issues for web sites on particular devices. I will also highlight perspectives for further work.

Mathieu Caralp : Visibly Pushdown Automata with Multiplicities : Finiteness and K-Boundedness

 Date : Jeudi 10 mai à 13h30, salle de séminaire (R163), CMI.
 Orateur : Mathieu Caralp (LIF)

We propose an extension of visibly pushdown automata by means of weights (represented as positive integers) associated with transitions, called visibly pushdown automata with multiplicities. The multiplicity of a computation is the product of the multiplicities of the transitions used along this computation. The multiplicity of an input is the sum of the ones of all its successful computations. Finally, the multiplicity of such an automaton is the supremum of multiplicities over all possible inputs. We show the problem of deciding whether the multiplicity of an automaton is finite can be solved in PTIME. We also consider the K-boundedness problem, i.e. whether the multiplicity is bounded by K : we prove this problem to be EXPTIME- complete if K is part of the input and in PTIME if K is fixed. As visibly pushdown automata are closely related to tree automata, we discuss deeply the relationship of our extension with weighted tree automata.

Avril 2012

Emmanuel Filiot : Exploiting Structure in LTL Synthesis

 Date : Jeudi 12 avril à 13h30, salle de séminaire (R163), CMI.
 Orateur : Emmanuel Filiot (ULB)

The aim of program synthesis is to automatically generate a program that satisfies a given specification, in contrast to program verification, for which both the specification and the program are given as input. The underlying goal is to improve program reliability and optimize design constraints, like time and human errors, and to get rid of the low-level programming tasks, by replacing them with the design of high-level specifications. The old dream of automatic synthesis, which among others was shared by Church, is difficult to realize for general-purpose programming languages. However in recent years, there has been a renewed interest in feasible methods for the synthesis of application specific programs, which have been, for instance, applied to reactive systems, distributed systems, programs manipulating arithmetic or concurrent data-structures.

Reactive systems are non-terminating programs that continuously interact with their environment. They arise both as hardware and software, and are usually part of safety-critical systems, for example microprocessors, air traffic controllers, programs to monitor medical devices, or nuclear plants. It is therefore crucial to guarantee their correctness. The temporal logic LTL is a very important abstract formalism to describe properties of reactive systems. As shown by Pnueli and Rosner in 89, the synthesis of reactive systems from LTL specifications is a 2-Exptime complete problem.

In this talk, I will present recent progresses in LTL synthesis based on a bounded synthesis approach inspired by bounded model-checking, and show that the high worst-case time complexity of LTL synthesis does not handicap its practical feasibility. This is achieved by exploiting the structure underlying the automata constructions used to solve the synthesis problem.

Akka Zemmari : Analyse des algorithmes distribués probabilistes

 Date : Jeudi 5 avril à 13h30, salle de séminaire (R163), CMI.
 Orateur : Akka Zemmari (LaBRI)

Dans cet exposé, on s’intéresse à la conception et à l’analyse des algorithmes distribués probabilistes. Ces algorithmes ont une description "simple" mais leur analyse (complexité en moyenne ou complexité avec forte probabilité) est une tâche assez ardue.

Je présenterai quelques résultats récents concernant le problème de l’élection, le problème de l’ensemble indépendant maximal (MIS) et le problème de la coloration de graphes. Les résultats établissent des bornes inférieures et des bornes supérieures sur la complexité des algorithmes probabilistes solution de ces problèmes.

Ensuite, je présenterai en détail une étude du problème de la coloration distribuée de graphes. Je présenterai un algorithme probabiliste optimal en temps et en taille de messages pour résoudre ce problème.

Mars 2012

Emmanuel Godard : Expressivity of Time-Varying Graphs and the Power of Waiting in Dynamic Networks

 Date : Jeudi 29 mars à 13h30, salle de séminaire (R163), CMI.
 Orateur : Emmanuel Godard (LIF)

In infrastructure-less highly dynamic networks, computing and performing even basic tasks (such as routing and broadcasting) is a very challenging activity due to the fact that connectivity does not necessarily hold,and the network may actually be disconnected at every time instant. Clearly the task of designing protocols for these networks is less difficult if the environment allows waiting (i.e., it provides the nodes with store-carry-forward-like mechanisms such as local buffering) than if waiting is not feasible. No quantitative corroborations of this fact exist (e.g., no answer to the question : how much easier ?).

In this paper, we consider these qualitative questions about dynamic networks, modeled as time-varying (or evolving) graphs, where edges exist only at some times. We examine the difficulty of the environment in terms of the expressivity of the corresponding time-varying graph ; that is in terms of the language generated by the feasible journeys in the graph.

We prove that the set of languages L_nowait when no waiting is allowed contains all computable languages. On the other end, using algebraic properties of quasi-orders, we prove that L_wait is just the family of regular languages. In other words, we prove that, when waiting is no longer forbidden, the power of the accepting automaton (difficulty of the environment) drops drastically from being as powerful as a Turing machine, to becoming that of a Finite-State machine. This (perhaps surprisingly large) gap is a measure of the computational power of waiting.

En collaboration avec Arnaud Casteigts, Paola Flocchini, Nicola Santoro, Masafumi Yamashita

Florian Huc : On distributed computing with Byzantine adversary

 Date : Jeudi 22 mars à 13h30, salle de séminaire (R163), CMI.
 Orateur : Florian Huc (LPD, EPFL)

The history of distributed computing is strongly tied to the assumption of a static network composed predominantly of honest nodes. Yet, modern distributed systems not only are dynamic but exhibit a high level of churn. In this talk, I will present a solution to achieve distributed computing in a highly dynamic environment despite the presence of an adversary controlling a large fraction of the nodes. Somewhat surprisingly, we prove that it is possible to efficiently maintain clusters of nodes with a majority of honest ones in each, within a system whose size can vary polynomially compared to its initial size. So far, dealing with such a highly dynamic setting has been an open problem in distributed computing. Our construction provides a basic abstraction enabling for the first time several types of distributed coordination in a highly dynamic setting, such as peer sampling, broadcast, agreement and aggregation. In a nutshell, we are the first to achieve dynamic clustering with a low complexity, namely with a communication cost induced by each node arrival or departure that is polylogarithmic, with respect to N, the maximal size of the system, and this in presence of a static Byzantine adversary controlling a fraction b ≤ 1/2l²-e of the nodes (for some fixed constants l>√2 and e>0, independent of N). The clusters maintained are of size O(log² N), and all contain a majority of honest nodes with high probability. Our approach built on two algorithms : NOW (for Neighbors On Watch), which preserves the desired properties of the partition in the presence of high churn (up to a polynomial increase and decrease of the number of nodes), and OVER (for Over-Valued Erdös-Rényi graph), which maintains an overlay with high expansion coefficient and low degree on the graph of clusters.

Février 2012

Julien Ferté : Complexity of Graded Patterns

 Date : Jeudi 16 février à 13h30, salle de séminaire (R163), CMI.
 Orateur : Julien Ferté (LIF)

Patterns are tree schemata for unranked trees (ordered or unordered) that are used to express modifications of active XML documents using a suitable notion of rewriting. A pattern is a labelled tree where the relations between nodes are | (immediate child) or || (descendant). Three problems are relevant in rewriting active XML documents :
 model-checking that checks if a given document satisfies the pattern
 pattern satisfiability that checks if there is a document that satisfies a pattern (resp. a boolean combination of patterns)
 pattern satisfiability modulo a DTD which is the same problem with the additional constraint that the document must satisfy a DTD.

We study these problems for graded patterns, that extend patterns with constraints ≥c,=c, ≤c on the number of children of some nodes.

Yann Strozecki : Complexité d’énumération : méthodes logiques et algébriques

 Date : Jeudi 9 février à 13h30, salle de séminaire (R163), CMI.
 Orateur : Yann Strozecki (Univ. Paris 11)

Je vais présenter dans cet exposé des problèmes d’énumérations, c’est à dire qu’on veut lister toutes les solutions d’un problème. Le but est de réaliser cette tâche avec un algorithme de complexité la plus faible possible. Dans ce cadre on s’intéresse à la fois au temps total de l’algorithme et au délai entre deux solutions.

Dans une première partie je montrerai comment représenter certains problèmes d’énumération par des formules du premier ordre contenant des variables libres du second ordre. On verra que la complexité d’énumération dépend du nombre de quantificateurs ainsi que de la structure sur lequel ces formules sont évaluées (degré bornée, largeur arborescente bornée, ...).

Dans un deuxième temps je présenterai des algorithmes probabilistes qui permettent d’énumérer les monômes d’un polynôme. Je montrerai ensuite comment on peut utiliser ces algorithmes pour résoudre des problèmes sur des graphes, des hypergraphes, des automates probabilistes.

Akshay Sundararaman : Decidability issues for time-constrained message sequence graphs

 Date : Jeudi 2 février à 13h30, salle de séminaire (R163), CMI.
 Orateur : Akshay Sundararaman (INRIA Rennes)

Systems involving both time and concurrency are notoriously difficult to analyze. Existing decidability results apply in settings where clocks on different processes cannot be compared or where the set of timed executions is regular. We prove new decidability results for timed concurrent systems, requiring neither restriction. Message sequence graphs (MSGs) are a high-level formalism which can be used to describe infinite collections of interacting scenarios. We consider MSGs enriched with timing constraints between events (TCMSGs), as our basic model for timed and concurrent systems. Several properties are known regarding TCMSGs, when they are structurally restricted to have only a regular set of behaviors. However, for general TCMSGs, even the emptiness problem of checking whether the set of timed-executions of a TCMSG is empty is known to be undecidable.

In this light, we come up with arguably mild restrictions on TCMSGs, which allow for non-regular sets of behaviors and still have effectively decidable properties. In particular, we show the decidability of the emptiness problem under the restriction that a path of the TC-MSG does not force a basic scenario to take more than K units of time to complete (for a given K). Further, we prove that this condition can be effectively checked. Our approach consists in a symbolic encoding of timed constraints seen along a path into a bounded system of inequalities. Now, instead of constructing an interleaved model and using zones of timed automata as in existing approaches, we symbolically manipulate this system of inequalities. This allows for decision procedures which are both efficient and handle non regular specifications. We also show that with an additional structural restriction, we can obtain a regular set of timed representatives for a TCMSG, even if the set of all timed executions is not regular.

Janvier 2012

Thomas Place : Decidable Characterizations for Classes of Tree Languages : Infinite trees that are boolean combinations of open sets.

 Date : Jeudi 26 janvier à 13h15, salle de séminaire (R163), CMI.
 Orateur : Thomas Place (University of Warsaw)

This talk will be about the quest for decidable charcterizations for tree languages. Fix some class C of tree languages, a decidable characterization for C is an algorithm which given as input a regular tree language, answers whether this language is in C or not. Obtaining such a result is often very rewarding because it yields a deep insight on the class under investigation. The main open problem in this domain is to obtain a decidable characterization for first order logic on trees.

In the talk I will first present this main problem and the difficulties associated with it. Then I will present recent work for a particular class C : regular languages of infinite trees that are boolean (not necessarily positive) combinations of open sets. The decidable characterization will be presented with techniques using both algebra (myhill-nerode equivalence) and games.

This is joint work with Mikolaj Bojanczyk

Jurek Czyzowicz : Problème de patrouille

 Date : Jeudi 19 janvier à 11h00, salle de réunion du LIF (6ième étage de TPR1), Luminy.
 Orateur : Jurek Czyzowicz (Université du Québec en Outaouais)

Sur une courbe de longueur 1 se trouvent k agents mobiles. Les agents doivent patrouiller la courbe en se déplaçant perpétuellement, sans dépasser leurs vitesses maximales. L’efficacité d’une patrouille est exprimée par le temps maximal durant lequel un point de la courbe n’est pas visitée par un agent. L’algorithme de patrouille optimal est donc celui qui minimise la valeur I, telle que dans chaque intervalle de temps [t, t+I] chaque point p de l’environnement est visité au moins une fois par un agent. Nous considérons d’abord le cas où les agents possèdent des vitesses maximales distinctes. Ensuite, nous envisageons le cas des agents ayant la même vitesse maximale, qui doivent patrouiller un sous-ensemble de la courbe sur laquelle ils se déplacent.

Décembre 2011

Etienne Coulouma : Évaluation d’outils de vérification à partir d’algorithmes distribués

 Date : Jeudi 8 décembre à 13h30, salle de séminaire (R163), CMI.
 Orateur : Etienne Coulouma (LIF)

Dans cet exposé, on présentera en détail l’algorithme de consensus LastVoting (une version synchrone de Paxos), puis on proposera une grille d’évaluation de cet algorithme pour deux outils de vérification, POEM et ALCOOL.

Alexandre Donzé : Robust Satisfaction of Signal Temporal Logics and Applications

 Date : Jeudi 1er décembre à 13h30, salle de séminaire (R163), CMI.
 Orateur : Alexandre Donzé (Vérimag)

The Signal Temporal Logic (STL) is adapted to specify rigorously properties constraining real-valued, dense-time signals such as traces resulting from the simulation of continuous and hybrid systems. Recently, we extended STL with a quantitative (robust) interpretation which provides a numerical margin by which a simulation trace satisfies or violate a property. Moreover, we can estimate in some cases the sensitivity of this margin to a parameter change. By combining this information with different parameters exploration strategies, we get an efficient methodology to investigate which properties are satisfied by a model, how robustly these properties are satisfied and how to find parameters values which guarantees a robust satisfaction. I will describe this methodology and the toolbox which implements it, Breach, along with different application examples.

Novembre 2011

Alexander Heussner : Towards Model Checking Communicating Processes : From Reachability to Run Graphs, Graph Grammars, and MSO

 Date : Jeudi 24 novembre à 13h30, salle de séminaire (R163), CMI.
 Orateur : Alexander Heussner (ULB)

Extending previous results on control-state reachability for recursive communicating processes (RCPS) to model checking LTL on runs of RCPS demands to either restrict LTL or to limit RCPS profoundly. We propose to leave behind the interleaving semantics underlying LTL and focus a partial order representation of RCPS’s execution by run graphs. As the latter are shown to be context-free, we easily derive positive decidability results for MSO (seen as partial order logic). Further, width-bounded graph grammars generalize known semantic boundedness restrictions on RCPS, and proof to be a useful framework to derive new semantic boundedness conditions.

Euripides Markou : Gathering Asynchronous Oblivious Mobile Robots in a Ring

 Date : Jeudi 17 novembre à 13h30, salle de séminaire (R163), CMI.
 Orateur : Euripides Markou (University of Central Greece)

We consider the problem of gathering identical, memoryless, mobile robots in one node of an anonymous unoriented ring. Robots start from different nodes of the ring. They operate in Look-Compute-Move cycles and have to end up in the same node. In one cycle, a robot takes a snapshot of the current configuration (Look), makes a decision to stay idle or to move to one of its adjacent nodes (Compute), and in the latter case makes an instantaneous move to this neighbor (Move). Cycles are performed asynchronously for each robot. For an odd number of robots we prove that gathering is feasible if and only if the initial configuration is not periodic, and we provide a gathering algorithm for any such configuration. For an even number of robots we decide feasibility of gathering except for one type of symmetric initial configurations, and provide gathering algorithms for initial configurations proved to be gatherable.

B Srivathsan : Zone based verification of timed automata revisited

 Date : Jeudi 10 novembre à 13h30, salle de séminaire (R163), CMI.
 Orateur : B Srivathsan (LaBRI)

In this talk, we first consider the reachability problem for the classic model of timed automata defined by Alur and Dill. The reachability problem asks if there exists a path from the initial state to a final state of the automaton. A standard solution to this problem involves computing a search tree whose nodes are approximations of the so-called zones. For reasons of efficiency, only convex approximations have been implemented in tools. We provide efficient techniques to incorporate some non-convex approximations that subsume existing convex ones. The structure of our new algorithm also permits to calculate approximating parameters on-the-fly during exploration of the zone graph, yielding further improvement.

We would conclude the talk with a list of some other recent results on the Buchi emptiness problem : does a timed automaton have a non-Zeno run passing through a final state infinitely often ?

Octobre 2011

Pierre-Alain Reynier : Visibly Pushdown Transducers : Functionality, k-Valuedness, and Streamability

 Date : Jeudi 20 octobre à 13h30, salle de séminaire (R163), CMI.
 Orateur : Pierre-Alain Reynier (LIF)

Visibly pushdown transducers (VPTs) form a strict subclass of pushdown transducers (PTs) that extends finite state transducers with a stack. Like visibly pushdown automata, the input symbols determine the stack operations. It has been shown that visibly pushdown languages form a robust subclass of context-free languages. Along the same line, we show that word transductions defined by VPTs enjoy strong properties, in contrast to PTs. In particular, functionality is decidable in PTIME, k-valuedness is in NPTIME and equivalence of (non-deterministic) functional VPTs is EXPTIME-C.

In a second part, we study the problem of evaluating in streaming (i.e. in a single left-to-right pass) the transduction realized by a functional VPT. A transduction is said to be height bounded memory (HBM) if it can be evaluated with a memory that depends only on the height of the input word (and not on its length). We show that it is decidable in coNTPTime whether such a transduction is HBM. In this case, the required amount of memory may depend exponentially on the height of the input word. We exhibit a sufficient, decidable condition for a VPT to be evaluated with a memory that depends quadratically on the height of the input word. This condition defines a class of transductions that strictly contains all determinizable VPTs.

This talk is based on the two following papers :

• Properties of Visibly Pushdown Transducers. Emmanuel Filiot, Jean-François Raskin, Pierre-Alain Reynier Reynier, Frédéric Servais and Jean-Marc Talbot. In Proc. MFCS’10.
• Streamability of Nested Word Transductions. Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier and Frédéric Servais. In Proc. FSTTCS’11.

Emmanuel Godard : Consensus en présence d’omissions

 Date : Jeudi 13 octobre à 13h30, salle de séminaire (R163), CMI.
 Orateur : Emmanuel Godard (LIF)

Dans un environnement sujet à pertes de messages, à quelles conditions résoudre le problème classique du Consensus. Nous présenterons deux caractérisations des environnement pour lesquels il existe une solution à ce problème. Dans un premier temps, pour des motifs de pertes de messages très généraux, mais pour deux processus uniquement. Dans un deuxième temps, pour des motifs indépendants du temps mais pour des réseaux arbitraires. Cette seconde caractérisation a pour conséquence assez surprenante que le problème du Consensus est dans ce cas complètement équivalent au problème de la Diffusion, a priori plus simple. Nous utiliserons également ces caractérisations pour répondre de deux manières différentes à une question ouverte de Santoro et Wiedmayer.

Un travail effectué en collaboration avec Joseph Peters, SFU.

Janusz Malinowski : Hybrid algorithms for controller synthesis

 Date : Jeudi 6 octobre à 13h30, salle C105, CMI.
 Orateur : Janusz Malinowski (LIF)

Dans cette présentation, nous montrerons des résultats obtenus avec Peter Niebert et Pierre-Alain Reynier concernant la synthèse de contrôleur. Un des premiers résultats est une utilisation de la structure des systèmes d’équations différentielles afin de dégager une dépendance entre les variables et ainsi permettre une résolution hiérarchique de la synthèse. Un second résultat combine cette approche hiérarchique avec une stratégie Reachability and Safety. Enfin nous présenterons nos dernières avancées permettant la synthèse de contrôleurs dont l’objectif évolue au cours du temps.

Septembre 2011

Victor Chepoi : Nice labeling of event structures and embedding into products of trees of CAT(0) cube complexes

 Date : Jeudi 29 septembre de 13h à 14h, salle de séminaire (R163), CMI.
 Orateur : Victor Chepoi (LIF)

In this talk, we present a counterexample to a conjecture of Rozoy and Thiagarajan from 1991 (called also the nice labeling problem) asserting that any (coherent) event structure with finite degree admits a labeling with a finite number of labels, or equivalently, that there exists a function f : N → N such that an event structure with degree ≤ n admits a labeling with at most f(n) labels. Our counterexample is based on the Burling’s construction from 1965 of 3-dimensional box hypergraphs with clique number 2 and arbitrarily large chromatic numbers and the bijection between domains of event structures and median graphs (alias 1-skeletons of CAT(0) cube complexes) established by Barthélemy and Constantin in 1993.

In the second part of the talk, we will outline the proof that the contact graph of a 2-dimensional CAT(0) cube complex X of maximum degree d can be coloured with at most q(d)= Md^15 colours, for a fixed constant M. This implies that X (and the associated median graph) isometrically embeds in the Cartesian product of at most q(d) trees, and that theevent structure whose domain is X admits a nice labeling with q(d) labels. This second result is based on a join paper with Mark Hagen.

Sabine Frittella : Variétés de treillis avec une hiérarchie d’alternation des points fixes triviale

 Date : Jeudi 22 septembre à 13h30, salle de séminaire (R163), CMI.
 Orateur : Sabine Frittella (LIF)

Nous étudions ici les opérateurs de plus petit et de plus grand points fixes des fonctions croissantes et la façon de les évaluer par approximations successives à partir du plus petit élément d’un ensemble ordonné et, respectivement, à partir du plus grand élément. Il existe un algorithme standard qui calcule le plus petit et le plus grand point fixe en temps linéaire par rapport au nombre d’approximations. Ce nombre est en fait égal au nombre d’itérations (étapes) de la boucle principale de cet algorithme. Nous nous concentrons ici sur des variétés de treillis L(n), pour n <= 0, qui généralisent les treillis distributifs (L(0) est la variété des treillis distributifs). Nous prouvons que sur chaque variété L(n) le calcul du plus petit point fixe et du plus grand point fixe d’une formule de la théorie des treillis se fait sûrement et nécessairement en n+1 étapes avec l’algorithme standard. Cela nous permet d’affirmer que l’ajout des opérateurs de plus petit et de plus grand points fixes à la logique des treillis n’augmente pas l’expressivité de cette dernière lorsqu’on l’utilise sur des treillis appartenant à l’une des variétés L(n).

Arnaud Labourel : Tight Bounds for Scattered Black Hole Search in a Ring or a Torus

 Date : Jeudi 15 septembre à 13h30, salle de séminaire (R163), CMI.
 Orateur : Arnaud Labourel (LIF)

We study the problem of locating a dangerous node called black-hole in a synchronous anonymous network (a ring or a toroidal grid) with mobile agents. A black-hole is a harmful stationary process residing in a node of the network and destroying all mobile agents visiting that node. We consider the scenario when the agents are initially scattered within the network . Moreover, the agents have only constant memory and can only place a constant number of tokens to leave some information to the other agents. We give lower and upper bounds resources (number of agents and tokens) necessary for locating all links incident to the black hole.

Voir les exposés de 2010/2011, les exposés de 2009/2010, de 2008/2009, de 2007/2008 et de 2006/2007