Exposés 2021-2022
- Marie Fortin (University of Liverpool)
- Jeudi 9 décembre, 10h30
- Luminy TPR2 4.05
- How undecidable are HyperLTL and HyperCTL*?
- Antonio Casares (LaBRI, Université de Bordeaux)
- Jeudi 2 décembre, 10h30
- Luminy TPR2 4.05
- On a correspondence between memory structures for Muller games and Rabin automata
- Filip Mazowiecki (University of Warsaw)
- Jeudi 25 novembre, 10h30
- Luminy TPR2 4.05
- The boundedness and zero isolation problems for weighted automata over nonnegative rationals
- Pierre Ohlmann (IRIF, Université de Paris)
- Jeudi 4 novembre, 10h30
- Luminy TPR2 4.05
- Positionalité pour un joueur dans les jeux à durée infinie
- Denis Lugiez (LIS)
- Jeudi 23 septembre, 10h30
- Luminy TPR2 4.05
- Décidabilité de l'accessibilité dans les réseaux de Petri
Exposés 2020-2021
- Dhruv Nevatia (LIS and CMI)
- Jeudi 17 juin, 14h00
- Visio Zoom
- An Algebraic Characterisation of First-Order Logic with Neighbour
-
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.
- Saison indécidabilité/impossibilité
- Guillaume Theyssier (I2M, CNRS)
- 29 avril 2021, 10h30
- Visio
- Théorèmes de Rice dans les automates cellulaires
- Ismaël Jecker (IST Austria)
- Jeudi 1er avril 2021, 10h30
- Visio
- Prime languages
- 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.
- Saison indécidabilité/impossibilité
- Denis Lugiez (LIS)
- 11 mars 2021, 10h30
- Luminy TPR2 4.05 et visio
- Undecidability of halting of one-Clause logic program
- Saison indécidabilité/impossibilité
- Pierre Guillon (I2M, CNRS)
- 25 février 2021, 10h30
- Luminy TPR2 4.05 et visio
- Pavages : transducteurs et indécidabilité dans les systèmes affines
- Saison indécidabilité/impossibilité
- Guilhem Gamard (LIS)
- 11 février 2021, 10h30
- Visio
- Pavages : apériodicité et preuve substitutive de l'indécidabilité
- Saison indécidabilité/impossibilité
- Jérémie Chalopin (LIS)
- 21 janvier 2021, 10h30
- Luminy TPR2 4.05 et visio
- Explorabilité d'un réseau avec des jumelles et indécidabilité de la simple connexité
- Karoliina Lehtinen (LIS)
- Vendredi 22 janvier, 14h
- Luminy TPR2 4.05 et visio
- Between determinism and nondeterminism, what are good-for-games automata good for?
- 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.
- Saison indécidabilité/impossibilité
- Emmanuel Godard (LIS)
- 14 janvier 2021, 10h30
- Luminy TPR2 4.05 et visio
- Impossibilité de l'élection déterministe et probabiliste dans les anneaux anonymes
- Marie Fortin (University of Liverpool)
- Mardi 15 décembre, 10h30
- Visio
- Expressivity of first-order logic, star-free propositional dynamic logic and communicating automata
- 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ütchi-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.
- Engel Lefaucheux (Max-Planck Institute for Software Systems, Sarrebrucken)
- 8 décembre 2020
- Visio
- On the Monniaux Problem in abstract interpretation
- 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.
- Léo Exibard (LIS-ULB)
- 30 novembre 2020
- Visio
- Computability and Continuity of Data Word Functions Defined by Transducers
- 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.
- Guillaume Maurras (LIS)
- 23 novembre 2020
- Visio
- Caractérisation logique de langages d'ordre supérieur - introduction
- 1/ Büchi : la déterminisabilité des automates finis est l'élément clé de la réciproque
2/ Les langages algébriques :
i/ les automates à Pile ne sont pas déterminisables, par contre Alur introduit les NWA (déterminisables) qui permettent un argument "à la Büchi" pour montrer que les modèles de ExistMatchMSO sont exactement les langages algébriques.
ii/ conclusion : en enrichissant la structure des mots (d'un couplage) et en construisant une classe d'automates déterminisable (les NWA) on a caractériser logiquement une classe de langage (les algébriques)
3/ Les langages indexés :
on voudrait appliquer (ii) on enrichit la structure de mot de 2 couplages (se répondant l'un l'autre d'une certaine façon qu'on appelle "haricot"), on a définit des automates sur ces mots enrichis et prouvés qu'ils sont déterminisables on voudrait catégoriser logiquement la partie (?) des indexés à laquelle ils correspondent.
exemple : le langage uu où u est de longueur paire est un langage de "haricot" / un langage indexé
- Louis-Marie Dando (LIS)
- 5 novembre 2020
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Les automates circulaires sur les rationnels
- 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.
- Charles Paperman (Université de Lille)
- Mercredi 21 octobre, 14h00
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Stackless processing of streamed trees
- 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.
- Benjamin Monmege (LIS)
- Jeudi 1 octobre 2020 et jeudi 8 octobre 2020
- 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
- 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.
- Julie Parreaux (LIS)
- Jeudi 24 septembre, 10h30
- 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
- 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.
- Nathan Lhote (LIS)
- Jeudi 10 septembre, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Continuity and computability of regular functions
- 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.
Exposés 2019-2020
- Annulé pour cause de Covid-19
- Adrien Le Coënt (ENSTA Paris, U2IS)
- Lundi 23 mars, 10h30
- Salle de réunion BU1, Luminy
- Guaranteed simulation and control synthesis for switched systems
- Switched systems constitute a sub-class of hybrid systems, and the synthesis problem for such systems is still an important issue, particularly when considering safety critical systems.
Control synthesis for switched systems has been extensively studied in the past years. One of the current major approaches is symbolic methods, which basically aim at representing the continuous and infinite state-space of the system with a finite number of symbols, e.g. discrete points, sets of states, etc. This type of approaches is particularly adapted for safety critical systems, since it exhaustively ensures that an interest set is safe. However, their computational complexity is usually exponential with the dimension of the system and the fineness of the discretisation.
We present some recent results and ongoing work allowing to overcome some of the flaws of the current symbolic methods, relying on guaranteed numerical schemes, abstraction methods and compositional approaches.
- Annulé pour cause de Covid-19
- Matthieu Rosenfeld (LIS)
- Jeudi 19 mars, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Calculer le taux de croissance dans les arbres des ensembles définissables en logique monadique du second ordre
- Un résultat récent de Rote montre que le nombre d'ensembles dominants minimaux dans les arbres d'ordre \(n\) est au plus \(95^{\frac{n}{13}}\) et que cette borne est optimale. En généralisant les idées qu'il a utilisé on peut montrer qu'on peut calculer algorithmiquement de telles bornes pour tout type d'ensemble définissable en logique monadique du second ordre. En toute généralité, l'algorithme qu'on obtient nous permet d'approximer par le haut la borne optimale. La question de savoir si on peut aussi l'approximer par le bas et donc si ce nombre est calculable reste ouverte. Cependant, en pratique, dans un certain nombre de cas intéressants on arrive a obtenir la valeur exacte (exprimée sous forme de racine d'un polynôme).
La méthode utilisée consiste à calculer "le taux de croissance" du langage d'un automate d'arbre. Je commencerai dans mon exposé par m’intéresser à la même question, mais en remplaçant "arbres d'ordre n" par "chemin d'ordre n" pour illustrer certaines idées. Je m'attaquerai ensuite aux difficultés supplémentaires liés aux arbres avant de mentionner plusieurs généralisations.
- Annulé pour cause de Covid-19
- Vadim Malvone (Université d'Évry)
- Lundi 16 mars, 10h30
- Salle de réunion BU1, Luminy
- Raisonnement stratégique en théorie des jeux
- La théorie des jeux en intelligence artificielle est un puissant cadre mathématique largement appliqué au cours des trois dernières décennies pour le raisonnement stratégique dans les systèmes multi-agents. Les travaux fondateurs sur cette ligne de recherche ont commencé avec des jeux à deux joueurs au tour par tour (sous des informations parfaites et imparfaites) pour vérifier l'exactitude d'un système par rapport à un environnement imprévisible. Ensuite, de gros efforts ont été consacrés à étendre ces travaux au cadre multi-agents et, en particulier, au raisonnement efficace sur les concepts de solution importants tels que l'équilibre de Nash et similaires. Des contributions révolutionnaires dans ce sens concernent l'introduction des logiques pour le raisonnement stratégique telles que la logique temporelle à temps alterné (ATL), la logique stratégique (SL) et leurs extensions. Les jeux à deux joueurs et les logiques pour le raisonnement stratégique sont aujourd'hui des domaines de recherche très actifs. Dans cet exposé, nous présenterons nos contributions dans ces deux axes de recherche.
- Célia Borlido (Université de Coimbra)
- Jeudi 5 mars, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Stone Duality and the Substitution Principle
- 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.
- Saison indécidabilité/impossibilité
- Damien Imbs (LIS)
- Jeudi 20 février, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Impossibilité de l'accord k-ensembliste
- Mathias Ramparison (Université de Luxembourg)
- Jeudi 13 février, 10h30
- 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
- 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).
- Séminaire Pôle Calcul
- Jérôme Leroux (CNRS, LaBRI)
- Jeudi 30 janvier, après-midi
- St Charles
- Saison indécidabilité/impossibilité
- Théodore Lopez et Pierre-Alain Reynier (LIS)
- Jeudi 23 janvier, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Problèmes indécidables sur les transducteurs
- Maria Emilia Descotte (LaBRI, Université de Bordeaux)
- Jeudi 16 janvier, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Synchronized word relations
- 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 A*xA* 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.
- Engel Lefaucheux (Max-Planck Institute for Software Systems, Sarrebrucken)
- Jeudi 28 novembre, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Opacity of a Stochastic System : Maximisation versus Minimisation
- 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.
- Saison indécidabilité/impossibilité
- Denis Lugiez (LIS)
- Jeudi 21 novembre, 14h00
- Saint Charles, Bâtiment 5, Salle 18
- Undecidability of strong bisimulation of BPP with states
- Nathan Lhote (University of Warsaw)
- Jeudi 14 novembre, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Some recent results on polyregular functions
- 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.
- Denis Kuperberg (CNRS, LIP, ENS Lyon)
- Jeudi 7 novembre, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Circular proof systems for regular expressions
- 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
- Karoliina Lehtinen (University of Liverpool)
- Jeudi 24 octobre, 11h
- Amphithéâtre Herbrand (I2M, TPR2, 1er étage), Luminy
- Quasi-polynomial techniques for parity games and and other problems
- 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.
- Benjamin Monmege (LIS)
- Jeudi 3 octobre, 10h30
- 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
- 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.
- Théodore Lopez (LIS)
- Jeudi 19 septembre, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de l'ancienne BU), Luminy
- Determinisation of Finitely-Ambiguous Copyless Cost Register Automata
- 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.
Exposés 2018-2019
- Glenn Merlet (I2M, AMU)
- Jeudi 20 juin, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- Séparer des mots avec des automates à poids
- 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 \(\mathbb 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.
- Bruno Guillon (CRIStAL, Université de Lille)
- Jeudi 7 février, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- Finding paths in large graphs
- 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.
- Samir Ouchani (CESI eXia)
- Jeudi 24 janvier, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- Specifying, Modeling, and Gauging Security in inter-disciplinary Systems
- 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.
- Pierre-Alain Reynier (LIS)
- Jeudi 25 octobre, 10h30
- 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
- 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.
- Denis Lugiez (LIS)
- Jeudi 13 septembre, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- Gröbner bases are easy
- 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...
Exposés 2017-2018
- Nicola Zannone (Eindhoven University of Technology)
- Jeudi 12 juillet, 10h30
- 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
- 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.
- Benjamin Monmege (LIS)
- Jeudi 28 juin, 10h00
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- Groupe de travail : Algebraic methods to decide automata
- Marie van den Bogaard (Université libre de Bruxelles)
- Jeudi 14 juin, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- Beyond admissibility: Dominance betweens chains of strategies
- 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.
- Patricia Bouyer-Decitre (LSV, ENS Paris-Saclay, CNRS)
- Jeudi 31 mai, 10h30
- 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
- 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.
- Benjamin Monmege (LIS)
- Vendredi 18 mai, 14h00
- 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
- 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.
- James Worrell (University of Oxford)
- Jeudi 17 mai, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- Polynomial Invariants for Affine Programs
- 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.
- Mahsa Shirmohammadi (LIS)
- Jeudi 3 mai, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- Costs and Rewards in Priced Timed Automata
- We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an ε-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert’s 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.
- Nicolas Baudru (LIS)
- Jeudi 19 avril, 11h00
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- From Two-Way Transducers to Regular Functions Expressions
- Transducers constitute a fundamental extension of automata. The class of regular word functions has recently emerged as an important class of word-to-word functions, characterized by means of (functional, or unambiguous, or deterministic) two-way transducers, copyless streaming string transducers, and MSO-definable graph transformations. One of the most important result in language theory is Kleene theorem, relating finite state automata and regular expressions. R. Alur, A. Freilich and M. Raghothaman have introduced (CSL-LICS '14) a set of regular function expressions and proved a similar result for regular word functions, by showing the equivalence with copyless streaming string transducers. In this paper, we propose a direct, simplified and effective translation from unambiguous two-way transducers to regular function expressions. In addition, our approach allows us to derive a subset of regular function expressions characterizing the (strict) subclass of functional sweeping transducers.
- Jean-Marc Talbot (LIS)
- Jeudi 12 avril, 10h30
- Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy
- Two-Way Parikh Automata with a Visibly Pushdown Stack
- 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.
- Léo Exibard (LIS & ULB)
- Jeudi 8 février, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU), Luminy
- Two-Way Two-Tape Automata
- In this article we consider two-way two-tape (alternating) automata accepting pairs of words and we study some closure properties of this model. Our main result is that such alternating automata are not closed under complementation for non-unary alphabets. This improves a similar result of Kari and Moore for picture languages. We also show that these deterministic, non-deterministic and alternating automata are not closed under composition.
- Marion Hallet (Université de Mons)
- Jeudi 25 janvier, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Dynamics and Coalitions in Sequential Games
- We consider n-player non-zero sum games played on finite trees (i.e., sequential games), in which the players have the right to repeatedly update their respective strategies, for instance, to improve the outcome wrt to the current strategy profile. This generates different type of dynamics in the game which may eventually stabilise, for example to Nash Equilibrium.
- El Makki Voundy (LIF)
- Mercredi 8 novembre, 14h00
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Langages \(\epsilon\)-sûrs et caractérisations des langages d’ordres supérieurs
- Une ligne de recherche présente dans la littérature depuis les années soixante est celle des "théorèmes de représentation". Son résultat fondateur est le théorème de Chomsky-Schützenberger qui stipule qu'un langage est algébrique si et seulement si il est l'image par homomorphisme de l'intersection entre un langage régulier et le langage de Dyck. Ce résultat a connu depuis diverses généralisations à différentes familles de langages.
Dans cette thèse, nous proposons plusieurs généralisations de ce résultat aux langages d'ordres supérieurs. Ceux-ci sont des langages reconnaissables par des automates à piles itérées. Nous définissons une notion de langages de Dyck d'ordres supérieurs, nous introduisons et étudions des classes de transductions que nous qualifions d'\(\epsilon\)-sûres et nous montrons qu'un langage appartient à un niveau k+l de la hiérarchie des langages d'ordres supérieurs si et seulement si il est l'image d'un langage de Dyck de niveau k par une transduction \(\epsilon\)-sûre de niveau l. Ce résultat contribue à la description des traces d'exécutions des calculs des machines capables de reconnaître les langages d'ordres supérieurs et apporte un outil théorique visant à permettre de généraliser des résultats valant pour un niveau quelconque de la hiérarchie vers un autre. Nous illustrons ce dernier point en généralisant une caractérisation logique des langages algébriques aux langages indexés.
- Didier Villevalois (LIF)
- Jeudi 7 décembre, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- On string-to-outer-context transducers and their sequentialization
- Model synthesis from specifications often produce large and impractical models. A natural problem is then to simplify those models, and especially make them deterministic. In the context of transducers, i.e., automata with output, a machine that is deterministic in the way it reads its input is said to be sequential.
In this work, we are interested in non-deterministic streaming string transducers, a model of transducers with write-only registers introduced by Alur. We investigate a particular subclass of this model that uses only 1 *concatenation-free* register, i.e., whose updates are of the form X=uXv, for some words u,v. We present how this can be viewed as a string-to-string finite state transducer whose transitions have output labels that are contexts. At each move, the output context of the chosen transition is put around the already produced output word. We call those machines string-to-outer-context transducers.
This context-based presentation enables us to exhibit an elegant contextual twinning property, in the line of Choffrut's twinning property to decide sequentializability of string-to-string finite state transducers. We show that, given a string-to-outer-context transducer, it is equivalent i) whether it satisfies the contextual twinning property, ii) whether there exists an equivalent sequential string-to-outer-context transducer, and iii) whether the induced string-to-string function satisfies a Lipschitz property (for an appropriate notion of distance).
This is a work in progress and not all the details are set in stone yet. We will thus discuss what is done and what remains to be done.
- Denis Lugiez (LIF)
- Jeudi 14 septembre, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Est-ce que je peux écrire dans votre liste ?
- La logique de séparation est utilisée dans la preuve de programme pour exprimer des propriétés de la mémoire (le tas) et plusieurs outils ont été réalisés pour cette logique. La logique de base a été enrichie pour pouvoir prendre en compte des structures comme les listes ou les droits de lecture/écriture donnés à un thread. Plusieurs modèles ont été utilisés pour décrire ces droits (modèles de fraction, modèle de token, modèles des arbres de partage binaires...). Dans ce travail nous donnons une procédure permettant de tester la satisfaisabilité et l'implication de formules d'une logique de séparation avec listes paramétrée par le modèle de permission. Contrairement à ce qui se passe dans le cas des listes sans permissions, le problème de satisfaisabilité est NP-dur et l'implication est co-NP-dur. Nous donnons une procédure non-déterministe pour l'implication paramétrée par le modèle de permission permettant de prouver que le problème de l'implication est co-NP complet (modulo un oracle sur le modèle de permission). Cette procédure utilise une procédure qui résoud le problème sans liste mais avec permission qui est optimale dans un certain type de modèles de permissions. L'outil sur lequel repose la procédure est le SL-graphe qui est une représentation symbolique d'une formule permettant de ramener le problème à une question d'isomorphisme entre graphes. Pour finir, nous donnons des résultats de complexité optimaux dans les modèles de permissions pour les problèmes de satisfaisabilité et d'implication dans le modèle fractionnaire et une classe de modèles générique (modèles booléens).
Travail réalisé avec Stéphane Demri et Etienne Lozes (LSV, ENS Paris-Saclay).
PS: pour ceux qui doutent de l’intérêt pratique de cette logique, le bug "dirty cow" du noyau linux -qui a notamment servi à escroquer un hébergeur coréenne via un rançongiciel au mois de juin- repose sur le fait qu'un thread qui ne devrait avoir qu'un droit de lecture gagne un droit d'écriture suite à une race condition...
Exposés 2016-2017
- Emmanuel Filiot (Université libre de Bruxelles)
- Jeudi 6 juillet, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- A decidable logic for finite word transductions
- A finite word transduction is a binary relation of finite words. After a brief introduction on recent results about word transductions, in particular about logics, algebra and automata for word transductions, the talk introduces a new logic to specify properties of word transductions, and presents some of its expressiveness and algorithmic properties. In particular, the model-checking and synthesis problems for the expressive class of MSO-definable (functional) transductions, against/from properties specified in this logic, are considered. A connection with a logic for finite words over infinite alphabets (data words) will be shown as well.
This work is joint with Luc Dartois (ULB) and Nathan Lhote (ULB / UBordeaux).
- Pierre-Alain Reynier (LIF)
- Jeudi 29 juin, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Copyfull Streaming String Transducers
- Copyless streaming string transducers (copyless SST) have been introduced by R. Alur and P. Cerny in 2010 as a one-way deterministic automata model to define transductions of finite strings. Copyless SST extend deterministic finite state automata with a set of variables in which to store intermediate output strings, and those variables can be combined and updated all along the run, in a linear manner, i.e., no variable content can be copied on transitions. It is known that copyless SST capture exactly the class of MSO-definable string-to-string transductions, and are as expressive as deterministic two-way transducers. They enjoy good algorithmic properties. Most notably, they have decidable equivalence problem (in PSpace).
On the other hand, HDT0L systems have been introduced for a while, the most prominent result being the decidability of the equivalence problem. In this paper, we propose a semantics of HDT0L systems in terms of transductions, and use it to study the class of copyfull SST. Our contributions are as follows: (i) HDT0L systems and total copyfull SST are equi-expressive, (ii) the equivalence problem for copyfull SST and the equivalence problem for HDT0L systems are inter-reducible, in linear time. As a consequence, SST equivalence is decidable, (iii) the functionality of non-deterministic copyfull SST is decidable, (iv) determining whether a copyfull SST can be transformed into an equivalent copyless SST is decidable in polynomial time.
Joint work with Emmanuel Filiot.
- Ralf Treinen (IRIF, Université Paris Diderot)
- Jeudi 22 juin, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Towards the verification of file tree transformations - the Colis project
- This talk describes the ongoing ANR project Colis, which has the goal of developing techniques and tools for the formal verification of shell scripts. More specifically, our goal is to verify the transformation of a file system tree described by so-called Debian maintainer scripts. These scripts, often written in the Posix shell language, are part of the software packages in the Debian GNU/Linux distribution.
A possible example of a program specification is absence of execution error under certain initial conditions. Automatic program verification even for this kind of specification is a challenging task. In case of Debian maintainer scripts we are faced with even more challenging properties like idempotency of scripts (required by policy), or commutation of scripts.
The project is still in its early stage, so there are only some preliminary results at the moment. However, I will explain why I think that the case of Debian maintainer scripts is very interesting for program verification : some aspects of scripts (POSIX shell, manipulation of a complex data structure) make the problem very difficult, while other aspects of the Debian case are likely to make the problem easier than the task of verifying any arbitrary shell script.
- Frédéric Olive (LIF)
- Jeudi 15 juin, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- A logical approach to locality in pictures languages
- This paper deals with descriptive complexity of picture languages of any dimension by fragments of existential second-order logic: 1) We generalize to any dimension the characterization by Giammarresi et al. (1996) of the class of recognizable picture languages in existential monadic second-order logic. 2) We state natural logical characterizations of the class of picture languages of any dimension d≥1 recognized in linear time on nondeterministic cellular automata, a robust complexity class that contains, for d=1, all the natural NP-complete problems. Our characterizations are essentially deduced from normalization results for first-order and existential second-order logics over pictures.
Joint work with Etienne Grandjean
- Théodore Lopez (ENS Paris-Saclay & LIF)
- Jeudi 18 mai, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Positivité d'automates de Büchi non-ambigus
- Dans le cadre du model-checking, on s'intéresse au calcul de la probabilité que, pour une entrée infinie fournie par une chaîne de Markov, un automate de Büchi accepte sur celle-ci. Dans ce calcul, il est d'abord nécessaire de décider si l'automate a une probabilité non nulle d'accepter. Cette propriété est indépendante de la chaîne de Markov, on parle de positivité de l'automate. On fournira deux méthodes, une calculatoire et une constructive, décidant de la positivité.
- Tayssir Touili (LIPN, Université Paris 13)
- Jeudi 4 mai, 14h
- Salle CH301 du Département Informatique et Interactions, Campus St Charles
- On static malware detection
- The number of malware is growing extraordinarily fast. A malware may bring serious damage, e.g., the worm MyDoom slowed down global internet access by ten percent in 2004. Thus, it is crucial to have efficient up-to-date virus detectors. Existing antivirus systems use various detection techniques to identify viruses such as (1) code emulation where the virus is executed in a virtual environment to get detected; or (2) signature detection, where a signature is a pattern of program code that characterizes the virus. A file is declared as a virus if it contains a sequence of binary code instructions that matches one of the known signatures. These techniques are becoming insufficient. Indeed, emulation based techniques can only check the program's behavior in a limited time interval. As for signature based systems, it is very easy to virus developers to get around them. Thus, a robust malware detection technique needs to check the behavior (not the syntax) of the program without executing it. We show in this talk how using behavior signatures allow to efficiently detect malwares in a completely static way. We implemented our techniques in a tool, and we applied it to detect several viruses. Our results are encouraging. In particular, our tool was able to detect more than 800 viruses. Several of these viruses could not be detected by well-known anti-viruses such as Avira, Avast, Norton, Kaspersky and McAfee.
- Benjamin Monmege (LIF)
- Jeudi 30 mars, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Metric Interval Temporal Logic Revisited
- This talk will present two recent works on MITL logic.
The first, published at FORMATS'16, studies the reactive synthesis problem (RS) for specifications given in MITL. RS is known to be undecidable in a very general setting, but on infinite words only; and only the very restrictive BResRS subcase is known to be decidable (see D'Souza et al. and Bouyer et al.). We precise the decidability border of MITL synthesis. We show RS is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit BResRS and introduce an efficient on-the-fly algorithm to solve it. Based on a joint work with Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts, Hsi-Ming Ho and Nathalie Sznajder.
The second one deals with the tool support for MITL verification that is still lacking to this day. Therefore, we propose a new construction from MITL to timed automata via very-weak one-clock alternating timed automata. Our construction subsumes the well-known construction from LTL to 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.
- Aznam Yacoub (LSIS)
- Jeudi 23 mars, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Une approche de vérification formelle et de simulation pour les systèmes à événements discrets : Application à PROMELA
- Depuis quelques années, les nouvelles avancées technologiques ont permis la mise au point de systèmes physiques et logiciels qui aident considérablement l'Homme dans ses tâches, que ce soit dans la vie quotidienne ou dans des processus industriels. Aux allures simples, ces panneaux publicitaires, ces chaînes de fabrication automatisées ou même ces pilotes automatiques sont devenus, au fil du temps, de plus en plus complexes à comprendre et à maîtriser, entraînant en permanence de nouveaux lots de problématiques et de questions. Du fait qu'ils impliquent davantage d'interactions qu'auparavant, avec de plus en plus de composants qui communiquent entre eux, ces systèmes demandent encore plus de vigilances à leurs concepteurs qui doivent s'assurer que ces systèmes ne génèrent pas de comportements inadaptés ou imprévus. Ce constat, que nous faisons pour les systèmes et les processus que nous développons, est identique au constat réalisé dès lors que nous souhaitons modéliser et simuler un phénomène physique complexe, tel qu'un évènement météorologique ou le fonctionnement du cerveau humain, qui impliquent aussi des interactions compliquées entre des dizaines, des centaines voire des milliers d'entités différentes. Mais si les avancées ont été énormes dans les champs technologiques et scientifiques en général, les domaines de la Vérification et de la Validation ont également connu un bond significatif avec la mise au point de nouveaux concepts et de nouvelles méthodes, automatiques ou non, pour répondre à ce besoin de fiabilité. Parmi elles, se dégagent notamment deux grandes familles : celle de la Vérification Formelle et celle de la Simulation. Longtemps considérées comme à l'opposée l'une de l'autre, les recherches récentes essaient de rapprocher ces deux grandes familles de méthodologies. C'est dans ce cadre que les travaux de cette thèse proposent une nouvelle approche pour intégrer la Simulation dites à Evènements Discrets aux Méthodes Formelles. L'objectif d'une telle approche est alors d'améliorer les méthodes formelles existantes, en les combinant à la simulation, afin de leur permettre de détecter de potentielles erreurs qu'elles ne pouvaient déceler avant, notamment sur des systèmes temporisés. Cette approche nous a conduit à la mise au point d'un nouveau langage formel, le DEv-PROMELA. Ce nouveau langage, créé à partir du PROMELA et du formalisme DEVS, est à mi-chemin entre un langage de spécifications formelles vérifiables et un formalisme de simulation. En combinant alors un model-checking traditionnel et une simulation à évènements discrets sur le modèle exprimé dans ce nouveau langage, il est alors possible de détecter et de comprendre des dysfonctionnements qu'un model-checking seul ou qu'une simulation seule n'auraient pas permis de trouver. Ce résultat est notamment illustré à travers les différents exemples étudiés dans ces travaux.
- Didier Villevalois (LIF)
- Jeudi 16 mars, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Présentation d'article : Monadic Second-Order Logic on Finite Sequences (by Loris D'Antoni and Margus Veanes)
- We extend the weak monadic second-order logic of one successor for finite strings (M2L-STR) to symbolic alphabets by allowing character predicates to range over decidable quantifier free theories instead of finite alphabets. We call this logic, which is able to describe sequences over complex and potentially infinite domains, symbolic M2L-STR (S-M2L-STR). We present a decision procedure for S-M2L-STR based on a reduction to symbolic finite automata, a decidable extension of finite automata that allows transitions to carry predicates and can therefore model complex alphabets. The reduction constructs a symbolic automaton over an alphabet consisting of pairs of symbols where the first element of each pair is a symbol in the original formula’s alphabet, while the second element is a bit-vector. To handle this modified alphabet we show that the Cartesian product of two decidable Boolean algebras, e.g., the product of formula’s algebra and bit-vector’s algebra, also forms a decidable Boolean algebra. To make the decision procedure practical, we propose two efficient representations of the Cartesian product of two Boolean algebras, one based on algebraic decision diagrams and one on a variant of Shannon expansions. Finally, we implement our decision procedure and evaluate it on more than 10,000 formulas. Despite the generality, our implementation has comparable performance with the state-of-the-art M2L-STR solvers.
- Paul Brunet (University College London)
- Jeudi 2 mars, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Algebras of relations: from algorithms to formal proofs
- Algebras of relations appear naturally in many contexts, in computer science as well as in mathematics. They constitute a framework well suited to the semantics of imperative programs. Kleene algebras are a starting point: these algebras enjoy very strong decidability properties, and a complete axiomatisation. The goal of this thesis was to export known results from Kleene algebra to some of its extensions.
We first considered a known extension: Kleene algebras with converse. Decidability of these algebras was already known, but the algorithm witnessing this result was too complicated to be practical. We proposed a simpler algorithm, which is more efficient, and whose correctness is easier to establish. It allowed us to prove that this problem lies in the complexity class PSpace-complete.
Then we studied Kleene allegories. Few results were known about this extension. Following results about closely related algebras, we established the equivalence between equality in Kleene allegories and the equality of certain sets of graphs. We then developed a new automaton model (so-called Petri automata), based on Petri nets. We proved the equivalence between the original problem and comparing these automata. In the restricted setting of identity-free Kleene lattices, we also provided an algorithm performing this comparison. This algorithm uses exponential space. However, we proved that the problem of comparing Petri automata lies in the class ExpSpace- complete.
Finally, we studied Nominal Kleene algebras. We realised that existing descriptions of these algebra were not suited to relational semantics of programming languages. We thus modified them accordingly, and doing so uncovered several natural variations of this model. We then studied formally the bridges one could build between these variations, and between the existing model and our new version of it. This study was conducted using the proof assistant Coq.
- Bruno Guillon (Université de Varsovie)
- Jeudi 2 février, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Regular transductions with origin semantics
- This talk is about regular transductions, which are string-to-string functions realised by one of the following equivalent deterministic formalisms: MSO transduction, two-way transducer and streaming string transducer. We may observe that each of these formalisms provides more than just a function from words to words. Indeed, one can also reconstruct origin information, which says how positions of the output string originate from positions of the input string. It is also possible to provide any string-to-string function with an origin semantic, indicating an origin input position for each output position, in a similar way. This defines a general object, that extends functions and which we call origin graph. The main result of the talk is a characterisation of the families of origin graphs which correspond to a regular transduction with origin information.
This is joint work with Mikołaj Bojańczyk, Laure Daviaud and Vincent Penelle.
- Damien Busatto-Gaston (LIF)
- Jeudi 26 janvier, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- Optimal Reachability in Divergent Weighted Timed Games
- Weighted timed games are played by two players on a timed automaton equipped with weights: one player wants to minimise the accumulated weight while reaching a target, while the other has an opposite objective. Used in a reactive synthesis perspective, this quantitative extension of timed games allows one to measure the quality of controllers. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. Decidability results exist for subclasses of one-clock games, and for a subclass with non-negative weights defined by a semantical restriction on the weights of cycles. In this work, we introduce the class of divergent weighted timed games as a generalisation of this semantical restriction to arbitrary weights. We show how to compute their optimal value, yielding the first decidable class of weighted timed games with negative weights and an arbitrary number of clocks. In addition, we prove that divergence can be decided in polynomial space. Last, we prove that for untimed games, this restriction yields a class of games decidable in non-deterministic logarithmic space, and for which the value can be computed in polynomial time.
Joint work with Benjamin Monmege and Pierre-Alain Reynier
- Ocan Sankur (IRISA, CNRS)
- Jeudi 5 janvier, 10h30
- Salle de réunion du bâtiment modulaire (en bas de la BU)
- A Practical Abstraction Technique for Parameterized Model Checking of Leader Election Protocols
- We consider distributed timed systems that implement leader election protocols which are at the heart of clock synchronization protocols. We develop abstraction techniques for parameterized model checking of such protocols under arbitrary network topologies, where, moreover, nodes have independently evolving clocks. We apply our technique for model checking the root election part of the flooding time synchronisation protocol (FTSP), and obtain improved results compared to previous work. We model check the protocol for all topologies in which the distance to the node to be elected leader is bounded by a given parameter. Our results prove the correctness of the protocol on networks including for 2D grids of hundreds of nodes, and 3D of thousands of nodes.
- Mahsa Shirmohammadi (University of Oxford)
- Jeudi 15 décembre, 10h30
- Salle BU3A
- Minimal probabilistic automata have to make irrational choices
- In this talk, we answer the question of whether, given a probabilistic automaton (PA) with rational transition probabilities, there always exists a minimal equivalent PA that also has rational transition probabilities. The PA and its minimal equivalent PA accept all finite words with equal probabilities. We approach this problem by exhibiting a connection with a longstanding open question concerning nonnegative matrix factorization (NMF). NMF is the problem of decomposing a given nonnegative n×m matrix M into a product of a nonnegative n×d matrix W and a nonnegative d×m matrix H. In 1993 Cohen and Rothblum posed the problem of whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries. As a corollary we obtain a negative answer to the question on rationality of minimal probabilistic automata.
This talk is based on two papers in ICALP 2016 and SODA 2017.
Séminaire LIF de James Worrell (University of Oxford) : consultez toutes les informations
- Didier Villevalois (LIF)
- Jeudi 24 novembre, 10h30
- Salle de réunion du 6ème étage du LIF
- Degree of sequentiality of weighted automata
- Weighted automata (WA) are an important formalism to describe quantitative properties. Obtaining equivalent deterministic machines is a longstanding research problem. In this paper we consider WA with a set semantics, meaning that the semantics is given by the set of weights of accepting runs. We focus on multi-sequential WA that are defined as finite unions of sequential WA. The problem we address is to minimize the size of this union. We call this minimum the degree of sequentiality of (the relation realized by) the WA. For a given positive integer k, we provide multiple characterizations of relations realized by a union of k sequential WA over an infinitary finitely generated group: a Lipschitz-like machine independent property, a pattern on the automaton (a new twinning property), and a subclass of cost register automata. When possible, we effectively translate a WA into an equivalent union of k sequential WA. We also provide a decision procedure for our twinning property for commutative computable groups thus allowing to compute the degree of sequentiality. Last, we show that these results also hold for word transducers and that the associated decision problem is Pspace-complete.
Joint work with Laure Daviaud, Ismael Jecker, and Pierre-Alain Reynier
- El Makki Voundy (LIF)
- Jeudi 3 novembre, 10h30
- Salle de réunion du 6ème étage du LIF
- Théorie des AFL
- Un cône rationnel est une famille de langages close par intersection avec des langages réguliers, homomorphismes et homomorphismes inverses ; un full-AFL (Abstract Family of Languages) est un cône rationnel clos par union, concatenation et étoile de Kleene. Ces notions ont été introduites par Greibach et Ginsburg sous l'observation que les familles de la hiérarchie de Chomsky (du moins, telle qu’elle était dans les années 60) sont généralement closes par ces opérations et avec pour motivation d'apporter une approche générique à l'étude de ces familles. La "théorie des AFL" consiste à étudier l'incidence de ces propriétés de clôture sur les propriétés globales des familles qui en sont closes. Il est par exemple possible d'établir que tout cône rationnel généré à partir d'un langage est clos par union ; ou que le problème de la régularité d'un langage est indécidable pour tout cône rationnel clos par union et qui contient le langage \(\{a^nb^n, n \geq 0\}\). Dans cet éxposé, je vous présenterai quelques résultats de cette dite théorie des AFL. Nous observerons la dépendance entre differentes opérations de clôture, de quelle façon la présence d'un langage dans une famille puisse lui garantir des propriétés de clôture et comment correler clôture et indécidabilité.
- Guillaume Rabusseau (LIF)
- Jeudi 6 octobre, 10h30
- Salle de réunion du 6ème étage du LIF
- Séries reconnaissables de graphes et minimisation approximée d'automates pondérés
- Pendant cet exposé, je présenterai deux travaux réalisés pendant ma thèse au sein de l'équipe Qarma. Ces deux travaux ont été initialement motivés par des problématiques d'apprentissage automatique et concernent les automates pondérés. Après avoir rappelé les méthodes d'apprentissage spectral pour les automates pondérés, je présenterai ces deux contributions :
- Séries reconnaissables de graphes. Nous proposons une extension des modèles de séries reconnaissables de chaînes et d'arbres aux graphes. Nous montrons tout d'abord que les modèles d'automates pondérés de chaînes et d'arbres peuvent être interprétés d'une manière simple et unifiée à l'aide de réseaux de tenseurs, et que cette interprétation s'étend naturellement aux graphes. Nous étudions ensuite certaines propriétés fondamentales de ce modèle (clôture par somme et produit, reconnaissabilité des séries à support fini) avant de présenter des résultats préliminaires sur leur apprentissage.
- Minimisation approximée d'automates pondérés. Nous considérons le problème suivant : étant donné un automate pondéré à n états, comment trouver un automate à m (inférieur à n) états calculant une fonction proche de l'originale. Cette problématique a été considérée dans des travaux récents (Balle et al., LICS 2015) pour le cas d'automates pondérés sur les mots. Dans ces travaux, les auteurs introduisent une forme canonique pour les automates pondérés pour laquelle les états d'un automate sont clairement ordonnés et découplés, ce qui leur permet de proposer une approche théoriquement fondée à cette problématique. Nous présenterons l'extension de ces travaux aux automates pondérés d'arbres.
- Paul Gastin (LSV, ENS Paris-Saclay)
- Jeudi 29 septembre, 10h30
- Salle de réunion du 6ème étage du LIF
- Analyzing Timed Systems Using Tree Automata
- Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. Such graphs can be interpreted in trees opening the way to tree automata based techniques which are more powerful than analysis based on word automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).
This is a joint work with S. Akshay and Shankara Narayanan Krishna.
- Silvio Ranise (Bruno Kessler Foundation, Trento)
- Mardi 27 septembre, 10h00
- Salle de réunion du 6ème étage du LIF
- SMT-based Enforcement and Analysis of NATO Content-based Protection and Release Policies
- NATO is developing a new IT infrastructure that will enable automated information sharing between different information security domains and provide strong separation between different communities of interest while supporting dynamic and flexible enforcement of the need-to-know principle. In this context, the Content-based Protection and Release (CPR) model has been introduced to support the specification and enforcement of access control policies used in NATO and, more generally, in complex organizations. While the ability to support fine-grained security policies for a large variety of users, resources and devices is desirable, the definition, maintenance, and enforcement of these policies can be difficult, time-consuming, and error-prone. Thus, automated support for policy analysis to help designers in these activities is needed. In this talk we show that several policy-related analysis problems of practical interest can be reduced to SMT problems, we propose an effective enforcement mechanism relying on attribute-based encryption (ABE), and assess the scalability of our approach on an extensive set of synthetic benchmarks.
- Maribel Fernandez (King's College London)
- Mardi 27 septembre, 11h00
- Salle de réunion du 6ème étage du LIF
- Access control and obligations in the category-based metamodel
- We define an extension of the category-based access control (CBAC) metamodel to accommodate a general notion of obligation. Since most of the well-known access control models are instances of the CBAC metamodel, we obtain a framework for the study of the interaction between authorisation and obligation, such that properties may be proven of the metamodel that apply to all instances of it. In particular, the extended CBAC metamodel allows security administrators to check whether a policy combining authorisations and obligations is consistent.
- Worachet Uttha (LIF)
- Jeudi 22 septembre, 10h30
- Salle de réunion du 6ème étage du LIF
- Étude des politiques de sécurité pour les applications distribuées : le problème des dépendances transitives
- Le contrôle d'accès est un ingrédient fondamental de la sécurité des systèmes d'information. Depuis les années 70, les travaux dans ce domaine ont apporté des solutions aux problèmes de confidentialités des données personnelles avec applications à différents environnements (systèmes d'exploitation, bases de données, etc.). Parmi les modèles de contrôle d'accès, nous intéressons au modèle basé sur les organisations (OrBAC) et nous en proposons une extension adapté aux contextes distribués tels que les services web. Ce modèle étendu est capable en particulier de gérer les demandes d'accès transitives. Ce cas peut se produire lorsqu'un service doit appeler un autre service qui peut avoir besoin d'invoquer à son tour un ou plusieurs services afin de satisfaire la demande initiale.
Nous appelons D-OrBAC (Distributed Organisation Based Access Control), l'extension du modèle OrBAC avec une notion de procuration représentée par un graphe de délégation. Ce graphe nous permet de représenter des accords entre les différentes organisations impliquées dans la chaîne d'invocations de services, et de garder la trace des autorisations transitives. Nous proposons également une technique d'analyse basée sur Datalog qui nous permet de simuler des scénarios d'exécution et de vérifier l'existence de situations non sécurisées.
Nous utilisons ensuite des techniques de réécriture afin d'assurer que la politique de sécurité spécifiée via notre modèle D-OrBAC respecte des propriétés importantes telles que la terminaison et la consistance. Finalement, nous implémentations pour un cas d'étude, le mécanisme d'évaluation des demandes d'accès selon la norme XACML sur la plateforme WSO2 Identity Server, afin de montrer que notre solution est capable de fournir à la fois la fonctionnalité désirée et la sécurité nécessaire pour le système.
Exposés 2015-2016
- Aiswarya Cyriac (Chennai Mathematical Institue)
- Jeudi 7 juillet, 10h30
- Salle de réunion du 6ème étage du LIF
- Formal methods for the verification of distributed algorithms
- We propose automata-theoretic approach for the verification of distributed algorithms in which processes can store, send and compare process-identifiers (pids). Examples include leader election algorithms and distributed sorting algorithms. We introduce a logic to specify correctness of such distributed algorithms. This logic is inspired by data logics, and can reason about processes and pids. The model checking problem is undecidable in general; we will see some ideas to regain decidability for distributed algorithms over ring topologies.
Based on joint work with Benedikt Bollig and Paul Gastin.
- Madhur Gupta (stagiaire LIF, Thapar University)
- Jeudi 9 juin, 10h30
- Salle de réunion du 6ème étage du LIF
- Inference of (min,+) Automata
- We develop a method to infer min-plus automata from sample behaviors. Min-plus automata recently attracted a lot of interest as a model of online algorithms. Unlike existing approaches to the inference of automata in a quantitative setting, our procedure works in an active fashion: an automaton is gradually refined on the basis of multiplicity and equivalence queries. Moreover, it is not restricted to deterministic devices but applies to residual automata: a large class of non-deterministic automata that is strictly more expressive and exponentially more succinct. I will show the method, after recalling the standard L* Angluin’s algorithm, to infer deterministic finite-state automata.
Joint work with Benedikt Bollig (LSV, ENS Cachan, CNRS), Peter Habermehl (IRIF, Université Paris Diderot, CNRS), and Benjamin Monmege (LIF, AMU, CNRS)
- Youssouf Oualhadj (LACL)
- Jeudi 2 juin, 10h30
- Salle de réunion du 6ème étage du LIF
- Rational verification in Iterated Electric Boolean Games
- Electric boolean games are compact representations of games where the players have qualitative objectives described by LTL formulae and have limited resources. We study the complexity of several decision problems related to the analysis of rationality in electric boolean games with LTL objectives. In particular, we report that the problem of deciding whether a profile is a Nash equilibrium in an iterated electric boolean game is no harder than in iterated boolean games without resource bounds. We show that it is a PSPACE-complete problem. As a corollary, we obtain that both rational elimination and rational construction of Nash equilibria by a supervising authority are PSPACE-complete problems.
Joint work with Nicolas Troquard
- Clara Bertolissi (LIF)
- Jeudi 26 mai, 10h30
- Salle de réunion du 6ème étage du LIF
- A Methodology to Build Run-Time Monitors for Enforcing Authorization Policies in Business Processes
- We are interested in security-aware workflow management systems, which are at the heart of modern e-services and need to mediate access to their resources by imposing authorisation constraints (e.g., separation of duty). We introduce a class of symbolic transition systems capable of representing collections of security-aware workflows and we study the verification of reachability properties of such systems. We use our technique to build efficient run-time monitors capable of ensuring the successful termination of workflows subject to authorisation constraints.
- Emmanuel Beffara (I2M)
- Jeudi 28 avril, 10h30
- Campus St Charles, salle CH 301 (près du département Informatique et Interactions, à droite de l'amphi de Chimie au 3ème étage)
- Approches logiques en sémantique des langages concurrents
- Dans la modélisation des systèmes concurrents, un problème central est celui de la compositionnalité, ou comment déduire des propriétés d'un système complet à partir de l'analyse de ses composants de façon indépendante: c'est ce qui permet de “passer à l'échelle” et de concevoir des systèmes sûrs de façon modulaire. Dans le monde des langages de programmation, c'est le typage qui sert à composer correctement les programmes. Dans cet exposé, je raconterai des idées récentes sur ce que la théorie de la démonstration peut apporter à la question de la modélisation et du typage des processus concurrents, notamment en présence de mobilité, c'est-à-dire quand la topologie des canaux de communication évolue avec l'exécution.
- Matteo Mio (LIP, ENS Lyon)
- Jeudi 21 avril, 10h30
- Campus St Jérôme, Salle Gérard Jaumes du rez de chaussée du Bâtiment Polytech, map
- Measure Quantifier in Monadic Second Order Logic
- In this talk I will present some recent work, with H. Michalewski, on the study of an extension of MSO on infinite trees with the so-called "measure quantifier". This kind of research is motivated, as I will discuss, by a long-standing open problem in the field of verification of probabilistic programs. I will state a negative (i.e., undecidability) result but also present some interesting (currently) open problems.
- Ocan Sankur (IRISA, CNRS)
- Jeudi 14 avril, 10h30
- Salle de réunion du 6ème étage du LIF
- Admissible Strategies in Quantitative Games
- The notion of admissible strategies has been proposed in game theory to formalize rationality of players. It has been studied recently for games of infinite duration with Boolean objectives. In this talk, we give explain this notion, and give motivations on its interest for controller synthesis. We extend admissible strategies to games of infinite duration with quantitative objectives. First, we show that, under the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the notion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide verification and synthesis problems related to the notion of admissible strategy.
Joint with Romain Brenguier, Guillermo Perez, Jean-Francois Raskin.
- Nicolas Baudru (LIF)
- Jeudi 7 avril, 10h30
- Salle de réunion du 6ème étage du LIF
- Autour de l'algorithme de multiplication de D.V et G.V Chudnovsky
- Savoir multiplier deux éléments d'un corps fini est un problème important qui est au coeur des protocoles cryptographiques. En effet le chiffrement et le déchiffrement de ces protocoles reposent sur l'efficacité de la multiplication, qui a donc un impact direct sur la sécurité. Les algorithmes issus de l'approche de D.V. et G.V. Chudnovsky permettent de réaliser efficacement la multiplication de deux éléments de \(GF_{q^n}\) avec \(q\) une puissance d'un nombre premier. Efficace signifie ici avec une complexité bilinéaire linéaire en \(n\). Ces algorithmes utilisent des espaces de Riemann-Roch construits à partir de corps de fonctions algébriques. J'introduirai ces notions et présenterai la méthode des frères Chudnovsky.
- Laure Daviaud (LIP, ENS Lyon)
- Jeudi 10 mars, 10h30
- Salle de réunion du 6ème étage du LIF
- A Generalised Twinning Property for Minimisation of Cost Register Automata
- Weighted automata extend finite-state automata by associating with transitions weights from a semiring S, defining functions from words to S. Recently, cost register automata have been introduced as an alternative model to describe any function realised by a weighted automaton by means of a deterministic machine. Unambiguous weighted automata over a group G can equivalently be described by cost register automata whose registers take their values in G, and are updated by operations of the form x:=y.c, with c in G, and x,y registers. This class is denoted by CRA(G). In this talk, I will introduce a twinning property and a bounded variation property parametrised by an integer k, such that the corresponding notions introduced originally by Choffrut for finite-state transducers are obtained for k=1. Our main result links these notions with the register complexity of CRA(G). More precisely, we prove that given an unambiguous weighted automaton W over an infinitary group G realizing some function f, the three following properties are equivalent: i) W satisfies the twinning property of order k, ii) f satisfies the k-bounded variation property, iii) f can be described by a CRA(G) with at most k registers. Actually, this result is proved in a more general setting, considering machines over the semiring of finite sets of elements from G and is extended to prove a similar result for finite-valued finite-state transducers. Finally, the effectiveness of the constructions leads to decidability/complexity results about the register complexity (i.e. what is the minimal number of registers needed to compute a given function) of cost register automata.
This is a joint work with Pierre-Alain Reynier and Jean-Marc Talbot.
- Jean-Marc Talbot (LIF)
- Jeudi 3 mars, 10h30
- Salle de réunion du 6ème étage du LIF
- Two-Way Visibly Pushdown Automata and Transducers
- Automata-logic connections are pillars of the theory of regular languages. Such connections are harder to obtain for transducers, but a well-known result proved for word-to-word transformations shows that deterministic two-way transducers and monadic second-order (MSO) transducers are equivalent. Nested words are words with a nesting structure, allowing to model unranked trees as their depth-first-search linearisations. In this presentation, we consider transformations from nested words to words, allowing in particular to produce unranked trees if output words have a nesting structure. The model of visibly pushdown transducers allows to describe such transformations, and we propose a simple deterministic extension of this model with two-way moves that has the following properties: i) it is a simple computational model, that naturally has a good evaluation complexity; ii) it is expressive: it subsumes nested word-to-word MSO transducers, and the exact expressiveness of MSO transducers is recovered using a simple syntactic restriction; iii) it has good algorithmic/closure properties: the model is closed under composition with a unambiguous one-way letter-to-letter transducer which gives closure under regular look-around, and has a decidable equivalence problem.
- Denis Kuperberg (TUM Munich)
- Jeudi 25 février, 10h30
- Salle de réunion du 6ème étage du LIF
- Coût de lecture pour les automates et la synthèse
- Je présenterai une nouvelle mesure de complexité pour automates et transducteurs, appelée coût de lecture, qui mesure quelle quantité d'information est lue en moyenne à chaque instant dans un environnement aléatoire. Il est ensuite naturel de chercher à minimiser ce coût de lecture parmi les automates reconnaissant un langage donné, ou les transducteurs solution d'un problème de synthèse. Je présenterai les résultats obtenus en ce sens, ainsi que les problèmes ouverts encore en cours d'investigation.
Ce travail est en collaboration avec Shaull Almagor et Orna Kupferman.
- Séverine Fratani (LIF)
- Jeudi 11 février, 10h30
- Salle de réunion du 6ème étage du LIF
- Homomorphic characterizations of indexed languages and more...
- I will present joint work with El Makki Voundy in which we study a subclass of context-free transducers generating indexed languages from the Dyck language. I will also present several works in progress: context-free transducer generating some subclasses of indexed languages, and logical characterization of context-free transducers.
- Benjamin Monmege (LIF)
- Jeudi 4 février, 11h
- Bâtiment TPR2, 1er étage, amphithéâtre Herbrand
- Logics for Weighted Automata and Transducers
- This talk will present some of the recent results obtained in the community on the relationship between weighted automata and weighted logics. The story started 10 years ago with the introduction of a quantitative semantics for MSO logic over words and an equivalence theorem between weighted automata and a restricted weighted MSO logic. Since then, many extensions have been studied: from words to trees, infinite words, pictures, etc; from semirings to more general weight computations. Also, the proof techniques have matured, from low level, carefully mimicking the classical proofs in the boolean setting, to higher level, using various abstract semantics. We illustrate this evolution by introducing a core weighted logic and its abstract semantics as multisets of weight structures. The equivalence between weighted automata and core weighted logic holds at the level of the abstract semantics. We will also demonstrate the versatility of the weighted automata approach by instantiating it into the transducer setting, showing a possible lead towards the design of an alternative logic for transductions.
- Denis Lugiez (LIF)
- Jeudi 21 janvier, 10h30
- Salle de réunion du 6ème étage du LIF
- Automata
- I will present several extensions of finite state automata and how to decide some logical fragments of the first-order theory of classical data types (lists and queues).
- Vincent Penelle (LIGM)
- Jeudi 14 janvier, 10h30
- Salle de réunion du 6ème étage du LIF
- Rewriting Higher-order Stack Trees
- Higher-order pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the satisfaction of any formula written in monadic second order logic (respectively first order logic with reachability predicates) can be decided on such a graph. The purpose of this talk is to propose a common extension to both higher-order stack operations and ground tree rewriting. We introduce a model of higher-order ground tree rewriting over trees labelled by higher-order stacks (henceforth called stack trees), which syntactically coincides with ordinary ground tree rewriting at order 1 and with the dynamics of higher-order pushdown automata over unary trees. The infinite graphs generated by this class have a decidable first order logic with reachability. Formally, an order n stack tree is a tree labelled by order n-1 stacks. Operations of ground stack tree rewriting are represented by a certain class of connected DAGs labelled by a set of basic operations over stack trees describing of the relative application positions of the basic operations appearing on it. Applying a DAG to a stack tree t intuitively amounts to paste its input vertices to some leaves of t and to simplify the obtained structure, applying the basic operations labelling the edges of the DAG to the leaves they are appended to, until either a new stack tree is obtained or the process fails, in which case the application of the DAG to t at the chosen position is deemed impossible. This model is a common extension to those of higher-order stack operations presented by Carayol and of ground tree transducers presented by Dauchet and Tison. As further results we can define a notion of recognisable sets of operations through a generalisation. The proof that the graphs generated by a ground stack tree rewriting system have a decidable first order theory with reachability is inspired by the technique of finite set interpretations presented by Colcombet and Loding.
- Luigi Santocanale (LIF)
- Jeudi 10 décembre, 10h30
- Salle 105H, 1er étage du bâtiment TPR1
- Fixed-point elimination in the Intuitionisitic Propositional Calculus
- It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras—that is, the algebraic models of the Intuitionistic Propositional Calculus—always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the μ-calculus based on intuitionistic logic is trivial, every μ-formula being equivalent to a fixed-point free formula. We give in this paper an axiomatization of least and greatest fixed-points of formulas, and an algorithm to compute a fixed-point free formula equivalent to a given μ-formula. The axiomatization of the greatest fixed-point is simple. The axiomatization of the least fixed-point is more complex, in particular every monotone formula converges to its least fixed-point by Kleene’s iteration in a finite number of steps, but there is no uniform upper bound on the number of iterations. We extract, out of the algorithm, upper bounds for such n, depending on the size of the formula. For some formulas, we show that these upper bounds are polynomial and optimal.
Joint work with Silvio Ghilardi, Milan, and Maria Gouveia, Lisbon
- Benjamin Monmege (LIF)
- Jeudi 26 novembre, 14h
- Salle de réunion du 6ème étage du LIF
- Interval Iteration Algorithm for MDPs and IMDPs
- Markov Decision Processes (MDP) are a widely used model including both non-deterministic and probabilistic choices. Minimal and maximal probabilities to reach a target set of states, with respect to a policy resolving non-determinism, may be computed by several methods including value iteration. This algorithm, easy to implement and efficient in terms of space complexity, consists in iteratively finding the probabilities of paths of increasing length. However, it raises three issues: (1) defining a stopping criterion ensuring a bound on the approximation, (2) analysing the rate of convergence, and (3) specifying an additional procedure to obtain the exact values once a sufficient number of iterations has been performed. The first two issues are still open and for the third one a "crude" upper bound on the number of iterations has been proposed. Based on a graph analysis and transformation of MDPs, we address these problems. First we introduce an interval iteration algorithm, for which the stopping criterion is straightforward. Then we exhibit convergence rate. Finally we significantly improve the bound on the number of iterations required to get the exact values. We extend our approach to also deal with Interval Markov Decision Processes (IMDP) that can be seen as symbolic representations of MDPs.
Joint work with Serge Haddad (LSV)
- Sebastian Maneth (University of Edinburgh)
- Jeudi 12 novembre, 10h30
- Salle de réunion du 6ème étage du LIF
- Equivalence of deterministic top-down tree-to-string transducers is decidable
- We solve a long standing open problem in formal language theory. For some subclasses we present efficient algorithms: polynomial time for total transducers with unary output alphabet (over a given top-down regular domain language), and co-randomized polynomial time for linear transducers; these results are obtained using techniques from multi-linear algebra. For our main result, we prove that equivalence can be certified by means of inductive invariants using polynomial ideals. This allows us to construct two semi-algorithms, one searching for a proof of equivalence, one for a witness of non-equivalence.
- Pierre-Alain Reynier (LIF)
- Jeudi 5 novembre, 10h30
- Salle de réunion du 6ème étage du LIF
- Decision Problems of Tree Transducers with Origin
- A tree transducer with origin translates an input tree into a pair of output tree and origin info. The origin info maps each node in the output tree to the unique input node that created it. In this way, the implementation of the transducer becomes part of its semantics. We show that the landscape of decidable properties changes drastically when origin info is added. For instance, equivalence of nondeterministic top-down and MSO transducers with origin is decidable. Both problems are undecidable without origin. The equivalence of deterministic top-down tree-to-string transducers is decidable with origin, while without origin it is a long standing open problem. With origin, we can decide if a deterministic macro tree transducer can be realized by a deterministic top-down tree transducer; without origin this is an open problem.
Joint work with Emmanuel Filiot, Sebastian Maneth and Jean-Marc Talbot
- Didier Villevalois (LIF)
- Jeudi 22 octobre, 10h30
- Salle de réunion du 6ème étage du LIF
- Utilisation de la sur-réduction pour le calcul du différentiel entre deux politiques de sécurité
- Un aspect important des politiques de sécurité pour les systèmes d'information concerne le contrôle des droits d'accès aux ressources par leurs utilisateurs. Les politiques de contrôle d'accès peuvent être spécifiées formellement sous la forme de systèmes de réécriture. Cette représentation permet la vérification statique de certaines propriétés des politiques (consistance, complétude, terminaison, ...). Elle offre aussi un moyen opérationnel éprouvé pour résoudre et contrôler les requêtes d'accès, que l'on exprime alors sous la forme d'un terme clos.
Nous présentons la sur-réduction, une généralisation de la réécriture, et plus particulièrement la sur-réduction nécessaire la plus extérieure, une variante qui s'applique sur la classe des systèmes de réécriture inductivement séquentiels. Nous montrons comment elle peut être utilisée dans le cadre des politiques de sécurité pour résoudre des patrons de requêtes d'accès, cette fois exprimés sous la forme de termes avec variables.
Finalement, nous nous intéressons aux différences entre deux versions d'une même politique de contrôle d'accès. Nous formulons pour cela un problème nouveau, l'identification d'exemples pour lesquels deux systèmes de réécriture présentent un comportement différent. Pour répondre à ce problème, nous proposons une technique basée à la fois sur la transformation des systèmes de réécriture et sur la sur-réduction. Nous discutons de son applicabilité dans des contextes où l'un des deux (ou les deux) systèmes peut ne pas être terminant.
- Antoine Durand-Gasselin (LIF)
- Jeudi 1er octobre, 10h30
- Salle de réunion du 6ème étage du LIF
- Transformations régulières de mots: extension aux data words
- La théorie des langages réguliers permet une analyse qualitative de propriétés sur les mots. Cette théorie a de nombreuses approches (logique avec mso, calculatoire avec les automates déterministes, algébrique, et descriptive avec les expressions regulières). Plutôt que d'étendre cette théorie des languages réguliers aux fonctions de coût pour une analyse qualitative, nous nous plaçons dans le cadre plus général des transformations de mots. Je vous présenterai une classe de transformations régulières de mots qui admet une caractérisation logique avec MSO, ainsi que deux caractérisations computationnelle, la première au moyen des transducteurs déterministes two-way, et la seconde grâce aux streaming string transducers, et vous présenterai une extension aux data words, qui conserve cette triple caractérisation.
- Laure Daviaud (LIF)
- Jeudi 24 septembre, 10h30
- Salle de réunion du 6ème étage du LIF
- Introduction à la théorie profinie des langages réguliers
- Cette présentation a pour vocation d'introduire les concepts de base de la théorie profinie des langages réguliers : - l'ensemble des mots profinis (complétion de A* pour une certaine distance que j'introduirai), - la notion d'équations profinies pour les treillis/algèbres booléennes (éventuellement clos par quotient) de langages réguliers, - la notion de variétés de langages et de monoïdes, le théorème d'Eilenberg et le théorème de Reiterman concernant les identités profinies. Je m'appuierai sur les exemples classiques : variétés des langages star-free, les langages piecewise-testable, et sur un travail en commun avec C. Paperman concernant les équations caractérisant des classes de langages générées par les langages de la forme u*.
- Benjamin Monmege (LIF)
- Jeudi 17 septembre, 10h30
- Salle de réunion du 6ème étage du LIF
- To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games
- Quantitative games are two-player zero-sum games played on directed weighted graphs. Total-payoff games—that can be seen as a refinement of the well-studied mean-payoff games—are the variant where the payoff of a play is computed as the sum of the weights. Our aim is to describe the first pseudo-polynomial time algorithm for total-payoff games in the presence of arbitrary weights. It consists of a non-trivial application of the value iteration paradigm. Indeed, it requires to study, as a milestone, a refinement of these games, called min-cost reachability games, where we add a reachability objective to one of the players. For these games, we give an efficient value iteration algorithm to compute the values and optimal strategies (when they exist), that runs in pseudo-polynomial time. We also propose heuristics to speed up the computations.
Joint work with Thomas Brihaye (UMONS), Gilles Geeraerts (ULB), and Axel Haddad (UMONS).