• Responsable : Benjamin Monmege
• Lieu : LIS, salle de réunion du bâtiment modulaire BP5 (en bas de la BU), campus de Luminy
• Horaire : jeudi de 10h30 à 12h
• Abonnement à la liste de diffusion
• Calendrier des évènements du laboratoire contenant le calendrier du séminaire MOVE (adresse du calendrier iCal sur la page)

## Exposés à venir

• Séminaire CANA
• Francesco Dolce (Université du Québec à Montréal)
• Jeudi 15 mars, 11h
• Salle des commissions, Bât TPR2, 1er étage, Luminy
• Tree sets: from combinatorics on words to symbolic dynamics
• A tree set is a language of finite words such that the extension graph of each of its elements, the graph describing left and right extensions of the word in the language, is a tree. This class of sets includes classical families such as Sturmian and episturmian sets, as well as the coding of interval exchange transformations. Despite the very simple combinatorial definition, this family of languages satisfies several non trivial properties. It also provides an interesting connection between combinatorics on words, symbolic dynamical systems, bifix codes and free groups. In this talk, we investigate these sets, focusing on some geometrical examples (interval exchanges and linear involutions) and on some closure properties.

• Séminaire CANA
• Thibault Godin (University of Turku)
• Jeudi 22 mars, 14h
• Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
• Automaton groups, structure and properties
• In this talk, I will give a brief overview of the interplay between the structure of a Mealy automaton and the properties of the (semi)group it generates. Mealy automata are special kind of transducers that can be used to generate (semi)groups. These (semi)groups have been widely used in mathematics since the 80's as they can have some very interesting properties. For instance for first example of a group of intermediate growth has been discovered using a Mealy automaton. Furthermore, the underlying automata make these (semi-)groups amenable to computer science techniques, and I explain how automaton theoretic tools be used to predict characteristics of the group generated by a Mealy automaton.

• Nicolas Baudru (LIS)
• Jeudi 19 avril, 10h30
• Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
• From Two-Way Transducers to Regular Functions Expressions
• Transducers constitute a fundamental extension of automata. The class of regular word functions has recently emerged as an important class of word-to-word functions, characterized by means of (functional, or unambiguous, or deterministic) two-way transducers, copyless streaming string transducers, and MSO-definable graph transformations. One of the most important result in language theory is Kleene theorem, relating finite state automata and regular expressions. R. Alur, A. Freilich and M. Raghothaman have introduced (CSL-LICS '14) a set of regular function expressions and proved a similar result for regular word functions, by showing the equivalence with copyless streaming string transducers. In this paper, we propose a direct, simplified and effective translation from unambiguous two-way transducers to regular function expressions. In addition, our approach allows us to derive a subset of regular function expressions characterizing the (strict) subclass of functional sweeping transducers.

• Jeudi 3 mai, 10h30
• Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
• Costs and Rewards in Priced Timed Automata
• We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an ε-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert’s 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.

• Damien Busatto-Gaston (LIS)
• Jeudi 17 mai, 10h30
• Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
• TBA
• TBA

## Exposés 2017-2018

• Léo Exibard (LIS & ULB)
• Jeudi 8 février, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU), Luminy
• Two-Way Two-Tape Automata
• In this article we consider two-way two-tape (alternating) automata accepting pairs of words and we study some closure properties of this model. Our main result is that such alternating automata are not closed under complementation for non-unary alphabets. This improves a similar result of Kari and Moore for picture languages. We also show that these deterministic, non-deterministic and alternating automata are not closed under composition.

• Séminaire CANA
• Amaury Pouly (Max Planck Institute)
• Mardi 30 janvier, 9h30
• Salle du conseil, Bât TPR2, 1er étage, Luminy
• Continuous models of computation: computability, complexity, universality
• In 1941, Claude Shannon introduced a continuous-time analog model of computation, namely the General Purpose Analog Computer (GPAC). The GPAC is a physically feasible model in the sense that it can be implemented in practice through the use of analog electronics or mechanical devices. It can be proved that the functions computed by a GPAC are precisely the solutions of a special class of differential equations where the right-hand side is a polynomial. Analog computers have since been replaced by digital counterpart. Nevertheless, one can wonder how the GPAC could be compared to Turing machines. A few years ago, it was shown that Turing-based paradigms and the GPAC have the same computational power. However, this result did not shed any light on what happens at a computational complexity level. In other words, analog computers do not make a difference about what can be computed; but maybe they could compute faster than a digital computer. A fundamental difficulty of continuous-time model is to define a proper notion of complexity. Indeed, a troubling problem is that many models exhibit the so-called Zeno's phenomenon, also known as space-time contraction. In this talk, I will present results from my thesis that give several fundamental contributions to these questions. We show that the GPAC has the same computational power as the Turing machine, at the complexity level. We also provide as a side effect a purely analog, machine- independent characterization of P and Computable Analysis. I will present some recent work on the universality of polynomial differential equations. We show that when we impose no restrictions at all on the system, it is possible to build a fixed equation that is universal in the sense it can approximate arbitrarily well any continuous curve over R, simply by changing the initial condition of the system. If time allows, I will also mention some recent application of this work to show that chemical reaction networks are strongly Turing complete with the differential semantics.

• Marion Hallet (Université de Mons)
• Jeudi 25 janvier, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Dynamics and Coalitions in Sequential Games
• We consider n-player non-zero sum games played on finite trees (i.e., sequential games), in which the players have the right to repeatedly update their respective strategies, for instance, to improve the outcome wrt to the current strategy profile. This generates different type of dynamics in the game which may eventually stabilise, for example to Nash Equilibrium.

• El Makki Voundy (LIF)
• Mercredi 8 novembre, 14h00
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Langages $$\epsilon$$-sûrs et caractérisations des langages d’ordres supérieurs
• Une ligne de recherche présente dans la littérature depuis les années soixante est celle des "théorèmes de représentation". Son résultat fondateur est le théorème de Chomsky-Schützenberger qui stipule qu'un langage est algébrique si et seulement si il est l'image par homomorphisme de l'intersection entre un langage régulier et le langage de Dyck. Ce résultat a connu depuis diverses généralisations à différentes familles de langages. Dans cette thèse, nous proposons plusieurs généralisations de ce résultat aux langages d'ordres supérieurs. Ceux-ci sont des langages reconnaissables par des automates à piles itérées. Nous définissons une notion de langages de Dyck d'ordres supérieurs, nous introduisons et étudions des classes de transductions que nous qualifions d'$$\epsilon$$-sûres et nous montrons qu'un langage appartient à un niveau k+l de la hiérarchie des langages d'ordres supérieurs si et seulement si il est l'image d'un langage de Dyck de niveau k par une transduction $$\epsilon$$-sûre de niveau l. Ce résultat contribue à la description des traces d'exécutions des calculs des machines capables de reconnaître les langages d'ordres supérieurs et apporte un outil théorique visant à permettre de généraliser des résultats valant pour un niveau quelconque de la hiérarchie vers un autre. Nous illustrons ce dernier point en généralisant une caractérisation logique des langages algébriques aux langages indexés.

• Didier Villevalois (LIF)
• Jeudi 7 décembre, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• On string-to-outer-context transducers and their sequentialization
• Model synthesis from specifications often produce large and impractical models. A natural problem is then to simplify those models, and especially make them deterministic. In the context of transducers, i.e., automata with output, a machine that is deterministic in the way it reads its input is said to be sequential. In this work, we are interested in non-deterministic streaming string transducers, a model of transducers with write-only registers introduced by Alur. We investigate a particular subclass of this model that uses only 1 *concatenation-free* register, i.e., whose updates are of the form X=uXv, for some words u,v. We present how this can be viewed as a string-to-string finite state transducer whose transitions have output labels that are contexts. At each move, the output context of the chosen transition is put around the already produced output word. We call those machines string-to-outer-context transducers. This context-based presentation enables us to exhibit an elegant contextual twinning property, in the line of Choffrut's twinning property to decide sequentializability of string-to-string finite state transducers. We show that, given a string-to-outer-context transducer, it is equivalent i) whether it satisfies the contextual twinning property, ii) whether there exists an equivalent sequential string-to-outer-context transducer, and iii) whether the induced string-to-string function satisfies a Lipschitz property (for an appropriate notion of distance). This is a work in progress and not all the details are set in stone yet. We will thus discuss what is done and what remains to be done.

• Denis Lugiez (LIF)
• Jeudi 14 septembre, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Est-ce que je peux écrire dans votre liste ?
• La logique de séparation est utilisée dans la preuve de programme pour exprimer des propriétés de la mémoire (le tas) et plusieurs outils ont été réalisés pour cette logique. La logique de base a été enrichie pour pouvoir prendre en compte des structures comme les listes ou les droits de lecture/écriture donnés à un thread. Plusieurs modèles ont été utilisés pour décrire ces droits (modèles de fraction, modèle de token, modèles des arbres de partage binaires...). Dans ce travail nous donnons une procédure permettant de tester la satisfaisabilité et l'implication de formules d'une logique de séparation avec listes paramétrée par le modèle de permission. Contrairement à ce qui se passe dans le cas des listes sans permissions, le problème de satisfaisabilité est NP-dur et l'implication est co-NP-dur. Nous donnons une procédure non-déterministe pour l'implication paramétrée par le modèle de permission permettant de prouver que le problème de l'implication est co-NP complet (modulo un oracle sur le modèle de permission). Cette procédure utilise une procédure qui résoud le problème sans liste mais avec permission qui est optimale dans un certain type de modèles de permissions. L'outil sur lequel repose la procédure est le SL-graphe qui est une représentation symbolique d'une formule permettant de ramener le problème à une question d'isomorphisme entre graphes. Pour finir, nous donnons des résultats de complexité optimaux dans les modèles de permissions pour les problèmes de satisfaisabilité et d'implication dans le modèle fractionnaire et une classe de modèles générique (modèles booléens).
Travail réalisé avec Stéphane Demri et Etienne Lozes (LSV, ENS Paris-Saclay).
PS: pour ceux qui doutent de l’intérêt pratique de cette logique, le bug "dirty cow" du noyau linux -qui a notamment servi à escroquer un hébergeur coréenne via un rançongiciel au mois de juin- repose sur le fait qu'un thread qui ne devrait avoir qu'un droit de lecture gagne un droit d'écriture suite à une race condition...

• Séminaire LDP
• Charles Grellois (LSIS)
• Jeudi 21 septembre, 11h00
• Salle de séminaire de l'I2M à Luminy, bâtiment TPR2, 3ème étage, 304-306
• Two Type-Theoretic Approaches to Probabilistic Termination
• A fundamental result in lambda-calculus states that terms that admit a simple type are strongly normalizing: in other words, they always terminate. The simply-typed lambda-calculus can be enriched with a recursion operator and, in this case, terms admitting a sized type always terminate. In this talk, we study a simply-typed lambda-calculus enhanced with a recursion operator and a probabilistic choice operator, and we focus on the probabilistic counterpart of termination: almost-sure termination (AST), that is, termination with probability 1. I will explain how the sized types approach can be extended to the probabilistic setting, so that we obtain a type system in which typability guarantees AST. I will then sketch ongoing work on a more powerful approach using dependent types, in order to capture AST for a wider class of programs. This is joint work with Dal Lago.

## Exposés 2016-2017

• Emmanuel Filiot (Université libre de Bruxelles)
• Jeudi 6 juillet, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• A decidable logic for finite word transductions
• A finite word transduction is a binary relation of finite words. After a brief introduction on recent results about word transductions, in particular about logics, algebra and automata for word transductions, the talk introduces a new logic to specify properties of word transductions, and presents some of its expressiveness and algorithmic properties. In particular, the model-checking and synthesis problems for the expressive class of MSO-definable (functional) transductions, against/from properties specified in this logic, are considered. A connection with a logic for finite words over infinite alphabets (data words) will be shown as well.
This work is joint with Luc Dartois (ULB) and Nathan Lhote (ULB / UBordeaux).

• Pierre-Alain Reynier (LIF)
• Jeudi 29 juin, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Copyfull Streaming String Transducers
• Copyless streaming string transducers (copyless SST) have been introduced by R. Alur and P. Cerny in 2010 as a one-way deterministic automata model to define transductions of finite strings. Copyless SST extend deterministic finite state automata with a set of variables in which to store intermediate output strings, and those variables can be combined and updated all along the run, in a linear manner, i.e., no variable content can be copied on transitions. It is known that copyless SST capture exactly the class of MSO-definable string-to-string transductions, and are as expressive as deterministic two-way transducers. They enjoy good algorithmic properties. Most notably, they have decidable equivalence problem (in PSpace).
On the other hand, HDT0L systems have been introduced for a while, the most prominent result being the decidability of the equivalence problem. In this paper, we propose a semantics of HDT0L systems in terms of transductions, and use it to study the class of copyfull SST. Our contributions are as follows: (i) HDT0L systems and total copyfull SST are equi-expressive, (ii) the equivalence problem for copyfull SST and the equivalence problem for HDT0L systems are inter-reducible, in linear time. As a consequence, SST equivalence is decidable, (iii) the functionality of non-deterministic copyfull SST is decidable, (iv) determining whether a copyfull SST can be transformed into an equivalent copyless SST is decidable in polynomial time.
Joint work with Emmanuel Filiot.

• Ralf Treinen (IRIF, Université Paris Diderot)
• Jeudi 22 juin, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Towards the verification of file tree transformations - the Colis project
• This talk describes the ongoing ANR project Colis, which has the goal of developing techniques and tools for the formal verification of shell scripts. More specifically, our goal is to verify the transformation of a file system tree described by so-called Debian maintainer scripts. These scripts, often written in the Posix shell language, are part of the software packages in the Debian GNU/Linux distribution.
A possible example of a program specification is absence of execution error under certain initial conditions. Automatic program verification even for this kind of specification is a challenging task. In case of Debian maintainer scripts we are faced with even more challenging properties like idempotency of scripts (required by policy), or commutation of scripts.
The project is still in its early stage, so there are only some preliminary results at the moment. However, I will explain why I think that the case of Debian maintainer scripts is very interesting for program verification : some aspects of scripts (POSIX shell, manipulation of a complex data structure) make the problem very difficult, while other aspects of the Debian case are likely to make the problem easier than the task of verifying any arbitrary shell script.

• Frédéric Olive (LIF)
• Jeudi 15 juin, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• A logical approach to locality in pictures languages
• This paper deals with descriptive complexity of picture languages of any dimension by fragments of existential second-order logic: 1) We generalize to any dimension the characterization by Giammarresi et al. (1996) of the class of recognizable picture languages in existential monadic second-order logic. 2) We state natural logical characterizations of the class of picture languages of any dimension d≥1 recognized in linear time on nondeterministic cellular automata, a robust complexity class that contains, for d=1, all the natural NP-complete problems. Our characterizations are essentially deduced from normalization results for first-order and existential second-order logics over pictures.
Joint work with Etienne Grandjean

• Théodore Lopez (ENS Paris-Saclay & LIF)
• Jeudi 18 mai, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Positivité d'automates de Büchi non-ambigus
• Dans le cadre du model-checking, on s'intéresse au calcul de la probabilité que, pour une entrée infinie fournie par une chaîne de Markov, un automate de Büchi accepte sur celle-ci. Dans ce calcul, il est d'abord nécessaire de décider si l'automate a une probabilité non nulle d'accepter. Cette propriété est indépendante de la chaîne de Markov, on parle de positivité de l'automate. On fournira deux méthodes, une calculatoire et une constructive, décidant de la positivité.

• Tayssir Touili (LIPN, Université Paris 13)
• Jeudi 4 mai, 14h
• Salle CH301 du Département Informatique et Interactions, Campus St Charles
• On static malware detection
• The number of malware is growing extraordinarily fast. A malware may bring serious damage, e.g., the worm MyDoom slowed down global internet access by ten percent in 2004. Thus, it is crucial to have efficient up-to-date virus detectors. Existing antivirus systems use various detection techniques to identify viruses such as (1) code emulation where the virus is executed in a virtual environment to get detected; or (2) signature detection, where a signature is a pattern of program code that characterizes the virus. A file is declared as a virus if it contains a sequence of binary code instructions that matches one of the known signatures. These techniques are becoming insufficient. Indeed, emulation based techniques can only check the program's behavior in a limited time interval. As for signature based systems, it is very easy to virus developers to get around them. Thus, a robust malware detection technique needs to check the behavior (not the syntax) of the program without executing it. We show in this talk how using behavior signatures allow to efficiently detect malwares in a completely static way. We implemented our techniques in a tool, and we applied it to detect several viruses. Our results are encouraging. In particular, our tool was able to detect more than 800 viruses. Several of these viruses could not be detected by well-known anti-viruses such as Avira, Avast, Norton, Kaspersky and McAfee.

• Benjamin Monmege (LIF)
• Jeudi 30 mars, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Metric Interval Temporal Logic Revisited
• This talk will present two recent works on MITL logic.
The first, published at FORMATS'16, studies the reactive synthesis problem (RS) for specifications given in MITL. RS is known to be undecidable in a very general setting, but on infinite words only; and only the very restrictive BResRS subcase is known to be decidable (see D'Souza et al. and Bouyer et al.). We precise the decidability border of MITL synthesis. We show RS is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit BResRS and introduce an efficient on-the-fly algorithm to solve it. Based on a joint work with Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts, Hsi-Ming Ho and Nathalie Sznajder.
The second one deals with the tool support for MITL verification that is still lacking to this day. Therefore, we propose a new construction from MITL to timed automata via very-weak one-clock alternating timed automata. Our construction subsumes the well-known construction from LTL to Büchi automata by Gastin and Oddoux and yet has the additional benefits of being compositional and integrating easily with existing tools. We implement the construction in our new tool MightyL and report on experiments using Uppaal and LTSmin as back-ends. Based on a joint work with Thomas Brihaye, Gilles Geeraerts and Hsi-Ming Ho.

• Aznam Yacoub (LSIS)
• Jeudi 23 mars, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Une approche de vérification formelle et de simulation pour les systèmes à événements discrets : Application à PROMELA
• Depuis quelques années, les nouvelles avancées technologiques ont permis la mise au point de systèmes physiques et logiciels qui aident considérablement l'Homme dans ses tâches, que ce soit dans la vie quotidienne ou dans des processus industriels. Aux allures simples, ces panneaux publicitaires, ces chaînes de fabrication automatisées ou même ces pilotes automatiques sont devenus, au fil du temps, de plus en plus complexes à comprendre et à maîtriser, entraînant en permanence de nouveaux lots de problématiques et de questions. Du fait qu'ils impliquent davantage d'interactions qu'auparavant, avec de plus en plus de composants qui communiquent entre eux, ces systèmes demandent encore plus de vigilances à leurs concepteurs qui doivent s'assurer que ces systèmes ne génèrent pas de comportements inadaptés ou imprévus. Ce constat, que nous faisons pour les systèmes et les processus que nous développons, est identique au constat réalisé dès lors que nous souhaitons modéliser et simuler un phénomène physique complexe, tel qu'un évènement météorologique ou le fonctionnement du cerveau humain, qui impliquent aussi des interactions compliquées entre des dizaines, des centaines voire des milliers d'entités différentes. Mais si les avancées ont été énormes dans les champs technologiques et scientifiques en général, les domaines de la Vérification et de la Validation ont également connu un bond significatif avec la mise au point de nouveaux concepts et de nouvelles méthodes, automatiques ou non, pour répondre à ce besoin de fiabilité. Parmi elles, se dégagent notamment deux grandes familles : celle de la Vérification Formelle et celle de la Simulation. Longtemps considérées comme à l'opposée l'une de l'autre, les recherches récentes essaient de rapprocher ces deux grandes familles de méthodologies. C'est dans ce cadre que les travaux de cette thèse proposent une nouvelle approche pour intégrer la Simulation dites à Evènements Discrets aux Méthodes Formelles. L'objectif d'une telle approche est alors d'améliorer les méthodes formelles existantes, en les combinant à la simulation, afin de leur permettre de détecter de potentielles erreurs qu'elles ne pouvaient déceler avant, notamment sur des systèmes temporisés. Cette approche nous a conduit à la mise au point d'un nouveau langage formel, le DEv-PROMELA. Ce nouveau langage, créé à partir du PROMELA et du formalisme DEVS, est à mi-chemin entre un langage de spécifications formelles vérifiables et un formalisme de simulation. En combinant alors un model-checking traditionnel et une simulation à évènements discrets sur le modèle exprimé dans ce nouveau langage, il est alors possible de détecter et de comprendre des dysfonctionnements qu'un model-checking seul ou qu'une simulation seule n'auraient pas permis de trouver. Ce résultat est notamment illustré à travers les différents exemples étudiés dans ces travaux.

• Didier Villevalois (LIF)
• Jeudi 16 mars, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Présentation d'article : Monadic Second-Order Logic on Finite Sequences (by Loris D'Antoni and Margus Veanes)
• We extend the weak monadic second-order logic of one successor for finite strings (M2L-STR) to symbolic alphabets by allowing character predicates to range over decidable quantifier free theories instead of finite alphabets. We call this logic, which is able to describe sequences over complex and potentially infinite domains, symbolic M2L-STR (S-M2L-STR). We present a decision procedure for S-M2L-STR based on a reduction to symbolic finite automata, a decidable extension of finite automata that allows transitions to carry predicates and can therefore model complex alphabets. The reduction constructs a symbolic automaton over an alphabet consisting of pairs of symbols where the first element of each pair is a symbol in the original formula’s alphabet, while the second element is a bit-vector. To handle this modified alphabet we show that the Cartesian product of two decidable Boolean algebras, e.g., the product of formula’s algebra and bit-vector’s algebra, also forms a decidable Boolean algebra. To make the decision procedure practical, we propose two efficient representations of the Cartesian product of two Boolean algebras, one based on algebraic decision diagrams and one on a variant of Shannon expansions. Finally, we implement our decision procedure and evaluate it on more than 10,000 formulas. Despite the generality, our implementation has comparable performance with the state-of-the-art M2L-STR solvers.

• Paul Brunet (University College London)
• Jeudi 2 mars, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Algebras of relations: from algorithms to formal proofs
• Algebras of relations appear naturally in many contexts, in computer science as well as in mathematics. They constitute a framework well suited to the semantics of imperative programs. Kleene algebras are a starting point: these algebras enjoy very strong decidability properties, and a complete axiomatisation. The goal of this thesis was to export known results from Kleene algebra to some of its extensions.
We first considered a known extension: Kleene algebras with converse. Decidability of these algebras was already known, but the algorithm witnessing this result was too complicated to be practical. We proposed a simpler algorithm, which is more efficient, and whose correctness is easier to establish. It allowed us to prove that this problem lies in the complexity class PSpace-complete.
Then we studied Kleene allegories. Few results were known about this extension. Following results about closely related algebras, we established the equivalence between equality in Kleene allegories and the equality of certain sets of graphs. We then developed a new automaton model (so-called Petri automata), based on Petri nets. We proved the equivalence between the original problem and comparing these automata. In the restricted setting of identity-free Kleene lattices, we also provided an algorithm performing this comparison. This algorithm uses exponential space. However, we proved that the problem of comparing Petri automata lies in the class ExpSpace- complete.
Finally, we studied Nominal Kleene algebras. We realised that existing descriptions of these algebra were not suited to relational semantics of programming languages. We thus modified them accordingly, and doing so uncovered several natural variations of this model. We then studied formally the bridges one could build between these variations, and between the existing model and our new version of it. This study was conducted using the proof assistant Coq.

• Bruno Guillon (Université de Varsovie)
• Jeudi 2 février, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Regular transductions with origin semantics
• This talk is about regular transductions, which are string-to-string functions realised by one of the following equivalent deterministic formalisms: MSO transduction, two-way transducer and streaming string transducer. We may observe that each of these formalisms provides more than just a function from words to words. Indeed, one can also reconstruct origin information, which says how positions of the output string originate from positions of the input string. It is also possible to provide any string-to-string function with an origin semantic, indicating an origin input position for each output position, in a similar way. This defines a general object, that extends functions and which we call origin graph. The main result of the talk is a characterisation of the families of origin graphs which correspond to a regular transduction with origin information.
This is joint work with Mikołaj Bojańczyk, Laure Daviaud and Vincent Penelle.

• Damien Busatto-Gaston (LIF)
• Jeudi 26 janvier, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• Optimal Reachability in Divergent Weighted Timed Games
• Weighted timed games are played by two players on a timed automaton equipped with weights: one player wants to minimise the accumulated weight while reaching a target, while the other has an opposite objective. Used in a reactive synthesis perspective, this quantitative extension of timed games allows one to measure the quality of controllers. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. Decidability results exist for subclasses of one-clock games, and for a subclass with non-negative weights defined by a semantical restriction on the weights of cycles. In this work, we introduce the class of divergent weighted timed games as a generalisation of this semantical restriction to arbitrary weights. We show how to compute their optimal value, yielding the first decidable class of weighted timed games with negative weights and an arbitrary number of clocks. In addition, we prove that divergence can be decided in polynomial space. Last, we prove that for untimed games, this restriction yields a class of games decidable in non-deterministic logarithmic space, and for which the value can be computed in polynomial time.
Joint work with Benjamin Monmege and Pierre-Alain Reynier

• Ocan Sankur (IRISA, CNRS)
• Jeudi 5 janvier, 10h30
• Salle de réunion du bâtiment modulaire (en bas de la BU)
• A Practical Abstraction Technique for Parameterized Model Checking of Leader Election Protocols
• 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, moreover, nodes have independently evolving clocks. We apply our technique for model checking the root election part of the flooding time synchronisation protocol (FTSP), and obtain improved results compared to previous work. We model check the protocol for all topologies in which the distance to the node to be elected leader is bounded by a given parameter. Our results prove the correctness of the protocol on networks including for 2D grids of hundreds of nodes, and 3D of thousands of nodes.

• Mahsa Shirmohammadi (University of Oxford)
• Jeudi 15 décembre, 10h30
• Salle BU3A
• 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.

Séminaire LIF de James Worrell (University of Oxford) : consultez toutes les informations
• Didier Villevalois (LIF)
• Jeudi 24 novembre, 10h30
• Salle de réunion du 6ème étage du LIF
• Degree of sequentiality of weighted automata
• Weighted automata (WA) are an important formalism to describe quantitative properties. Obtaining equivalent deterministic machines is a longstanding research problem. In this paper we consider WA with a set semantics, meaning that the semantics is given by the set of weights of accepting runs. We focus on multi-sequential WA that are defined as finite unions of sequential WA. The problem we address is to minimize the size of this union. We call this minimum the degree of sequentiality of (the relation realized by) the WA. For a given positive integer k, we provide multiple characterizations of relations realized by a union of k sequential WA over an infinitary finitely generated group: a Lipschitz-like machine independent property, a pattern on the automaton (a new twinning property), and a subclass of cost register automata. When possible, we effectively translate a WA into an equivalent union of k sequential WA. We also provide a decision procedure for our twinning property for commutative computable groups thus allowing to compute the degree of sequentiality. Last, we show that these results also hold for word transducers and that the associated decision problem is Pspace-complete.
Joint work with Laure Daviaud, Ismael Jecker, and Pierre-Alain Reynier

• El Makki Voundy (LIF)
• Jeudi 3 novembre, 10h30
• Salle de réunion du 6ème étage du LIF
• Théorie des AFL
• Un cône rationnel est une famille de langages close par intersection avec des langages réguliers, homomorphismes et homomorphismes inverses ; un full-AFL (Abstract Family of Languages) est un cône rationnel clos par union, concatenation et étoile de Kleene. Ces notions ont été introduites par Greibach et Ginsburg sous l'observation que les familles de la hiérarchie de Chomsky (du moins, telle qu’elle était dans les années 60) sont généralement closes par ces opérations et avec pour motivation d'apporter une approche générique à l'étude de ces familles. La "théorie des AFL" consiste à étudier l'incidence de ces propriétés de clôture sur les propriétés globales des familles qui en sont closes. Il est par exemple possible d'établir que tout cône rationnel généré à partir d'un langage est clos par union ; ou que le problème de la régularité d'un langage est indécidable pour tout cône rationnel clos par union et qui contient le langage $$\{a^nb^n, n \geq 0\}$$. Dans cet éxposé, je vous présenterai quelques résultats de cette dite théorie des AFL. Nous observerons la dépendance entre differentes opérations de clôture, de quelle façon la présence d'un langage dans une famille puisse lui garantir des propriétés de clôture et comment correler clôture et indécidabilité.

• Guillaume Rabusseau (LIF)
• Jeudi 6 octobre, 10h30
• Salle de réunion du 6ème étage du LIF
• Séries reconnaissables de graphes et minimisation approximée d'automates pondérés
• Pendant cet exposé, je présenterai deux travaux réalisés pendant ma thèse au sein de l'équipe Qarma. Ces deux travaux ont été initialement motivés par des problématiques d'apprentissage automatique et concernent les automates pondérés. Après avoir rappelé les méthodes d'apprentissage spectral pour les automates pondérés, je présenterai ces deux contributions :
- Séries reconnaissables de graphes. Nous proposons une extension des modèles de séries reconnaissables de chaînes et d'arbres aux graphes. Nous montrons tout d'abord que les modèles d'automates pondérés de chaînes et d'arbres peuvent être interprétés d'une manière simple et unifiée à l'aide de réseaux de tenseurs, et que cette interprétation s'étend naturellement aux graphes. Nous étudions ensuite certaines propriétés fondamentales de ce modèle (clôture par somme et produit, reconnaissabilité des séries à support fini) avant de présenter des résultats préliminaires sur leur apprentissage.
- Minimisation approximée d'automates pondérés. Nous considérons le problème suivant : étant donné un automate pondéré à n états, comment trouver un automate à m (inférieur à n) états calculant une fonction proche de l'originale. Cette problématique a été considérée dans des travaux récents (Balle et al., LICS 2015) pour le cas d'automates pondérés sur les mots. Dans ces travaux, les auteurs introduisent une forme canonique pour les automates pondérés pour laquelle les états d'un automate sont clairement ordonnés et découplés, ce qui leur permet de proposer une approche théoriquement fondée à cette problématique. Nous présenterons l'extension de ces travaux aux automates pondérés d'arbres.

• Paul Gastin (LSV, ENS Paris-Saclay)
• Jeudi 29 septembre, 10h30
• Salle de réunion du 6ème étage du LIF
• Analyzing Timed Systems Using Tree Automata
• Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. Such graphs can be interpreted in trees opening the way to tree automata based techniques which are more powerful than analysis based on word automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions). This is a joint work with S. Akshay and Shankara Narayanan Krishna.

• Silvio Ranise (Bruno Kessler Foundation, Trento)
• Mardi 27 septembre, 10h00
• Salle de réunion du 6ème étage du LIF
• SMT-based Enforcement and Analysis of NATO Content-based Protection and Release Policies
• NATO is developing a new IT infrastructure that will enable automated information sharing between different information security domains and provide strong separation between different communities of interest while supporting dynamic and flexible enforcement of the need-to-know principle. In this context, the Content-based Protection and Release (CPR) model has been introduced to support the specification and enforcement of access control policies used in NATO and, more generally, in complex organizations. While the ability to support fine-grained security policies for a large variety of users, resources and devices is desirable, the definition, maintenance, and enforcement of these policies can be difficult, time-consuming, and error-prone. Thus, automated support for policy analysis to help designers in these activities is needed. In this talk we show that several policy-related analysis problems of practical interest can be reduced to SMT problems, we propose an effective enforcement mechanism relying on attribute-based encryption (ABE), and assess the scalability of our approach on an extensive set of synthetic benchmarks.

• Maribel Fernandez (King's College London)
• Mardi 27 septembre, 11h00
• Salle de réunion du 6ème étage du LIF
• Access control and obligations in the category-based metamodel
• We define an extension of the category-based access control (CBAC) metamodel to accommodate a general notion of obligation. Since most of the well-known access control models are instances of the CBAC metamodel, we obtain a framework for the study of the interaction between authorisation and obligation, such that properties may be proven of the metamodel that apply to all instances of it. In particular, the extended CBAC metamodel allows security administrators to check whether a policy combining authorisations and obligations is consistent.

• Worachet Uttha (LIF)
• Jeudi 22 septembre, 10h30
• Salle de réunion du 6ème étage du LIF
• Étude des politiques de sécurité pour les applications distribuées : le problème des dépendances transitives
• Le contrôle d'accès est un ingrédient fondamental de la sécurité des systèmes d'information. Depuis les années 70, les travaux dans ce domaine ont apporté des solutions aux problèmes de confidentialités des données personnelles avec applications à différents environnements (systèmes d'exploitation, bases de données, etc.). Parmi les modèles de contrôle d'accès, nous intéressons au modèle basé sur les organisations (OrBAC) et nous en proposons une extension adapté aux contextes distribués tels que les services web. Ce modèle étendu est capable en particulier de gérer les demandes d'accès transitives. Ce cas peut se produire lorsqu'un service doit appeler un autre service qui peut avoir besoin d'invoquer à son tour un ou plusieurs services afin de satisfaire la demande initiale.
Nous appelons D-OrBAC (Distributed Organisation Based Access Control), l'extension du modèle OrBAC avec une notion de procuration représentée par un graphe de délégation. Ce graphe nous permet de représenter des accords entre les différentes organisations impliquées dans la chaîne d'invocations de services, et de garder la trace des autorisations transitives. Nous proposons également une technique d'analyse basée sur Datalog qui nous permet de simuler des scénarios d'exécution et de vérifier l'existence de situations non sécurisées.
Nous utilisons ensuite des techniques de réécriture afin d'assurer que la politique de sécurité spécifiée via notre modèle D-OrBAC respecte des propriétés importantes telles que la terminaison et la consistance. Finalement, nous implémentations pour un cas d'étude, le mécanisme d'évaluation des demandes d'accès selon la norme XACML sur la plateforme WSO2 Identity Server, afin de montrer que notre solution est capable de fournir à la fois la fonctionnalité désirée et la sécurité nécessaire pour le système.

## Exposés 2015-2016

• Aiswarya Cyriac (Chennai Mathematical Institue)
• Jeudi 7 juillet, 10h30
• Salle de réunion du 6ème étage du LIF
• Formal methods for the verification of distributed algorithms
• We propose automata-theoretic approach for the verification of distributed algorithms in which processes can store, send and compare process-identifiers (pids). Examples include leader election algorithms and distributed sorting algorithms. We introduce a logic to specify correctness of such distributed algorithms. This logic is inspired by data logics, and can reason about processes and pids. The model checking problem is undecidable in general; we will see some ideas to regain decidability for distributed algorithms over ring topologies. Based on joint work with Benedikt Bollig and Paul Gastin.

• Madhur Gupta (stagiaire LIF, Thapar University)
• Jeudi 9 juin, 10h30
• Salle de réunion du 6ème étage du LIF
• Inference of (min,+) Automata
• We develop a method to infer min-plus automata from sample behaviors. Min-plus automata recently attracted a lot of interest as a model of online algorithms. Unlike existing approaches to the inference of automata in a quantitative setting, our procedure works in an active fashion: an automaton is gradually refined on the basis of multiplicity and equivalence queries. Moreover, it is not restricted to deterministic devices but applies to residual automata: a large class of non-deterministic automata that is strictly more expressive and exponentially more succinct. I will show the method, after recalling the standard L* Angluin’s algorithm, to infer deterministic finite-state automata.
Joint work with Benedikt Bollig (LSV, ENS Cachan, CNRS), Peter Habermehl (IRIF, Université Paris Diderot, CNRS), and Benjamin Monmege (LIF, AMU, CNRS)

• Jeudi 2 juin, 10h30
• Salle de réunion du 6ème étage du LIF
• Rational verification in Iterated Electric Boolean Games
• Electric boolean games are compact representations of games where the players have qualitative objectives described by LTL formulae and have limited resources. We study the complexity of several decision problems related to the analysis of rationality in electric boolean games with LTL objectives. In particular, we report that the problem of deciding whether a profile is a Nash equilibrium in an iterated electric boolean game is no harder than in iterated boolean games without resource bounds. We show that it is a PSPACE-complete problem. As a corollary, we obtain that both rational elimination and rational construction of Nash equilibria by a supervising authority are PSPACE-complete problems. Joint work with Nicolas Troquard

• Clara Bertolissi (LIF)
• Jeudi 26 mai, 10h30
• Salle de réunion du 6ème étage du LIF
• A Methodology to Build Run-Time Monitors for Enforcing Authorization Policies in Business Processes
• We are interested in security-aware workflow management systems, which are at the heart of modern e-services and need to mediate access to their resources by imposing authorisation constraints (e.g., separation of duty). We introduce a class of symbolic transition systems capable of representing collections of security-aware workflows and we study the verification of reachability properties of such systems. We use our technique to build efficient run-time monitors capable of ensuring the successful termination of workflows subject to authorisation constraints.

• Emmanuel Beffara (I2M)
• Jeudi 28 avril, 10h30
• Campus St Charles, salle CH 301 (près du département Informatique et Interactions, à droite de l'amphi de Chimie au 3ème étage)
• Approches logiques en sémantique des langages concurrents
• Dans la modélisation des systèmes concurrents, un problème central est celui de la compositionnalité, ou comment déduire des propriétés d'un système complet à partir de l'analyse de ses composants de façon indépendante: c'est ce qui permet de “passer à l'échelle” et de concevoir des systèmes sûrs de façon modulaire. Dans le monde des langages de programmation, c'est le typage qui sert à composer correctement les programmes. Dans cet exposé, je raconterai des idées récentes sur ce que la théorie de la démonstration peut apporter à la question de la modélisation et du typage des processus concurrents, notamment en présence de mobilité, c'est-à-dire quand la topologie des canaux de communication évolue avec l'exécution.

• Matteo Mio (LIP, ENS Lyon)
• Jeudi 21 avril, 10h30
• Campus St Jérôme, Salle Gérard Jaumes du rez de chaussée du Bâtiment Polytech, map
• Measure Quantifier in Monadic Second Order Logic
• In this talk I will present some recent work, with H. Michalewski, on the study of an extension of MSO on infinite trees with the so-called "measure quantifier". This kind of research is motivated, as I will discuss, by a long-standing open problem in the field of verification of probabilistic programs. I will state a negative (i.e., undecidability) result but also present some interesting (currently) open problems.

• Ocan Sankur (IRISA, CNRS)
• Jeudi 14 avril, 10h30
• Salle de réunion du 6ème étage du LIF
• Admissible Strategies in Quantitative Games
• The notion of admissible strategies has been proposed in game theory to formalize rationality of players. It has been studied recently for games of infinite duration with Boolean objectives. In this talk, we give explain this notion, and give motivations on its interest for controller synthesis. We extend admissible strategies to games of infinite duration with quantitative objectives. First, we show that, under the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the notion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide verification and synthesis problems related to the notion of admissible strategy. Joint with Romain Brenguier, Guillermo Perez, Jean-Francois Raskin.

• Nicolas Baudru (LIF)
• Jeudi 7 avril, 10h30
• Salle de réunion du 6ème étage du LIF
• Autour de l'algorithme de multiplication de D.V et G.V Chudnovsky
• Savoir multiplier deux éléments d'un corps fini est un problème important qui est au coeur des protocoles cryptographiques. En effet le chiffrement et le déchiffrement de ces protocoles reposent sur l'efficacité de la multiplication, qui a donc un impact direct sur la sécurité. Les algorithmes issus de l'approche de D.V. et G.V. Chudnovsky permettent de réaliser efficacement la multiplication de deux éléments de $GF_{q^n}$ avec $q$ une puissance d'un nombre premier. Efficace signifie ici avec une complexité bilinéaire linéaire en $n$. Ces algorithmes utilisent des espaces de Riemann-Roch construits à partir de corps de fonctions algébriques. J'introduirai ces notions et présenterai la méthode des frères Chudnovsky.

• Laure Daviaud (LIP, ENS Lyon)
• Jeudi 10 mars, 10h30
• Salle de réunion du 6ème étage du LIF
• A Generalised Twinning Property for Minimisation of Cost Register Automata
• Weighted automata extend finite-state automata by associating with transitions weights from a semiring S, defining functions from words to S. Recently, cost register automata have been introduced as an alternative model to describe any function realised by a weighted automaton by means of a deterministic machine. Unambiguous weighted automata over a group G can equivalently be described by cost register automata whose registers take their values in G, and are updated by operations of the form x:=y.c, with c in G, and x,y registers. This class is denoted by CRA(G). In this talk, I will introduce a twinning property and a bounded variation property parametrised by an integer k, such that the corresponding notions introduced originally by Choffrut for finite-state transducers are obtained for k=1. Our main result links these notions with the register complexity of CRA(G). More precisely, we prove that given an unambiguous weighted automaton W over an infinitary group G realizing some function f, the three following properties are equivalent: i) W satisfies the twinning property of order k, ii) f satisfies the k-bounded variation property, iii) f can be described by a CRA(G) with at most k registers. Actually, this result is proved in a more general setting, considering machines over the semiring of finite sets of elements from G and is extended to prove a similar result for finite-valued finite-state transducers. Finally, the effectiveness of the constructions leads to decidability/complexity results about the register complexity (i.e. what is the minimal number of registers needed to compute a given function) of cost register automata.
This is a joint work with Pierre-Alain Reynier and Jean-Marc Talbot.

• Jean-Marc Talbot (LIF)
• Jeudi 3 mars, 10h30
• Salle de réunion du 6ème étage du LIF
• Two-Way Visibly Pushdown Automata and Transducers
• Automata-logic connections are pillars of the theory of regular languages. Such connections are harder to obtain for transducers, but a well-known result proved for word-to-word transformations shows that deterministic two-way transducers and monadic second-order (MSO) transducers are equivalent. Nested words are words with a nesting structure, allowing to model unranked trees as their depth-first-search linearisations. In this presentation, we consider transformations from nested words to words, allowing in particular to produce unranked trees if output words have a nesting structure. The model of visibly pushdown transducers allows to describe such transformations, and we propose a simple deterministic extension of this model with two-way moves that has the following properties: i) it is a simple computational model, that naturally has a good evaluation complexity; ii) it is expressive: it subsumes nested word-to-word MSO transducers, and the exact expressiveness of MSO transducers is recovered using a simple syntactic restriction; iii) it has good algorithmic/closure properties: the model is closed under composition with a unambiguous one-way letter-to-letter transducer which gives closure under regular look-around, and has a decidable equivalence problem.

• Denis Kuperberg (TUM Munich)
• Jeudi 25 février, 10h30
• Salle de réunion du 6ème étage du LIF
• Coût de lecture pour les automates et la synthèse
• Je présenterai une nouvelle mesure de complexité pour automates et transducteurs, appelée coût de lecture, qui mesure quelle quantité d'information est lue en moyenne à chaque instant dans un environnement aléatoire. Il est ensuite naturel de chercher à minimiser ce coût de lecture parmi les automates reconnaissant un langage donné, ou les transducteurs solution d'un problème de synthèse. Je présenterai les résultats obtenus en ce sens, ainsi que les problèmes ouverts encore en cours d'investigation.
Ce travail est en collaboration avec Shaull Almagor et Orna Kupferman.

• Séverine Fratani (LIF)
• Jeudi 11 février, 10h30
• Salle de réunion du 6ème étage du LIF
• Homomorphic characterizations of indexed languages and more...
• I will present joint work with El Makki Voundy in which we study a subclass of context-free transducers generating indexed languages from the Dyck language. I will also present several works in progress: context-free transducer generating some subclasses of indexed languages, and logical characterization of context-free transducers.

• Séminaire LDP-MOVE
• Benjamin Monmege (LIF)
• Jeudi 4 février, 11h
• Bâtiment TPR2, 1er étage, amphithéâtre Herbrand
• Logics for Weighted Automata and Transducers
• This talk will present some of the recent results obtained in the community on the relationship between weighted automata and weighted logics. The story started 10 years ago with the introduction of a quantitative semantics for MSO logic over words and an equivalence theorem between weighted automata and a restricted weighted MSO logic. Since then, many extensions have been studied: from words to trees, infinite words, pictures, etc; from semirings to more general weight computations. Also, the proof techniques have matured, from low level, carefully mimicking the classical proofs in the boolean setting, to higher level, using various abstract semantics. We illustrate this evolution by introducing a core weighted logic and its abstract semantics as multisets of weight structures. The equivalence between weighted automata and core weighted logic holds at the level of the abstract semantics. We will also demonstrate the versatility of the weighted automata approach by instantiating it into the transducer setting, showing a possible lead towards the design of an alternative logic for transductions.

• Denis Lugiez (LIF)
• Jeudi 21 janvier, 10h30
• Salle de réunion du 6ème étage du LIF
• Automata
• I will present several extensions of finite state automata and how to decide some logical fragments of the first-order theory of classical data types (lists and queues).

• Vincent Penelle (LIGM)
• Jeudi 14 janvier, 10h30
• Salle de réunion du 6ème étage du LIF
• Rewriting Higher-order Stack Trees
• Higher-order pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the satisfaction of any formula written in monadic second order logic (respectively first order logic with reachability predicates) can be decided on such a graph. The purpose of this talk is to propose a common extension to both higher-order stack operations and ground tree rewriting. We introduce a model of higher-order ground tree rewriting over trees labelled by higher-order stacks (henceforth called stack trees), which syntactically coincides with ordinary ground tree rewriting at order 1 and with the dynamics of higher-order pushdown automata over unary trees. The infinite graphs generated by this class have a decidable first order logic with reachability. Formally, an order n stack tree is a tree labelled by order n-1 stacks. Operations of ground stack tree rewriting are represented by a certain class of connected DAGs labelled by a set of basic operations over stack trees describing of the relative application positions of the basic operations appearing on it. Applying a DAG to a stack tree t intuitively amounts to paste its input vertices to some leaves of t and to simplify the obtained structure, applying the basic operations labelling the edges of the DAG to the leaves they are appended to, until either a new stack tree is obtained or the process fails, in which case the application of the DAG to t at the chosen position is deemed impossible. This model is a common extension to those of higher-order stack operations presented by Carayol and of ground tree transducers presented by Dauchet and Tison. As further results we can define a notion of recognisable sets of operations through a generalisation. The proof that the graphs generated by a ground stack tree rewriting system have a decidable first order theory with reachability is inspired by the technique of finite set interpretations presented by Colcombet and Loding.

• Séminaire LDP-MOVE
• Luigi Santocanale (LIF)
• Jeudi 10 décembre, 10h30
• Salle 105H, 1er étage du bâtiment TPR1
• Fixed-point elimination in the Intuitionisitic Propositional Calculus
• It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras—that is, the algebraic models of the Intuitionistic Propositional Calculus—always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the μ-calculus based on intuitionistic logic is trivial, every μ-formula being equivalent to a fixed-point free formula. We give in this paper an axiomatization of least and greatest fixed-points of formulas, and an algorithm to compute a fixed-point free formula equivalent to a given μ-formula. The axiomatization of the greatest fixed-point is simple. The axiomatization of the least fixed-point is more complex, in particular every monotone formula converges to its least fixed-point by Kleene’s iteration in a finite number of steps, but there is no uniform upper bound on the number of iterations. We extract, out of the algorithm, upper bounds for such n, depending on the size of the formula. For some formulas, we show that these upper bounds are polynomial and optimal.
Joint work with Silvio Ghilardi, Milan, and Maria Gouveia, Lisbon

• Benjamin Monmege (LIF)
• Jeudi 26 novembre, 14h
• Salle de réunion du 6ème étage du LIF
• Interval Iteration Algorithm for MDPs and IMDPs
• Markov Decision Processes (MDP) are a widely used model including both non-deterministic and probabilistic choices. Minimal and maximal probabilities to reach a target set of states, with respect to a policy resolving non-determinism, may be computed by several methods including value iteration. This algorithm, easy to implement and efficient in terms of space complexity, consists in iteratively finding the probabilities of paths of increasing length. However, it raises three issues: (1) defining a stopping criterion ensuring a bound on the approximation, (2) analysing the rate of convergence, and (3) specifying an additional procedure to obtain the exact values once a sufficient number of iterations has been performed. The first two issues are still open and for the third one a "crude" upper bound on the number of iterations has been proposed. Based on a graph analysis and transformation of MDPs, we address these problems. First we introduce an interval iteration algorithm, for which the stopping criterion is straightforward. Then we exhibit convergence rate. Finally we significantly improve the bound on the number of iterations required to get the exact values. We extend our approach to also deal with Interval Markov Decision Processes (IMDP) that can be seen as symbolic representations of MDPs.

• Sebastian Maneth (University of Edinburgh)
• Jeudi 12 novembre, 10h30
• Salle de réunion du 6ème étage du LIF
• Equivalence of deterministic top-down tree-to-string transducers is decidable
• We solve a long standing open problem in formal language theory. For some subclasses we present efficient algorithms: polynomial time for total transducers with unary output alphabet (over a given top-down regular domain language), and co-randomized polynomial time for linear transducers; these results are obtained using techniques from multi-linear algebra. For our main result, we prove that equivalence can be certified by means of inductive invariants using polynomial ideals. This allows us to construct two semi-algorithms, one searching for a proof of equivalence, one for a witness of non-equivalence.

• Pierre-Alain Reynier (LIF)
• Jeudi 5 novembre, 10h30
• Salle de réunion du 6ème étage du LIF
• Decision Problems of Tree Transducers with Origin
• A tree transducer with origin translates an input tree into a pair of output tree and origin info. The origin info maps each node in the output tree to the unique input node that created it. In this way, the implementation of the transducer becomes part of its semantics. We show that the landscape of decidable properties changes drastically when origin info is added. For instance, equivalence of nondeterministic top-down and MSO transducers with origin is decidable. Both problems are undecidable without origin. The equivalence of deterministic top-down tree-to-string transducers is decidable with origin, while without origin it is a long standing open problem. With origin, we can decide if a deterministic macro tree transducer can be realized by a deterministic top-down tree transducer; without origin this is an open problem.
Joint work with Emmanuel Filiot, Sebastian Maneth and Jean-Marc Talbot

• Didier Villevalois (LIF)
• Jeudi 22 octobre, 10h30
• Salle de réunion du 6ème étage du LIF
• Utilisation de la sur-réduction pour le calcul du différentiel entre deux politiques de sécurité
• Un aspect important des politiques de sécurité pour les systèmes d'information concerne le contrôle des droits d'accès aux ressources par leurs utilisateurs. Les politiques de contrôle d'accès peuvent être spécifiées formellement sous la forme de systèmes de réécriture. Cette représentation permet la vérification statique de certaines propriétés des politiques (consistance, complétude, terminaison, ...). Elle offre aussi un moyen opérationnel éprouvé pour résoudre et contrôler les requêtes d'accès, que l'on exprime alors sous la forme d'un terme clos. Nous présentons la sur-réduction, une généralisation de la réécriture, et plus particulièrement la sur-réduction nécessaire la plus extérieure, une variante qui s'applique sur la classe des systèmes de réécriture inductivement séquentiels. Nous montrons comment elle peut être utilisée dans le cadre des politiques de sécurité pour résoudre des patrons de requêtes d'accès, cette fois exprimés sous la forme de termes avec variables. Finalement, nous nous intéressons aux différences entre deux versions d'une même politique de contrôle d'accès. Nous formulons pour cela un problème nouveau, l'identification d'exemples pour lesquels deux systèmes de réécriture présentent un comportement différent. Pour répondre à ce problème, nous proposons une technique basée à la fois sur la transformation des systèmes de réécriture et sur la sur-réduction. Nous discutons de son applicabilité dans des contextes où l'un des deux (ou les deux) systèmes peut ne pas être terminant.

• Antoine Durand-Gasselin (LIF)
• Jeudi 1er octobre, 10h30
• Salle de réunion du 6ème étage du LIF
• Transformations régulières de mots: extension aux data words
• La théorie des langages réguliers permet une analyse qualitative de propriétés sur les mots. Cette théorie a de nombreuses approches (logique avec mso, calculatoire avec les automates déterministes, algébrique, et descriptive avec les expressions regulières). Plutôt que d'étendre cette théorie des languages réguliers aux fonctions de coût pour une analyse qualitative, nous nous plaçons dans le cadre plus général des transformations de mots. Je vous présenterai une classe de transformations régulières de mots qui admet une caractérisation logique avec MSO, ainsi que deux caractérisations computationnelle, la première au moyen des transducteurs déterministes two-way, et la seconde grâce aux streaming string transducers, et vous présenterai une extension aux data words, qui conserve cette triple caractérisation.

• Laure Daviaud (LIF)
• Jeudi 24 septembre, 10h30
• Salle de réunion du 6ème étage du LIF
• Introduction à la théorie profinie des langages réguliers
• Cette présentation a pour vocation d'introduire les concepts de base de la théorie profinie des langages réguliers : - l'ensemble des mots profinis (complétion de A* pour une certaine distance que j'introduirai), - la notion d'équations profinies pour les treillis/algèbres booléennes (éventuellement clos par quotient) de langages réguliers, - la notion de variétés de langages et de monoïdes, le théorème d'Eilenberg et le théorème de Reiterman concernant les identités profinies. Je m'appuierai sur les exemples classiques : variétés des langages star-free, les langages piecewise-testable, et sur un travail en commun avec C. Paperman concernant les équations caractérisant des classes de langages générées par les langages de la forme u*.

• Benjamin Monmege (LIF)
• Jeudi 17 septembre, 10h30
• Salle de réunion du 6ème étage du LIF
• To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games
• Quantitative games are two-player zero-sum games played on directed weighted graphs. Total-payoff games—that can be seen as a refinement of the well-studied mean-payoff games—are the variant where the payoff of a play is computed as the sum of the weights. Our aim is to describe the first pseudo-polynomial time algorithm for total-payoff games in the presence of arbitrary weights. It consists of a non-trivial application of the value iteration paradigm. Indeed, it requires to study, as a milestone, a refinement of these games, called min-cost reachability games, where we add a reachability objective to one of the players. For these games, we give an efficient value iteration algorithm to compute the values and optimal strategies (when they exist), that runs in pseudo-polynomial time. We also propose heuristics to speed up the computations.
Joint work with Thomas Brihaye (UMONS), Gilles Geeraerts (ULB), and Axel Haddad (UMONS).