Seminars

Organized by Karoliina Lehtinen and Nathan Lhote
Takes mostly place in the room 4.05 of building TPR2 at Luminy campus, on Fridays (new! it used to be on Thursdays since the summer 2024) from 10:30 to 12:00
Registration to the mailing list here

List of previous seminars

27/06/2024, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Karoliina Lehtinen
20/06/2024, 10h30 at 4.05 TPR2 Luminy

’‘Synthesis from LTL specifications and examples’‘
by Emmanuel Filiot

We study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against all possible behaviours of the environment. In the variant studied here, the user provides a high level LTL specification S of the system to design, and a set E of examples of executions that the solution must produce. The examples are used to guide the synthesis procedure, and are generalized as much as possible, while preserving realizability of the specification. This talk presents some approach to this problem based on a combination of RPNI automata learning and antichain-based LTL synthesis methods.
13/06/2024, 10h30 at 4.05 TPR2 Luminy

’‘Bisimulation invariant MSO over finite transition systems’‘
by Denis Kuperberg

I will present a recent result obtained in collaboration with Thomas Colcombet and Amina Doumane, on the properties definable in MSO which are bisimulation invariant over finite transition systems. We show that these coincide with mu-calculus-definable properties. This is a variant of a result from Janin and Walukiewicz over general (ie possibly infinite) transition systems. Our proof techniques involve developing an algebraic theory of infinite regular trees, in particular establishing on the way that recognizable languages of regular trees coincide (over regular trees) with MSO definable language of trees.
11/06/2024, 10h30 at 4.05 TPR2 Luminy

’‘Deterministic Suffix-reading Automata’‘
by B Srivathsan

We present deterministic suffix-reading automata (DSA), a new automaton model over finite words. Our motivation for this model comes from specifications which can be described using rules of the form: when a certain sequence of inputs is seen, perform this action. DSAs provide a cleaner representation, compared to deterministic finite automata (DFA), in such situations. Transitions of a DSA are labeled with words. From a state, a DSA triggers an outgoing transition when a word ending with the transition-label is seen. Therefore, rather than moving along an input word letter by letter, a DSA can jump along blocks of letters, with each block ending in a suitable suffix. This feature allows DSAs to recognize regular languages more concisely. In this talk, we will focus on questions around finding a minimal DSA for a regular language. A key technical ingredient that we will describe is a natural method to derive DSAs from a given DFA: a DFA-to-DSA conversion. We make a (surprising) observation that the smallest DSA that we derive from the canonical DFA of a regular language L need not be a minimal DSA for L. This showcases some fundamental bottlenecks (aka. interesting challenges) in determining minimal DSAs. In fact, we prove that given a DFA and a number k, deciding whether there exists a DSA with size less than k is NP-complete. Joint work with R Keerthan, R Venkatesh and Sagar Verma.
30/05/2024, 10h30 at 4.05 TPR2 Luminy

’‘Positionality of omega-regular objectives’‘
by Pierre Ohlmann
16/05/2024, 10h30 at 4.05 TPR2 Luminy

’‘Computability and complexity on the reals’‘
by Manon Blanc
02/05/2024, 10h30 at 4.05 TPR2 Luminy

’‘State-based vs transition-based acceptance for omega-automata’‘
by Antonio Casares
18/04/2024, 9h30 at 4.05 TPR2 Luminy

’‘Lookahead Games for History-Deterministic Parity Automata’‘
by Aditya Prakash

History-deterministic automata are nondeterministic automata in which the nondeterminism that arises while reading a word can be resolved based on the prefix read so far. This talk will be about history-determinism in parity automata, focusing on the questions of recognisability and determinisation. Based on joint work with Rohan Acharya and Marcin Jurdziński.
28/03/2024, 14h30 at 4.05 TPR2 Luminy

’‘The probabilistic Rabin theorem for MSO over infinite trees.’‘
by Michał Skrzypczak

The classical Rabin Tree Theorem states that the monadic second-order (MSO) theory of the full infinite binary tree is decidable. It is usually expressed in terms of satisfiability. Given an MSO formula, decide if there exists a labelling of the tree which satisfies it. A probabilistic variant of this question asks, given a formula, what is the probability that a randomly-generated tree satisfies it. This question has been open, even in the decision variant, is a formula satisfied with a positive probability. During the talk I will present a recent result showing decidability of both probabilistic problems. This is joint work with Damian Niwiński and Paweł Parys, presented at LICS 2023. The technical core of the construction is a variant of a mu-calculus-like formalism, which can be evaluated in orders which are not necessarily lattices. Once an appropriate formula of this formalism is constructed, one can simultaneously compute its semantics over trees, and over a special order on probability distributions. The latter semantics can be formalised in Tarski’s theory of reals and thus effectively computed.
29/02/2024, 10h30 at 4.05 TPR2 Luminy

’‘Explorable automata, expressiveness and decidability’‘
by Olivier Idir

Explorable automata lie on the border between deterministic and nondeterministic automata. They are nondeterministic automata where it is possible to solve the nondeterminism. When given a word spelled one letter at a time, an automaton is said explorable if there exists a way to produce an accepting run by moving forward tokens in a given number of copies of the automata. (the case with exactly one copy corresponds to the history-deterministic case). In this joint work with Denis Kuperberg, I studied explorable automata on infinite words. More specifically, I studied, for different accepting conditions, their expressiveness and the decidability of the explorability property.
22/02/2024, 10h30 at 4.05 TPR2 Luminy

’‘Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous and Broadcasts.’‘
by Lucie Guillou

I will present two recent joint works done with Arnaud Sangnier et Nathalie Sznajder. We study networks of processes that all execute the same finite protocol and communicate synchronously in two different ways. A process can broadcast one message to all other processes or send it to at most one other process. We study two coverability problems with a parameterised number of processes (state coverability and configuration coverability). It is already known that these problem are Ackermann-hard (and decidable) in the general case. This already holds when the processes communicate only by broadcasts. We show that when forbidding broadcasts, the two problems are EXPSPACE-complete. We also study a restriction on the protocol a Wait-Only protocol has no state from which a process can send and receive messages. We show that without broadcasts, both problems are Ptime-complete in this restriction, and with broadcasts, state coverability is Ptime-complete and configuration coverability PSPACE-complete.
26/01/2024, 10h30 at 4.05 TPR2 Luminy

’‘Parameterized Analysis of Distributed Systems’‘
by Chana Weil-Kennedy

My future research project focuses on parameterized verification of distributed systems, where the parameter is often the number of agents present in the system. During my thesis with Javier Esparza in Munich, I studied this kind of problem for subclasses of Petri nets with application to population protocols (a distributed computing model), but also for systems communicating by broadcast or by shared register. Currently in my postdoc I am continuing the study of these systems with simple modes of communication, and I’m also starting to look at language inclusion problems. In the future, I want to continue to analyze distributed systems for which the parameterized problems are not immediately undecidable, broadening the range of formal method techniques used. I will concentrate on distributed systems that are decentralized, symmetric (agent identities are interchangeable), and with local interactions.
07/12/2023, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Aliaume Lopez
16/11/2023, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Léo Henry
09/11/2023, 10h30 at 4.05 TPR2 Luminy

’‘Strategy Complexity of Zero-Sum Games on Graphs’‘
by Pierre Vandenhove

We consider zero-sum turn-based games on graphs, which can be used to model the interaction between a computer system and its environment, assumed to be antagonistic. A crucial question in this framework is the complexity of strategies. A standard measure of strategy complexity is the amount of memory needed to implement winning strategies for a given objective; how much information should be remembered about the past to make optimal decisions about the future? Proving the existence of bounds on memory requirements has historically had a significant impact. Particularly relevant are the finite-memory-determined objectives (for which winning strategies can be implemented with finite memory), as they allow for implementable controllers. In this talk, we review recent works on this topic. First, we show characterizations of a variant of finite-memory determinacy in multiple contexts. In particular, we show that understanding the memory requirements in one-player games (i.e., the simpler situation of games where the same player controls all the actions) leads to bounds on memory requirements in two-player zero-sum games. We also show a strong link between finite-memory determinacy and omega-regularity. Second, we show effective characterizations of the precise memory requirements of subclasses of the omega-regular objectives and discuss the related decision problems. We discuss that, perhaps surprisingly, the memory requirements of omega-regular objectives are not completely settled.
19/10/2023, 10h30 at 4.05 TPR2 Luminy

’‘An Automata Theoretic Characterization of Weighted First-Order Logic’‘
by Benjamin Monmege

Since the 1970s with the work of McNaughton, Papert and Schützenberger, a regular language is known to be definable in the first-order logic if and only if its syntactic monoid is aperiodic. This algebraic characterisation of a fundamental logical fragment has been extended in the quantitative case by Droste and Gastin, dealing with polynomially ambiguous weighted automata and a restricted fragment of weighted first-order logic. In the quantitative setting, the full weighted first-order logic (without the restriction that Droste and Gastin use, about the quantifier alternation) is more powerful than weighted automata, and extensions of the automata with two-way navigation, and pebbles or nested capabilities have been introduced to deal with it. In this work, we characterise the fragment of these extended weighted automata that recognise exactly the full weighted first-order logic, under the condition that automata are polynomially ambiguous.
28/09/2023, 10h30 at 4.05 TPR2 Luminy

’‘Broadcast networks with registers’‘
by Corto Mascle
06/07/2023, 11h00 at Luminy TPR2

’‘Integer Parameter Synthesis for Parametric Timed Automata’‘
by Arnab Sur

Parametric Timed Automata (PTA) were introduced by Alur et al. as a formalism to model real-time systems with certain timing parameters. The Parameter Synthesis Problem for Reachability asks for all the values of the parameters for which there is an accepting run in the corresponding timed automaton. However, the problem is undecidable in general. We focus on a decidable subclass of PTA where the domain of the parameters is restricted to a bounded set of integers. We shall discuss two approaches to the problem.
22/06/2023, 9h15 at 4.05 TPR2 Luminy

’‘Algebraic Recognition of Regular Functions’‘
by Nguyễn Lê Thành Dũng, aka Tito

We consider regular string-to-string functions, i.e. functions that are recognized by copyless streaming string transducers, or any of their equivalent models, such as deterministic two-way automata. We give yet another characterization, which is very succinct: finiteness-preserving functors from the category of semigroups to itself, together with a certain output function that is a natural transformation. (Joint work with Mikołaj Bojańczyk.)
08/06/2023, 10h30 at 4.05 TPR2 Luminy

’‘Verification of weak memory models’‘
by Elli Anastasiadi (Uppsala University)

Distributed algorithms and architectures are everywhere, and along with them bring faster computation and harder verification. In the heart of the verification effort lies always the the understanding of how exactly a piece of software can execute, and it is exactly there where parallelism and concurrency introduce extra potential execution scenaria and complicate the process. The concept of weak memory approaches this issue from an applied perspective, where the implementation of a system is what defines what potential executions can occur. Unfortunately the outcome is usually that many, additional to the expected ones, program behaviours are present, and thus the program’s safety is even more at risk. In this talk we will first look at exactly how weak memory presents itself through different implementations and then discuss some important concepts and problems about the verification of programs in those circumstances.
30/03/2023, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Benjamin Bordais
16/03/2023, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Chana Weil-Kennedy
12/01/2023, 10h30 at 4.05 TPR2 Luminy

’‘Approximation and semantic tree-width of conjunctive regular-path queries’‘
by Rémi Morvan
01/12/2022, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Pierre Ohlmann
10/11/2022, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Léo Henry
20/10/2022, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Léonard Brice
13/10/2022, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Guillaume Maurras
13/06/2022, 10h30 at 4.05 TPR2 Luminy

’‘Un contrôle d’accès basé sur la provenance pour les systèmes collaboratifs’‘
by Alba Martinez Anton

Ces dernières années il y a eu explosion du nombre et de la variété des systèmes collaboratifs comme les réseaux sociaux, les drive partagés, les éditeurs de textes en ligne,… Ces systèmes viennent brouiller les frontières de ce qui était bien défini dans les contrôles d’accès classiques: qui est le propriétaire, qui choisit les droits sur tel objet, qui a des droits sur quel objet,…? Dans les systèmes collaboratifs, les utilisateurs sont au centre, ce sont eux qui deviennent les gestionnaires de leur propre privacité. Il faut donc des contrôles d’accès qui font sens aux yeux d’utilisateurs lambda. En se basant sur la provenance des objets et les relations entre les utilisateurs, nous proposons un contrôle d’accès modélisant ces différentes interconnexions permettant aux utilisateurs d’avoir un meilleur contrôle sur leur privacité.
12/05/2022, 10h30 at 4.05 TPR2 Luminy

’‘Synthèse de fonctions d’observation pour les jeux à information imparfaite’‘
by Nathan Lhote
28/04/2022, 10h30 at 4.05 TPR2 Luminy

’‘Continuous rational functions are deterministic regular’‘
by Gaëtan Douéneau-Tabot
07/04/2022, 10h30 at 4.05 TPR2 Luminy

’‘A Symmetric Attractor-Decomposition Lifting Framework for Solving Parity games.’‘
by Thejaswini Raghavan

In this talk, we will introduce the framework of Symmetric Attractor-Decomposition Lifting. We show how this helps us understand as well as obtain a quadratic improvement to the runtime of several pre-existing algorithm. This is joint work with Marcin Jurdzinski, Remi Morvan and Pierre Ohlmann.
24/03/2022, 10h30 at 4.05 TPR2 Luminy

’‘Quantitative synthesis and history-determinism’‘
by Karoliina Lehtinen

Le déterminisme en histoire est une forme légère de non-déterminisme qui permet souvent plus d’expressivité ou de concision que le déterminisme, tout en conservant certaines bonnes propriétés algorithmiques des automates déterministes. Dans cet exposé, j’expliquerai le pourquoi certains problèmes de synthèse reviennent à décider si un automate est déterministe en histoire. Je présenterai quelques techniques de résolution de problèmes de synthèse quantitative inspirées d’algorithmes pour décider de l’histoire-déterminisme dans le cadre omega-régulier. Il y aura beaucoup de jeux, et encore plus de jetons.
24/02/2022, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Nguyễn Lê Thành Dũng, aka Tito
13/01/2022, 10h30 at 4.05 TPR2 Luminy

’‘TBA’‘
by Ismaël Jecker
09/12/2021, 10h30 at Luminy TPR2 4.05

’‘How undecidable are HyperLTL and HyperCTL*?’‘
by Marie Fortin (University of Liverpool)
02/12/2021, 10h30 at Luminy TPR2 4.05

’‘On a correspondence between memory structures for Muller games and Rabin automata’‘
by Antonio Casares (LaBRI, Université de Bordeaux)
25/11/2021, 10h30 at Luminy TPR2 4.05

’‘The boundedness and zero isolation problems for weighted automata over nonnegative rationals’‘
by Filip Mazowiecki (University of Warsaw)
04/11/2021, 10h30 at Luminy TPR2 4.05

’‘Positionalité pour un joueur dans les jeux à durée infinie’‘
by Pierre Ohlmann (IRIF, Université de Paris)

Dans cet exposé, je présenterai une caractérisation de la posionalité pour un joueur (half-positionality) dans les jeux à durée infinie sur les graphes : une condition W ayant une lettre neutre est uniformément positionnelle sur toutes les arènes si et seulement si pour tout cardinal kappa, il existe un graphe monotone bien-ordonné qui est W-universel pour les graphes de cardinal kappa. C’est la premiere caractérisation de la posionalité pour un joueur. J’expliquerai ce que le théoreme signifie, comment on le prouve, et pourquoi il est intéressant.
23/09/2021, 10h30 at Luminy TPR2 4.05

’‘Décidabilité de l’accessibilité dans les réseaux de Petri’‘
by Denis Lugiez (LIS)
17/06/2021, 14h00 at Zoom

’‘An Algebraic Characterisation of First-Order Logic with Neighbour’‘
by Dhruv Nevatia (LIS and CMI)

We give an algebraic characterisation of first-order logic with the neighbour relation, on finite words. For this, we consider languages of finite words over alphabets with an involution on them. The natural algebras for such languages are involution semigroups. To characterise the logic, we define a special kind of semidirect product of involution semigroups, called the locally hermitian product. The characterisation theorem for FO with neighbour states that a language is definable in the logic if and only if it is recognised by a locally hermitian product of an aperiodic commutative involution semigroup, and a locally trivial involution semigroup. We then define the notion of involution varieties of languages, namely classes of languages closed under Boolean operations, quotients, involution, and inverse images of involutory morphisms. An Eilenberg-type correspondence is established between involution varieties of languages and pseudovarieties of involution semigroups.
29/04/2021, 10h30 at Zoom

’‘Saison indécidabilité/impossibilité: Théorèmes de Rice dans les automates cellulaires’‘
by Guillaume Theyssier (I2M, CNRS)
01/04/2021, 10h30 at Zoom

’‘Prime languages’‘
by Ismaël Jecker (IST Austria)

A regular language L of finite words is composite if there are regular languages L1, L2, …, Lt such that L is equal to the intersection of the Li, and the index (number of states in a minimal DFA) of every language Li is strictly smaller than the index of L. Otherwise, L is prime. This notion of primality was introduced by Orna Kupferman and Jonathan Mosheiff in 2015, and the complexity of deciding the primality of the language of a given DFA was left open, with a doubly-exponential gap between the upper and lower bounds. In this talk, I will present some recent results concerning primality in some subclasses of regular languages. First, we will consider unary regular languages, namely regular languages with a singleton alphabet. A unary language can be interpreted as a set of positive integers, making the study of prime unary languages close to that of primality in number theory. We will see that the setting of languages is richer. In particular, while every composite number is the product of two smaller numbers, the number t of languages necessary to decompose a composite unary language induces a strict hierarchy. In addition, a primality witness for a unary language L, namely a word that is not in L but is in all products of languages that contain L and have an index smaller than L’s, may be of exponential length. Still, we are able to characterize compositionality by structural properties of a DFA for L, leading to a LogSpace algorithm for checking primality of unary DFAs. Second, I will present our (ongoing) work on regular languages definable by permutation DFAs, namely DFAs whose transition monoid is a group. We will see that, while we cannot apply the exact same techniques used in the unary setting, they can be adapted to obtain an NP algorithm checking primality of permutation DFAs, improving the previously known PSpace algorithm.
11/03/2021, 10h30 at Luminy TPR2 4.05 and Zoom

’‘Saison indécidabilité/impossibilité: Undecidability of halting of one-Clause logic program’‘
by Denis Lugiez (LIS)
25/02/2021, 10h30 at Luminy TPR2 4.05 and Zoom

’‘Saison indécidabilité/impossibilité: Pavages : transducteurs et indécidabilité dans les systèmes affines’‘
by Pierre Guillon (I2M, CNRS)
11/02/2021, 10h30 at Zoom

’‘Saison indécidabilité/impossibilité: Pavages : apériodicité et preuve substitutive de l’indécidabilité’‘
by Guilhem Gamard (LIS)
21/01/2021, 10h30 at Luminy TPR2 4.05 and Zoom

’‘Saison indécidabilité/impossibilité: Explorabilité d’un réseau avec des jumelles et indécidabilité de la simple connexité’‘
by Jérémie Chalopin (LIS)
22/01/2021, 14h at Luminy TPR2 4.05 and Zoom

’‘Between determinism and nondeterminism, what are good-for-games automata good for?’‘
by Karoliina Lehtinen (LIS)

Nondeterminism probably makes your favourite automata model more expressive, or at least more succinct, than determinism. However, nondeterminism comes with higher algorithmic complexity. Good-for-games automata, also known as history deterministic automata, lie in between deterministic and nondeterministic models, trying to salvage some of the expressivity and succinctness of nondeterminism, without giving up on the nice algorithmic properties of deterministic automata. In this talk, I will give an overview of good-for-games automata, survey recent developments in the area for regular, dushdown and timed automata, and point to some of the hard questions that remain unanswered and some areas that remain unexplored.
14/01/2021, 10h30 at Luminy TPR2 4.05 and Zoom

’‘Saison indécidabilité/impossibilité: Impossibilité de l’élection déterministe et probabiliste dans les anneaux anonymes’‘
by Emmanuel Godard (LIS)
15/12/2020, 10h30 at Zoom

’‘Expressivity of first-order logic, star-free propositional dynamic logic and communicating automata’‘
by Marie Fortin (University of Liverpool)

This talk is concerned with the expressive power of first-order logic and other formalisms over different classes of ordered structures, among which MSCs (Message Sequence Charts), a standard model for executions of message-passing systems. This study is motivated by two classic problems: the k-variable property, that is, the equivalence of first-order logic and its k-variable fragment over certain classes of structures, and the study of logic-automata connections, in the spirit of Büchi-Elgot-Trakhtenbrot theorem. Our approach relies on star-free propositional dynamic logic (star-free PDL), a variant of PDL with the same expressive power as the 3-variable fragment of first-order logic. We start by studying the expressive power of star-free PDL over linearly ordered structures with unary and binary predicates. We show that under certain monotonicity conditions, star-free PDL becomes as expressive as first-order logic. This implies that any first-order formula can then be rewritten into an equivalent formula with at most 3 variables. This result applies to various natural classes of structures, generalizing several known results and answering some open questions. We then focus on MSCs, to which this first result also applies. We use star-free PDL to address another important problem: the synthesis of communicating finite-state machines (CFMs) from first-order specifications. CFMs are a model of concurrent systems in which a fixed number of finite-state automata communicate through unbounded FIFO channels. They accept languages of MSCs. While logical characterizations of the expressive power of CFMs have been established under different restrictions (bounding the size of the communication channels, or removing the ‘happened-before’ relation from the logic), the following question had remained open in the general case: can every first-order formula over MSCs be translated into an equivalent CFM? We prove that this is the case, using star-free PDL as an intermediate language.
08/12/2020 at Zoom

’‘On the Monniaux Problem in abstract interpretation’‘
by Engel Lefaucheux (Max-Planck Institute for Software Systems, Sarrebrucken)

The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program P, a safety (e.g., non-reachability) specification φ, and an abstract domain of invariants D, does there exist an inductive invariant in D guaranteeing that program P meets its specification φ. The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers. In this talk, I’ll present a select overview and survey of work on this problem, and discuss some recent results for semilinear invariants for unguarded affine programs.
30/11/2020 at Zoom

’‘Computability and Continuity of Data Word Functions Defined by Transducers’‘
by Léo Exibard (LIS-ULB)

Last year, Dave, Filiot, Krishna and Lhote established an equivalence between the notions of continuity and computability for functions over infinite (aka omega-) words[*]. In this talk, we extend the study to the case of an infinite alphabet, i.e. to the problem of synthesizing computable functions over data omega-words. The notion of computability is defined through Turing machines with infinite inputs which can produce the corresponding infinite outputs in the limit. We use non-deterministic transducers equipped with registers, an extension of register automata with outputs, to specify functions. Such transducers may not define functions but more generally relations of data omega-words, and we show that it is PSpace-complete to test whether a given transducer defines a function. Then, given a function defined by some register transducer, we show that it is decidable (and again, PSpace-complete) whether such function is computable. As for the finite alphabet case, we show that computability and continuity coincide for functions defined by register transducers, and show how to decide continuity. Nathan presented those results at the MoVe seminar last september, but this talk will be self-contained.
23/11/2020 at Zoom

’‘Caractérisation logique de langages d’ordre supérieur - introduction’‘
by Guillaume Maurras (LIS)
05/11/2020 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Les automates circulaires sur les rationnels’‘
by Louis-Marie Dando (LIS)

Dans cet exposé, je vous présenterai quelques résultats obtenus durant ma thèse. Le premier est que sur les semi-anneaux rationnellement additifs (et on peut étendre aux rationnels), les automates circulaires et les expressions de Hadamard réalisent les mêmes séries. Ce résultat est constructif. Le second résultat est que l’on peut transformer un automate two-way en un automate circulaire sur Q.
21/10/2020, 14h00 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Stackless processing of streamed trees’‘
by Charles Paperman (Université de Lille)

In this talk I will first present the state of the art of efficiency implementation of streaming-text algorithms on modern architecture. Then some recent results on the extraction of information on streamed of structured documents without stack overhead.
01/10/2020 and 08/10/2020 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Dynamics on Games: Simulation-Based Techniques and Applications to Routing’‘
by Benjamin Monmege (LIS)

We consider multi-player games played on graphs, in which the players aim at fulfilling their own (not necessarily antagonistic) objectives. In the spirit of evolutionary game theory, we suppose that the players have the right to repeatedly update their respective strategies (for instance, to improve the outcome w.r.t. the current strategy profile). This generates a dynamics in the game which may eventually stabilise to an equilibrium. The talk will start with a short presentation of evolutionay game theory. Then, I will present our twofold contribution. First, we aim at drawing a general framework to reason about the termination of such dynamics. In particular, we identify preorders on games (inspired from the classical notion of simulation between transitions systems, and from the notion of graph minor) which preserve termination of dynamics. Second, we show the applicability of the previously developed framework to interdomain routing problems. This is a joint work with Thomas Brihaye, Gilles Geeraerts, Marion Hallet and Bruno Quoitin.
24/09/2020, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Reaching Your Goal Optimally by Playing at Random with no Memory’‘
by Julie Parreaux (LIS)

Shortest-path games are two-player zero-sum games played on a graph equipped with integer weights. One player, that we call Min, wants to reach a target set of states while minimising the total weight, and the other one has an antagonistic objective. This combination of a qualitative reachability objective and a quantitative total-payoff objective is one of the simplest settings where Min needs memory (pseudo-polynomial in the weights) to play optimally. In this article, we aim at studying a tradeoff allowing Min to play at random, but using no memory. We show that Min can achieve the same optimal value in both cases. In particular, we compute a randomised memoryless ε-optimal strategy when it exists, where probabilities are parametrised by ε. We also show that for some games, no optimal randomised strategies exist. We then characterise, and decide in polynomial time, the class of games admitting an optimal randomised memoryless strategy. This is a joint work with Benjamin Monmege and Pierre-Alain Reynier.
10/09/2020, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Continuity and computability of regular functions’‘
by Nathan Lhote (LIS)

Regular functions from infinite words to infinite words can be equivalently specified by MSO-transducers, streaming omega-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. Even though regular functions are robustly characterised by several finite-state devices, even the subclass of rational functions may contain functions which are not computable ((by a Turing machine with infinite input). This paper proposes a decision procedure for the following synthesis problem: given a regular function f (equivalently specified by one of the aforementioned transducer model), is f computable and if it is, synthesize a Turing machine computing it. For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in NLogSpace (it was already known to be in PTime by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.
05/03/2020, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Stone Duality and the Substitution Principle’‘
by Célia Borlido (Université de Coimbra)«/b>

Fragments of first-order logic defining regular languages of words can be studied inductively via the so-called “Substitution Principle”. Through this principle, one is able to study logic fragments by successively adding a layer of quantifiers, which is in turn algebraically modeled by the semidirect product of suitable monoids. In this talk we will see that, by interpreting the “Substitution Principle” from the standpoint of Stone duality, one is able to extend it beyond regularity and obtain topo-algebraic counterparts for classes of languages defined by arbitrary first-order logic fragments. As in the regular setting, applying a layer of quantifiers is modeled by a semidirect product construction for suitable recognizers. Such recognizers were proposed by Gehrke, Grigorieff and Pin in 2010 as the topo-algebraic objects to handle not-necessarily regular languages, and they generalize the classical finite and profinite monoids. This is based on joint work with Czarnetzki, Gehrke and Krebs. All concepts related to Stone duality will be introduced during the talk.
20/02/2020, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Saison indécidabilité/impossibilité: Impossibilité de l’accord k-ensembliste’‘
by Damien Imbs (LIS)
13/02/2020, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Updatable Parametric Timed Automata: Decidability, Algorithms, and Application to Security’‘
by Mathias Ramparison (Université de Luxembourg)

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

’‘Saison indécidabilité/impossibilité: Problèmes indécidables sur les transducteurs’‘
by Théodore Lopez and Pierre-Alain Reynier (LIS)
16/01/2020, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Synchronized word relations’‘
by Maria Emilia Descotte (LaBRI, Université de Bordeaux)

A natural approach to defining binary word relations over a finite alphabet A is through two-tape finite state automata, which can be seen as regular languages L over {1,2}xA, where (i,a) is interpreted as reading letter a from tape i. Thus, a word w of the language L denotes the pair (u_1,u_2) in AxA in which u_i is the projection of w onto i-labelled letters. While this formalism defines the well-studied class of Rational relations (a.k.a. non-deterministic finite state transducers), enforcing restrictions on the reading regime from the tapes, that we call synchronization, yields various sub-classes of relations. Such synchronization restrictions are imposed through regular properties on the projection of the language onto {1,2}. In this way, for each regular language C over the alphabet {1,2}, one obtains a class Rel(C) of relations, such as the classes of Regular, Recognizable, or length-preserving relations, as well as (infinitely) many other classes. During the talk, we will introduce the formalism of synchronized relations along with its basic properties without assuming any previous knowledge about it. Then we will give the main ideas for the proof of several recent results on the subject. To begin, we will discuss the problem of containment for synchronized classes of relations: given C,D regular languages over the alphabet {1,2}, is Rel(C) a subset of Rel(D)? We will show a characterization in terms of C and D which gives a decidability procedure to test for class inclusion. Then we will move to the problem of deciding whether a given class of synchronized relations is closed under paradigmatic operations such as intersection, complement, etc. We will prove the decidability of these problems by giving a characterization of the classes that are indeed closed under those operations. We will finally make a link between these closure properties and classical problems within the theory of transducers. Only basic knowledge about automata theory will be required.
28/11/2019, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Opacity of a Stochastic System: Maximisation versus Minimisation’‘
by Engel Lefaucheux (Max-Planck Institute for Software Systems, Sarrebrucken)

This talk explores opacity questions where an observation function provides to an external attacker a view of the states along executions and secret executions are those visiting some state from a fixed subset. Disclosure occurs when the observer can deduce from a finite observation that the execution is secret. In a probabilistic and non deterministic setting, where an internal agent can choose between actions, there are two points of view, depending on the status of this agent: the successive choices can either help the attacker trying to disclose the secret, if the system has been corrupted, or they can prevent disclosure as much as possible if these choices are part of the system design. In the former situation, corresponding to a worst case, the disclosure value is the supremum over the strategies of the probability to disclose the secret (maximisation), whereas in the latter case, the disclosure is the infimum (minimisation). I will consider both quantitative problems (comparing the optimal value with a threshold) and qualitative ones (when the threshold is zero or one) for a fixed or a finite horizon and discuss the strange asymmetry existing between maximisation and minimisation problems.
21/11/2019, 14h00 at Saint Charles, Bâtiment 5, Salle 18

’‘Saison indécidabilité/impossibilité: Undecidability of strong bisimulation of BPP with states’‘
by Denis Lugiez (LIS)
14/11/2019, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Some recent results on polyregular functions’‘
by Nathan Lhote (University of Warsaw)

Regular word functions are well-studied and correspond to several different formalisms: MSO-transductions, two-way transducers, one-way transducers with registers (SST), as well as several formalisms of regular expressions for transducitons. Polyregular functions were introduced last year in an article of Bojańczyk, where they are shown to be characterized by 4 different models of computation. The first one, which comes from [Milo, Suciu, Vianu ‘03], is an extension of two-way transducers with a bounded number of pebbles. Polyregular functions have polynomial size increase, which means in particular that they strictly subsume regular functions; however, they still retain some of the nice properties of regular functions, such as preserving regular languages by inverse image, and being closed under composition. In this talk we present polyregular functions, and two results that were obtained this year.
07/11/2019, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Circular proof systems for regular expressions’‘
by Denis Kuperberg (CNRS, LIP, ENS Lyon)

Cyclic proofs are a class of formal proof systems that allow some kind of circular reasoning. Unlike classical proofs, represented by finite trees with axioms as leaves, cyclic proofs are represented by trees containing infinite branches. We investigate the computational content of a cyclic proof system for Kleene algebra. If e,f are regular expressions, the sequent e -> f can be proved in the cyclic proof system if and only if L(e) is contained in L(f). Different proofs of the same sequent can be interpreted as different programs mapping each word of e to a witness that it is in f. We show that depending on the particular rules allowed in the system, the computational content of proofs matches different complexity classes. In particular, if the contraction rule is added, we obtain a rich class of languages, for which we exhibit an equivalent automaton model: Jumping Multihead automata. In presence of the cut rule, corresponding to composition of programs, we can define primitive recursive functions (without contraction) or functions from System T (with contraction). This is joint work with Laureline Pinault and Damien Pous.
24/10/2019, 11h at Amphithéâtre Herbrand (I2M, TPR2, 1er étage), Luminy

’‘Quasi-polynomial techniques for parity games and and other problems’‘
by Karoliina Lehtinen (University of Liverpool)

Parity games are central to the verification and synthesis of reactive systems: various model-checking, realisability and synthesis problems reduce to solving these games. Solving parity games – that is, deciding which player has a winning strategy – is one of the few problems known to be in both UP and co-UP yet not known to be in P. So far, the quest for a polynomial algorithm has lasted over 25 years. In 2017 a major breakthrough occurred: parity games are solvable in quasi-polynomial time. Since then, several seemingly very distinct quasi-polynomial algorithms have been published, and some of these ideas have been used to solve other automata-theoretic problems. In this talk, I will give an overview of these developments and the state-of-the art, with a slight automata-theoretic bias.
03/10/2019, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach’‘
by Benjamin Monmege (LIS)

This talk will survey existing and new results on the robust controller synthesis in timed Büchi automata. The goal of the controller is to play according to an accepting lasso of the automaton, while resisting to timing perturbations chosen by a competing environment. We will first recall how the problem is shown to be PSPACE-complete using game and region-based techniques. The new contribution is a purely symbolic computation using zones only, thus more resilient to state-space explosion problem. The key ingredient is the introduction of branching constraint graphs allowing to decide in polynomial time whether a given lasso is robust, and even compute the largest admissible perturbation if it is. We also make an original use of constraint graphs in this context in order to test the inclusion of timed reachability relations, crucial for the termination criterion of our algorithm. Our techniques are illustrated using a case study on the regulation of a train network. The new results are a joint work with Damien Busatto-Gaston, Pierre-Alain Reynier and Ocan Sankur.
19/09/2019, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de l’ancienne BU), Luminy

’‘Determinisation of Finitely-Ambiguous Copyless Cost Register Automata’‘
by Théodore Lopez (LIS)

Cost register automata (CRA) are machines reading an input word while computing values using write-only registers: values from registers are combined using the two operations, as well as the constants, of a semiring. Particularly interesting is the subclass of copyless CRAs where the content of a register cannot be used twice for updating the registers. Originally deterministic, non-deterministic variant of CRA may also be defined: the semantics is then obtained by combining the values of all accepting runs with the additive operation of the semiring (as for weighted automata). We show that finitely-ambiguous copyless non-deterministic CRAs (i.e. the ones that admit a bounded number of accepting runs on every input word) can be effectively transformed into an equivalent copyless (deterministic) CRA, without requiring any specific property on the semiring. As a corollary, this also shows that regular look-ahead can effectively be removed from copyless CRAs. This is a joint work with Benjamin Monmege and Jean-Marc Talbot.
20/06/2019, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Séparer des mots avec des automates à poids’‘
by Glenn Merlet (I2M, AMU)

Une des questions les plus simples que l’on puisse poser à une machine est : ces deux mots sont-ils égaux ? Le problème de la séparation des mots est le suivant: étant donné une paire de mots, quelle est la taille du plus petit d’automate (déterministe) nécessaire pour les séparer (i.e en accepter un et pas l’autre). Si les deux mots sont de longueur différentes, il suffit de prendre un automate cyclique qui calcule la longueur modulo un petit entier bien choisi. Si les longueurs sont égales, le problème est étonnament difficile : la borne inf sur le nombre d’états de l’automate nécessaire est logarithmique, tandis que la borne sup est O(n^{2/5} (log n)^{3/5}). Si l’on s’autorise des automates à poids, on peut imaginer séparer toutes les paires de mots avec des automates d’une taille donnée. C’est le cas pour des poids dans R muni des opérations usuelles. Dans un travail récent avec Zur Izhakian, nous avons trouvé pour tout n des paires de mots impossibles à séparer avec des automates max-plus, même non déterministes. Dans cet exposé, je présenterai des élements de ce travail, fondé sur les différentes notions de rang pour les matrices tropicales, et un état des lieu des différentes bornes connues pour différentes versions de ce problème.
07/02/2019, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Finding paths in large graphs’‘
by Bruno Guillon (CRIStAL, Université de Lille)

When dealing with large graphs, classical algorithms for finding paths such as Dijkstra’s Algorithm are unsuitable, because they require to perform too many disk accesses. To avoid this cost, while keeping a data structure of size quasi-linear in the size of the graph, we propose to guide the path search with a distance oracle, obtained from a topological embedding of the graph. I will present fresh experimental research on this topic, in which we obtain graph embeddings using learning algorithms from natural language processing. On some graphs, such as the graph of publications of DBLP, our topologically-guided path search allows us to visit a small portion of the graph only, in average. This is joint work with Charles Paperman.
24/01/2019, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Specifying, Modeling, and Gauging Security in inter-disciplinary Systems’‘
by Samir Ouchani (CESI eXia)

Nowadays systems are complex by controlling and integrating entities of various natures and size: physics, information, computational, network elements, or even of social nature that are combined to execute a precise task. The main difficulty in analyzing this type of system lies in the modeling of each component separately, then the way in which the various components inter-operate especially with the existing of an important number of connected low-energy objects. This talk aims to answer these problems by proposing a formal and practical framework where it is possible to model different aspects of components, their connectivity, and to assess how well they are secure. First, the talk details the meta-architecture proposed for these systems and its dedicated analysis approach. Then, it introduces a mechanism to specify and to constraint security in such system. In addition, it will be an opportunity to detail my current research activities for a perspective collaboration.
25/10/2018, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty’‘
by Pierre-Alain Reynier (LIS)

In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing constraints and variable energy rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.
13/09/2018, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Gröbner bases are easy’‘
by Denis Lugiez (LIS)

Polynomials ideals are finitely generated but some generating sets are more interesting than others: Gröbner basis allow a simple membership test. I will show how to compute a Gröbner basis from any basis using a completion-like algorithm relying on simple and powerful ideas. Disclaimer: all these results have been well known since at least 40 years…
12/07/2018, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘An efficient approach for the (extended) evaluation of ABAC policies’‘
by Nicola Zannone (Eindhoven University of Technology)

A main challenge of attribute-based access control (ABAC) is the handling of missing information. Several studies show that the way standard ABAC mechanisms (e.g., XACML) handle missing information is flawed, making ABAC policies vulnerable to attribute-hiding attacks. Recent work addressed the problem of missing information in ABAC by introducing the notion of extended evaluation, where the evaluation of a query considers all possible ways of extending that query. This method counters attribute-hiding attacks, but a naive implementation is intractable, as it requires an evaluation of the whole query space. In this paper, we present an efficient extended ABAC evaluation method that relies on the encoding of ABAC policies as multiple Binary Decision Diagrams (BDDs), and on the specification of query constraints to avoid including the evaluation of queries that do not represent a valid state of the system. We illustrate our approach on two real-world case studies, which would be intractable with the original method and are analyzed in seconds with our method.
28/06/2018, 10h00 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Groupe de travail : Algebraic methods to decide automata’‘
by Benjamin Monmege (LIS)
14/06/2018, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Beyond admissibility: Dominance betweens chains of strategies’‘
by Marie van den Bogaard (Université libre de Bruxelles)

In this talk, we focus on the concept of rational behaviour in multi-player games on finite graphs, taking the point of view of a player that has access to the structure of the game but cannot make assumptions on the preferences of the other players. In the qualitative setting, admissible strategies have been shown to fit the rationality requirements, as they coincide with winning strategies when these exist, and enjoy the fundamental property that every strategy is either admissible or dominated by an admissible strategy. However, as soon as there are three or more payoffs, one finds that this fundamental property does not necessarily hold anymore: one may observe chains of strategies that are ordered by dominance and such that no admissible strategy dominates any of them. Thus, to recover a satisfactory rationality notion (still based on dominance), we depart from the single strategy analysis approach and consider instead chains of strategies as families of behaviours. We establish a sufficient criterion for games to enjoy a similar fundamental property, ie, all chains are below some maximal chain, and, as an illustration, we present a class of games where admissibility fails to capture some intuitively rational behaviours, while our chain-based analysis does.
31/05/2018, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Nash equilibria in games on graphs with a public signal monitoring’‘
by Patricia Bouyer-Decitre (LSV, ENS Paris-Saclay, CNRS)

In this talk, I will start by presenting all basic material about games on graphs, which will be useful. I will then focus on pure Nash equilibria in such games on graphs, with an imperfect monitoring based on a public signal. In such games, deviations and players responsible for those deviations can be hard to detect and track. I will present a generic epistemic game abstraction, which conveniently allows to represent the knowledge of the players about these deviations, and give a characterization of Nash equilibria in terms of winning strategies in the abstraction. I will then explain how that abstraction helps providing algorithms for computing Nash equilibria for some payoff functions.
18/05/2018, 14h00 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘A journey through negatively-weighted timed games: undecidability, decidability, approximability’‘
by Benjamin Monmege (LIS)

Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the accumulated weight while reaching a target. Used in a reactive synthesis perspective, this quantitative extension of timed games allows one to measure the quality of controllers in real-time systems. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. However, for a few years now, we explored, and we continue to explore, the world of weighted timed games with negative weights too, in order to get a more useful modelling mechanism. This gave rise to stronger undecidability results, but we also discovered new decidable fragments. In this talk, I will survey these results: decidability when limiting the number of distinct weights in the game, using corner-point abstraction techniques; decidability for a large fragment of one-clock weighted timed games, and for the so-called divergent weighted timed games, using value iteration schemes; approximability in the case of the so-called almost-divergent weighted timed games.
17/05/2018, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Polynomial Invariants for Affine Programs’‘
by James Worrell (University of Oxford)

Automatically generating invariants is a fundamental challenge in program analysis and verification. In this talk we give a select overview of previous work on this problem, starting with Michael Karr’s 1976 algorithm for computing affine invariants for affine programs (i.e., programs in which all assignments are affine and which conditionals are abstracted by non-determinism) and proceeding to subsequent work on computing polynomial invariants for affine programs. We then present our main result—an algorithm to compute all polynomial invariants that hold at each location of a given a affine program. Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate. This is joint work with Ehud Hrushovski, Joel Ouaknine, and Amaury Pouly.
03/05/2018, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Costs and Rewards in Priced Timed Automata’‘
by Mahsa Shirmohammadi (LIS)

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.
19/04/2018, 11h00 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘From Two-Way Transducers to Regular Functions Expressions’‘
by Nicolas Baudru (LIS)

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.
12/04/2018, 10h30 at Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy

’‘Two-Way Parikh Automata with a Visibly Pushdown Stack’‘
by Jean-Marc Talbot (LIS)

We investigate the complexity of the emptiness problem for Parikh automata equipped with a pushdown stack. Pushdown Parikh automata extend pushdown automata with counters which can only be incremented and an acceptance condition given as a semi-linear set over the final values of the counters. We show that the non-emptiness problem both in the deterministic and non-deterministic cases is NP-ccomplete. If the input head can move in a two-way fashion, emptiness gets undecidable, even if the pushdown stack is visibly and the automaton deterministic. We define a restriction, called the single-use restriction, to recover decidability in the presence of two-wayness, when the stack is visibly. This syntactic restriction enforces that any transition which increments at least one dimension is triggered only a bounded number of times per input position. We show that non-emptiness of two-way visibly pushdown Parikh automata which are single-use is NExpTime-ccomplete. We finally give applications to decision problems for expressive transducer models from nested words to words, including the equivalence problem.
08/02/2018, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU), Luminy<

’‘Two-Way Two-Tape Automata’‘
by Léo Exibard (LIS and ULB)

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.
25/01/2018, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Dynamics and Coalitions in Sequential Games’‘
by Marion Hallet (Université de Mons)

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.
18/01/2018, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Synchronism versus asynchronism in monotonic Boolean automata networks’‘
by Sylvain Sené (LIS)
08/11/2017, 14h00 at 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’‘
by El Makki Voundy (LIF)

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.
07/12/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘On string-to-outer-context transducers and their sequentialization’‘
by Didier Villevalois (LIF)

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.
14/09/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Est-ce que je peux écrire dans votre liste ?’‘
by Denis Lugiez (LIF)

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…
06/07/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘A decidable logic for finite word transductions’‘
by Emmanuel Filiot (Université libre de Bruxelles)

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).
29/06/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Copyfull Streaming String Transducers’‘
by Pierre-Alain Reynier (LIF)

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.
22/06/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Towards the verification of file tree transformations - the Colis project’‘
by Ralf Treinen (IRIF, Université Paris Diderot)

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.
15/06/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘A logical approach to locality in pictures languages’‘
by Frédéric Olive (LIF)

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.
18/05/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Positivité d’automates de Büchi non-ambigus’‘
by Théodore Lopez (ENS Paris-Saclay & LIF)

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é.
04/05/2017, 14h at Salle CH301 du Département Informatique et Interactions, Campus St Charles

’‘On static malware detection’‘
by Tayssir Touili (LIPN, Université Paris 13)

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.
30/03/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Metric Interval Temporal Logic Revisited’‘
by Benjamin Monmege (LIF)

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 Bü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.
23/03/2017, 10h30 at 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’‘
by Aznam Yacoub (LSIS)

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.
16/03/2017, 10h30 at 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)’‘
by Didier Villevalois (LIF)

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.
02/03/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Algebras of relations: from algorithms to formal proofs’‘
by Paul Brunet (University College London)

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.
02/02/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Regular transductions with origin semantics’‘
by Bruno Guillon (Université de Varsovie)

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.
26/01/2017, 10h30 at Salle de réunion du bâtiment modulaire (en bas de la BU)

’‘Optimal Reachability in Divergent Weighted Timed Games’‘
by Damien Busatto-Gaston (LIF)

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.
05/01/2017, 10h30 at 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’‘
by Ocan Sankur (IRISA, CNRS)

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.
15/12/2016, 10h30 at Salle BU3A

’‘Minimal probabilistic automata have to make irrational choices’‘
by Mahsa Shirmohammadi (University of Oxford)

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 nm matrix M into a product of a nonnegative nd 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.
24/11/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Degree of sequentiality of weighted automata’‘
by Didier Villevalois (LIF)

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.
03/11/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Théorie des AFL’‘
by El Makki Voundy (LIF)

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^n b^n, n ≥ 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é.
06/10/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Séries reconnaissables de graphes et minimisation approximée d’automates pondérés’‘
by Guillaume Rabusseau (LIF)

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.
29/09/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Analyzing Timed Systems Using Tree Automata’‘
by Paul Gastin (LSV, ENS Paris-Saclay)

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.
27/09/2016, 10h00 at Salle de réunion du 6ème étage du LIF

’‘SMT-based Enforcement and Analysis of NATO Content-based Protection and Release Policies’‘
by Silvio Ranise (Bruno Kessler Foundation, Trento)

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.
27/09/2016, 11h00 at Salle de réunion du 6ème étage du LIF

’‘Access control and obligations in the category-based metamodel’‘
by Maribel Fernandez (King’s College London)

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.
22/09/2016, 10h30 at 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’‘
by Worachet Uttha (LIF)

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.
07/07/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Formal methods for the verification of distributed algorithms’‘
by Aiswarya Cyriac (Chennai Mathematical Institue)

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.
09/06/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Inference of (min,+) Automata’‘
by Madhur Gupta (stagiaire LIF, Thapar University)

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).
02/06/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Rational verification in Iterated Electric Boolean Games’‘
by Youssouf Oualhadj (LACL)

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
26/05/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘A Methodology to Build Run-Time Monitors for Enforcing Authorization Policies in Business Processes’‘
by Clara Bertolissi (LIF)

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.
28/04/2016, 10h30 at Campus St Charles, salle CH 301

’‘Approches logiques en sémantique des langages concurrents’‘
by Emmanuel Beffara (I2M)

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.
21/04/2016, 10h30 at Campus St Jérôme, Salle Gérard Jaumes du rez de chaussée du Bâtiment Polytech

’‘Measure Quantifier in Monadic Second Order Logic’‘
by Matteo Mio (LIP, ENS Lyon)

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.
14/04/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Admissible Strategies in Quantitative Games’‘
by Ocan Sankur (IRISA, CNRS)

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.
07/04/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Autour de l’algorithme de multiplication de D.V et G.V Chudnovsky’‘
by Nicolas Baudru (LIF)

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.
10/03/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘A Generalised Twinning Property for Minimisation of Cost Register Automata’‘
by Laure Daviaud (LIP, ENS Lyon)

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.
03/03/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Two-Way Visibly Pushdown Automata and Transducers’‘
by Jean-Marc Talbot (LIF)

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.
25/02/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Coût de lecture pour les automates et la synthèse’‘
by Denis Kuperberg (TUM Munich)

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.
11/02/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Homomorphic characterizations of indexed languages and more…’‘
by Séverine Fratani (LIF)

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.
04/02/2016, 11h at Bâtiment TPR2, 1er étage, amphithéâtre Herbrand

’‘Logics for Weighted Automata and Transducers’‘
by Benjamin Monmege (LIF)

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.
21/01/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Automata’‘
by Denis Lugiez (LIF)

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).
14/01/2016, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Rewriting Higher-order Stack Trees’‘
by Vincent Penelle (LIGM)

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.
10/12/2015, 10h30 at Salle 105H, 1er étage du bâtiment TPR1

’‘Fixed-point elimination in the Intuitionisitic Propositional Calculus’‘
by Luigi Santocanale (LIF)

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
26/11/2015, 14h at Salle de réunion du 6ème étage du LIF

’‘Interval Iteration Algorithm for MDPs and IMDPs’‘
by Benjamin Monmege (LIF)

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. Joint work with Serge Haddad (LSV)
12/11/2015, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Equivalence of deterministic top-down tree-to-string transducers is decidable’‘
by Sebastian Maneth (University of Edinburgh)

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.
05/11/2015, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Decision Problems of Tree Transducers with Origin’‘
by Pierre-Alain Reynier (LIF)

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
22/10/2015, 10h30 at 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é’‘
by Didier Villevalois (LIF)

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.
01/10/2015, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Transformations régulières de mots: extension aux data words’‘
by Antoine Durand-Gasselin (LIF)

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.
24/09/2015, 10h30 at Salle de réunion du 6ème étage du LIF

’‘Introduction à la théorie profinie des langages réguliers’‘
by Laure Daviaud (LIF)

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*.
17/09/2015, 10h30 at Salle de réunion du 6ème étage du LIF

’‘To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games’‘
by Benjamin Monmege (LIF)

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).