Liste des événements uniques du groupe Graphes et Logique


2013-11-26Systèmes de réécriture (de mots) à une règle préservant les longueurs et transductions rationnelles
11:00-12:00
salle 076
L'exposé présentera quelques avancées concernant la question suivante : étant donné un système de réécriture S à une règle u -> v où les mots u et v sont distincts et de même longueur, comment décider si la transformation, qui à tout mot w fait correspondre l'ensemble S(w) des mots qu'on peut obtenir à partir de w en itérant l'application de la règle u -> v, définit une transduction rationnelle?

L'un des exemples négatifs parmi les plus simples est clairement le système S = {ab -> ba}. En revanche, le système S = {abb -> baa} définit, lui, une transduction rationnelle.

Dans cet exposé, on répond partiellement à une conjecture (maintenant ancienne!) portant sur une caractérisation simple des systèmes S = { u -> v } définissant une transduction rationnelle. On y présentera aussi les questions ouvertes que ces travaux ont engendrées dont une caractéristique commune est la simplicité de leur énoncé!
 Plus d'infos  


2013-10-01Computational complexity of commutative grammars
11:00-12:00
salle 076
There are some natural languages that allow the free ordering of words or phrases in their sentences while preserving grammaticality. In order to model such sentences, we consider a term algebra with two operators: one that models the usual concatenation, and another that denotes the "free order combination", that is the concatenation of its arguments in any possible left-to-right order.

Multiple Context-Free Grammars (MCFG) are an extension of context-free grammars, where non-terminals in a derivation are associated with a tuple of strings (rather than a single string). Each production rule then specifies how the strings on the right-hand side are combined to form the strings of the left-hand side.

We consider an extension of MCFG that, instead of strings, produces terms (or contexts) over the previously described algebra, to represent sentences with free order. We describe several natural subclasses of those so-called commutative grammars, and give an account of the computational complexity associated with their (universal) parsing problems.

This is joint work with Sylvain Salvati.
 Plus d'infos  


2013-07-02Specification of Quantitative Properties: Logics, Automata, Expressions
11:00-12:00
Salle 076
Automatic verification has nowadays become a central domain of investigation in computer science. Over 25 years, a rich theory has been developed leading to numerous tools, both in academics and industry, allowing the verification of Boolean properties - those that can be either true or false. Current needs evolve to a finer analysis, a more quantitative one. Extension of verification techniques to quantitative domains has begun 15 years ago with probabilistic systems. However, many other quantitative properties are of interest, such as the lifespan of an equipment, energy consumption of an application, the reliability of a program, or the number of results matching a database query. Expressing these properties requires new specification languages, as well as algorithms checking these properties over a given structure.

We study several formalisms, equipped with weights, able to specify such properties: denotational ones – like regular expressions, first-order logic, or temporal logics – or more operational ones, like navigating automata, possibly extended with pebbles. We study the compared expressiveness of these formalisms. In particular, we give efficient translations from denotational formalisms to the operational one. These objects, and the associated results, are presented in a unified framework of graph structures permitting to handle finite words, ranked trees, nested words, pictures or messsage sequence charts, as special cases. Therefore, possible applications are the verification of quantitative properties of traces of programs (possibly recursive, or concurrent), querying of XML documents (modelling databases for example), or natural language processing. We also present results about algorithmic questions that naturally arise in this context, like evaluation and satisfiability.
 Plus d'infos  


2013-06-11Multi-dimensional trees and a Chomsky-Schützenberger-Weir representation theorem for simple context-free tree grammars
11:00-12:00
salle 076


Weir (1987) showed that every tree-adjoining language can be expressed as a homomorphic image of the intersection of three sets: a regular set R, the Dyck language D_{2n} over the alphabet consisting of 2n pairs of brackets [_1, ]_1,..., [_{2n}, ]_{2n}, and g^{-1}(D_{2n}), where g is the bijection that maps [_{2i+1} to itself and cyclically permutes ]_{2i+1}, [_{2i+2}, ]_{2i+2}, for each i = 0, ..., n-1.

I generalize this theorem to simple context-free tree grammars: If L is the yield image of the language of a simple context-free tree grammar of rank m-1, then L can be expressed as a homomorphic image of the intersection of a regular set R, the Dyck language D_{mn} over the alphabet of mn pairs of brackets, and g^{-1}(D_{mn}), where g is the bijection that maps [_{mi+1} to itself and cyclically permutes ]_{mi+1}, [_{mi+2}, ]_{mi+2}, ..., [_{mi+m}, ]_{mi+m}, for i = 0, ..., n-1.

I obtain this result via a natural generalization of the Chomsky-Schützenberger theorem to the tree languages of simple context-free tree grammars. This intermediate result is stated in terms of "Dyck tree languages". In order to emphasize the analogy between the string case and the tree case, I use the notion of "multi-dimensional tree" introduced by Rogers (2003). An element of a Dyck tree language is regarded as a two-dimensional encoding of a three-dimensional tree, just like an element of an ordinary Dyck language encodes an ordinary, two-dimensional tree. A simple context-free tree language is defined to be the yield image of a local set of three-dimensional trees, where the "yield" is obtained from two-dimensional encoding by erasing the "brackets". I show that many necessary lemmas can be stated as general facts about m-dimensional trees.
 Plus d'infos  


2013-06-04Böhm trees as higher-order recursion schemes
11:00-12:00
Salle 076
Higher-order recursive schemes (HORS) are schematic representations of functional programs. They generate possibly infinite ranked labelled trees and, viewed as tree generators, are equivalent to λY-terms of ground type in which free variables can only have types of the form o → ... → o (with o as a special case). In this talk, I will show that any λY-term (with no restrictions on term type or the types of free variables) has an equivalent presentation as a HORS. That is, for any λY-term, there exists a HORS generating a tree that faithfully represents the Böhm tree of the λY-term. In particular, the HORS encodes higher-order binding information contained in the Böhm tree. The result reduces the problem of Böhm tree equivalence for the λY-calculus to the equivalence problem for HORS and enables MSO model-checking of Böhm trees. We also show how to adapt the methodology to finitary PCF (over finite datatypes). This is joint work with Andrzej Murawski.
 Plus d'infos  


2013-05-28Towards a characterisation of linear-time first-order existential queries
11:00-12:00
Salle 076
(or three complexity dichotomy theorems for existential first-order)

It is known that the data complexity of a Conjunctive Query (CQ) is determined only by the way its variables are shared between atoms, reflected by its hypergraph. In particular, Yannakakis [Yan81, BFMY83] proved that a CQ is decidable in linear time when it is alpha- acyclic, i.e. its hypergraph is alpha-acyclic; Bagan et al. [BDG07] even state: "Any CQ is decidable in linear time iff it is alpha-acyclic (under certain hypotheses)". They also prove a similar result for the enumeration problem.

Since the complexity of a Negative Conjunctive Query (NCQ), a conjunctive query where all atoms are negated, also only depends on its hypergraph, there must be a similar dichotomy in this case. We show that: "Any NCQ is decidable in linear time iff it is beta-acyclic (under certain hypotheses)" and also give a similar result for the enumeration problem.

If we consider Signed Conjunctive Query (SCQ), a conjunctive query where *some* atoms are negated, we need to introduce a notion of acyclicity of bicolored hypergraphs, that generalizes both alpha and beta acyclicities. With this notion, we finally generalize both previous dichotomy theorems in a single one, that deals with both the decision and the enumeration problems. This dichotomy theorem implies that beta-acyclic existential first-order queries are decidable in linear time, and that this hypergraph criterion is optimal.
 Plus d'infos  


2013-04-30LALBLC: a program testing the equivalence of dpda's
11:00-12:00
Salle 076
We present a preliminar version of the program "LALBLC" (i.e. LA=LB? Let us Compute).

The equivalence problem for dpda consists in deciding, for two given deterministic pushdown automata A,B, whether they recognize the same language. It was proved in [TCS 2001, G.S.] that this problem is decidable by means of some complete proof systems.

The program LALBLC gives, in some sense, life to the above completeness proof: on an input A,B, the program computes either a proof of their equivalence (w.r.t. to the system D5 of the above reference) or computes a witness of their non-equivalence (i.e. a word that belongs to the symmetric difference of the two languages).

We shall outline the main mathematical objects that are manipulated as well as the main functions performed over these objects. We shall also describe some experimental results obtained so far.

The talk is based on an ongoing, joint, work with P. Henry.
 Plus d'infos  


2013-03-26Algebras, automata and logic for languages of labeled birooted trees
11:00-12:00
Salle 076
We study languages of labeled finite birooted trees: Munn’s birooted trees extended with vertex labeling.

We define a notion of finite state birooted tree automata that is shown to capture the class of languages that are upward closed w.r.t. the natural order and definable in Monadic Second Order Logic. Then, relying on the inverse monoid structure of labeled birooted trees, we derive a notion of recognizable languages by means of (adequate) premorphisms into finite (adequately) ordered monoids. This notion is shown to capture finite boolean combinations of languages as above.

As a particular case, a simple encoding of finite (mono-rooted) labeled trees in an antichain of labeled birooted trees shows that classical regular languages of finite (mono-rooted) trees are also recognized by such premorphisms and finite ordered monoids.
 Plus d'infos  


2013-03-19A Formal Analysis in Coq of a Handshake Randomised Distributed Algorithm
11:00-12:00
Salle 178
Under some hypothesis on the distributed system, there is no deterministic solution of certain classical problems, as the handshake problem. Randomised solutions are then needed to solve those problems. We present a formalisation in Coq of a distributed randomised algorithm that solves this problem. This allows us to formally prove properties of this algorithm such as termination and probabilistic results.
 Plus d'infos  


2013-03-05Deterministic regular expressions
11:00-12:00
Salle 076
Deterministic regular expressions appear in many schema languages for XML (DTDs, XML Schemas) to define the possible content of an element. We prove that one can determine in linear time whether a given expression is deterministic. We also present algorithms to decide in linear time if a given word is accepted by an expression, for large families of deterministic regular expressions. Our algorithms build datastructures on the expression's parse tree, whereas classical algorithms for those problems rely on the Glushkov automaton which may have quadratic size when the size of the alphabet is not bounded.
 Plus d'infos  


2013-02-26The expressivity of Separation Logic : a survey
11:00-12:00
Salle 76
Separation logic is a program logic à la Hoare that was introduced by Reynolds and O'Hearn at the end of the 90s.

Proving a program goes through writing valid Hoare triples {Pre} p {Post}, where Pre, Post are logical assertions and p is a program. The main novelty of separation logic with respect to Hoare logic is that the assertion language introduces two new logical connectives, the separating conjunction and the magic wand, and exploits them in some inference rules for Hoare triples. In the context of heap-manipulating programs, the assertion language can be seen as a special case of the spatial logic for graphs, where a graph property "A and separately B" means that the set of edges of the graph can be partitioned in two subsets such that the two resulting subgraphs satisfy A and B respectively. In this talk, after briefly reviewing the context of separation logic, I will compare separation logic and its fragments with weak second order and weak monadic second order logic. Separation logic will be shown to be equivalent to second order logic. It will also be shown that the magic wand subsumes the separating conjunction, in the sense that there is a logspace elimination procedure for separating conjunction (joint work with Remi Brochenin and Stephane Demri).

I will also report about a result due to Dawar and Antonopoulos that states that Separation logic without magic wand is strictly less expressive than monadic second order logic.
 Plus d'infos  


2013-02-19From Two-Way to One-Way Finite State Transducers
11:00-12:00
Salle 076
Any two-way finite state automaton is equivalent to some one-way finite state automaton. This well-known result, shown by Rabin and Scott and independently by Shepherdson, states that two-way finite state automata (even non-deterministic) characterize the class of regular languages. It is also known that this result does not extend to finite string transductions: (deterministic) two-way finite state transducers strictly extend the expressive power of (functional) one-way transducers. In particular deterministic two-way transducers capture exactly the class of MSO-transductions of finite strings.

In this talk, I will address the following definability problem: given a function defined by a two-way finite state transducer, is it definable by a one-way finite state transducer? By extending Rabin and Scott's proof to transductions, we show that this problem is decidable. Our procedure builds a one-way transducer, which is equivalent to the two-way transducer, whenever one exists. This is a joint work with Emmanuel Filiot, Olivier Gauwin and Pierre-Alain Reynier.
 Plus d'infos  


2013-01-15Trace equivalence of protocols for an unbounded number of sessions
11:00-12:00
Salle 076
Secure design of communication protocols in order to ensure the authen- tication of electronic agents or the safety of secret data is known to be difficult and fairly error-prone. Symbolic frameworks such as the Dolev-Yao model and later various process algebra have proven themselves valuable for finding attacks and assessing the security of these protocols. Several tools have thus been developed to answer the need of automated verification: ProVerif, AVISPA and Scyther rely on various formal methods to prove that a range of security properties holds in protocols.

The problem of deciding reachability for cryptographic protocols has been thoroughly studied for an unbounded number of sessions and proven to be undecidable in general. Nevertheless some fragments were shown to be decidable, either by tagging or by restricting the number of blind-copies. On the other hand, trace equivalence has only been proven to be decidable for a bounded number of sessions. The objective of this talk is to provide the first results of decidability of trace equivalence for an unbounded number of sessions.

Trace equivalence for a first class of protocols was shown undecidable under scarce restrictions one variable and symmetric encryption are indeed enough. Consequently, we restrained our class of protocols a step further by making the protocols deterministic in some sense and preventing it from disclosing secret keys. This tighter class of protocols was then shown to be decidable after reduction to an equivalence between deterministic pushdown automata.
 Plus d'infos  


2012-11-20Nouvelles notions de rang et indépendance pour graphes finis
11:00-12:00
Salle 076
L'année dernière, Izakhian et Rhodes ont développé une théorie de représentation de matroïdes par des matrices booléennes où tous les matroïdes deviennent représentables, au contraire de ce qui se passe avec les représentations classiques sur des corps. Dans un travail de collaboration avec John Rhodes, on développe une théorie analogue pour les graphes finis, menant à de nouvelles notions de rang et d'indépendance de sommets. Ces notions admettent une caractérisation alternative purement combinatoire et sont la base de quelques résultats inespérés.
 Plus d'infos  


2012-11-13Automates avec multiplicité et epsilon-transitions
11:00-12:00
salle 76
Les epsilon-transitions apparaissent naturellement dans les automates lors de certains algorithmes de conversion d'expressions rationnelles, ou lorsque l'on manipule des transducteurs. La présence d'epsilon-transitions peut conduire un même mot à être accepté par un nombre infini de calculs, ce qui posent des problèmes dans le cadre des automates avec multiplicité. Nous verrons comment les définitions habituelles du comportement de tels automates peuvent être mises en défaut et comment définir la validité d'un tel automate de façon à avoir une définition stable, décidable et qui permette la suppression des epsilon-transitions quel que soit le type de multiplicité avec lequel on travaille.
 Plus d'infos  


2012-10-23La théorie des fonctions de coût régulières
11:00-12:00
salle 76
La théorie des fonctions de coûts régulières permet d'étendre quantitativement celle des langages réguliers, et présente plusieurs avantages. Premièrement, les caractérisations en termes d'automates, de monoides ou de logique (MSO,FO,LTL), s'étendent bien dans le cadre des fonctions de coût, et on peut obtenir des généralisations des théorèmes de caractérisation à la Schutzenberger, ainsi que de nouveaux théorèmes propres aux fonctions de coût. Deuxièmement, cette nouvelle théorie permet d'obtenir des résultats difficiles de décidabilité dans la théorie classique des langages réguliers, comme celui du problème de la hauteur d'étoile (qui est à l'origine du développement de cette théorie). On présentera le modèle des fonctions de coût, et on montrera comment les notions classiques sur les langages réguliers (comme celle de monoide syntactique) se généralisent à ce cadre quantitatif.
 Plus d'infos  


2012-10-16A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Infinite Words
11:00-12:00
76
We discuss the completeness of an axiomatization of Monadic Second-Order Logic (MSO) on infinite words (or streams). By using model-theoretic tools, we give an alternative proof of D. Siefkes' result that a fragment with full comprehension and induction of second-order Peano's arithmetic is complete w.r.t. the validity of MSO-formulas on streams. We rely on Feferman-Vaught Theorems and the Ehrenfeucht-Fraïssé method for Henkin models of second-order arithmetic. Our main technical contribution is an infinitary Feferman-Vaught Fusion of such models. We show it using Ramseyan factorizations similar to those for standard infinite words. We also discuss a Ramsey's theorem for MSO-definable colorings, and show that in linearly ordered Henkin models, Ramsey's theorem for additive MSO-definable colorings implies Ramsey's theorem for all MSO-definable colorings.
 Plus d'infos  


2012-10-02Walking in the free inverse monoid
11:00-12:00
Salle 076
We consider subsets of the free inverse monoid or, following Munn's representation theorem, languages of finite birooted trees.

We propose three notions of definability for these languages: definability by means of finite state walking automata with nested (invisible) pebbles, definability by means of (extension of) Kleene regular expressions, and definability by means of (adequate) premorphisms (or relational morphisms) in (adequate) finite ordered monoids.

Various correspondences, linking these three notions together, are shown to hold. Finite walking automata with a finite number of pebbles are shown to be captured by regular expressions; the number of allowed pebbles corresponds to the nesting depth of a projection operator onto languages of idempotent birooted trees.

Finite walking automata with a finite or an infinite number of pebbles are also shown to be captured by finitely generated premorphisms from the (naturally ordered) free inverse monoid in their associated (finite) transition monoids (ordered by inclusion).

These results strengthen the idea that the category of (quasi-inverse) ordered monoids and (appropriate) premorphisms is an adequate framework for the study of walking automata on trees much in the same way the category of monoids and morphisms is an adequate framework for the study of classic (one way) automata.

Moreover, since our algebraic characterization of walking automata holds even for automata using infinitely many pebbles, it also provides a presumably new algebraic framework for the study of regular languages of finite trees.

This work extend a similar work on languages of one-dimensional tiles (linear unidirectional birooted trees) recently done with Anne Dicky.
 Plus d'infos  


2012-09-18Complexity of languages of geodesics
11:00-12:00
salle 178
We address questions about recognizing geodesics in groups with simple automata, and consider both full languages of all geodesics from the identity and languages of unique normal form geodesics from the identity. We describe languages of geodesics which can be recognized by simple automata- finite state automata, pushdown automata and counter automata, and give some criteria which rule out the ability of some automata to recognize certain geodesic languages. The examples include wreath products examples and Thompson's group F, and we show that the linguistic complexity of languages of geodesics can depend upon choice of generating set. This is joint work with Jennifer Taback and Murray Elder.
 Plus d'infos  


2012-05-29Journée Méthodes Formelles
09:30-17:00
Amphi LaBRI
9h30-10h Hugo Gimbert: Jeux stochastiques à observation partielle

10h-10h30 Gabriele Puppis: Regular languages of countable words

10h30-11h Sylvain Salvati: A l'interface entre syntaxe et sémantique -
lambda-calcul, logique et grammaires formelles en action

11h30-12h Pascal Weil: The FO2 quantifier alternation hierarchy is decidable

12h-12h30 Irène Durand: Verifying monadic second order graph properties with
tree automata

14h-14h30 Mohamed Mosbah: Visidia - visualisation et preuves
d'algorithmes distribués

14h30-15h00 Frédéric Herbréteau: Better abstractions for timed
automata

15h30-16h Richard Moot: Analyse syntaxique et sémantique en théorie des types:
comment reconstituer un itinéraire à partir d'un récit de voyage
16h-16h30 David Janin: Problèmes ouverts en modélisation musicale et
applications aux méthodes formelles

16h30-17h Anca Muscholl: On distributed control and monitoring
 Plus d'infos  


2012-05-25Some operators that preserve the locality of a pseudovariety of semigroups.
11:00-12:00
salle 178
Finite semigroups are a useful algebraic tool to decide computational problems from automata theory, formal languages and logic. In this framework, the decidability of a property is quite often reduced to the decidability of (the membership in) a pseudovariety of semigroups. For example, a language of finite words can be expressed by a sentence of the first order fragment FO^2[<] if and only of its syntactic semigroup belongs to the pseudovariety DA, as shown by Thérien and Wilke.

Frequently a pseudovariety is expressed in terms of more simple decidable pseudovarieties, using operations between them, like the Mal'cev product and the semidirect product. However, these operations do not always preserve decidability. In this context, an algebraic property of pseudovarieties called "locality" is useful. For example, Thérien and Wilke showed that the pseudovariety corresponding to FO^2[<,suc] is DA*D, which is decidable since Almeida proved DA is local.

We study a family of Mal'cev operators of the form Z(m)_, showing that some of them preserve the locality of pseudovarieties. In the process, we deal with the localization operator L( ) and the semidirect product operator ( )*D, establishing some interplay between them. Among these operators we find K(m)_ and D(m)_.

As an application, we deduce that the pseudovarieties in the hierarchies R_1, R_2, R_3... and L_1, L_2, L_3... of subpseudovarieties of DA, obtained from J by alternate application of the operators K(m)_ and D(m)_, are local when m>1. These pseudovarieties are interesting, since recently Kufleitner and Weil proved the decidability of the variety of languages expressed by the fragment of sentences of FO^2[<] with at most m alternating blocks of quantifiers in its parsing tree, by showing that this variety corresponds to the intersection between R_m and L_m.

This is joint work with Ana Escada.
 Plus d'infos  


2012-04-17Bisimulations pour les opérateurs de contrôle délimité
11:00-12:00
salle 76
Nous présentons les premiers résultats sur la définition d'une théorie comportementale pour un lambda-calcul étendu avec les opérateurs de contrôle délimité shift et reset. Dans un premier temps, nous définissons une notion d'équivalence comportementale, que nous cherchons ensuite à caractériser à l'aide de bisimulations (applicative et de forme normale). Nous étudions aussi la relation entre équivalence comportementale et une autre équivalence basée sur une transformation CPS.
 Plus d'infos  


2012-04-10Largeur de décomposition d'hypergraphe
11:00-12:00
salle 76
Dans cet exposé, je vais présenter une décomposition arborescente d'hypergraphe. Cette notion est très simple et généralise notamment des notions de décomposition sur les matroïdes. On va montrer certaines propriétés de cette décomposition par rapport à divers opérations sur les hypergraphes ainsi que des exemples d'hypergraphes qui ont une petite ou une grande largeur. Par ailleurs, cette décomposition admet plusieurs restrictions intéressantes, et sur les graphes elle est équivalente à la largeur de clique. Enfin, on s'intéressera au problème de trouver en temps polynomial de bonnes décomposition pour des hypergraphes.
 Plus d'infos  


2012-03-27Schützenberger groups of primitive substitutions are decidable
11:00-12:00
salle 76
(joint work with Alfredo Costa)

It is well known that the words that appear as factors in the
iteration on the letters of a primitive endomorphism (substitution) f
of the free semigroup on a finite alphabet A is the language of blocks
of a minimal symbolic dynamical system (subshift) X_f, consisting of
biinfinite words over the alphabet A whose blocks are those factors. I
proved in 2005 that, associating to a minimal subshift X over the
alphabet A the closure J(X) of its language of blocks in the profinite
semigroup freely generated by A, one obtains a bijection between
minimal subshifts and J-maximal regular J-classes. My co-author showed
in his thesis that, viewed as an abstract group G(X), the maximal
subgroups of J(X) constitute a conjugacy invariant. I also showed
that, if f induces an automorphism of the free group on A, then G(X_f)
is a free profinite group, while there are examples for which G(X_f),
which is always finitely generated, is not a free profinite group.

Rhodes and Steinberg proved that the closed subgroups of a free
profinite semigroup are projective as profinite groups. Hence, as
observed by Lubotzky, if finitely generated, such groups admit finite
presentations, as profinite groups, in which the relations simply
state that each generator is a fixed point of a retraction of the free
profinite group. I conjectured in 2005 that, under special conditions
on the primitive substitution f, the group G(X_f) admits such a
presentation in which the retraction is obtained as a (profinite)
idempotent iterate of a positive finite continuous endomorphism f' of
the free profinite group, where f' can be effectively computed from f.
The interest in such presentations stems from the fact that the
relations can be effectively checked in a given finite group, so that
the group with such a retract presentation has decidable finite
quotients.

It turns out that the conjecture holds for every primitive
substitution f. It is therefore decidable whether a finite group is a
quotient of G(X_f). The proof of the conjecture in such a wide setting
depends on a synchronization result of Mossé for (biinfinite) fixed
points of primitive substitutions. As an application, we show that the
group associated with the classical Prouhet-Thue-Morse substitution
(a -> ab, b -> ba) is not free.
 Plus d'infos  


2012-03-20A game approach to determinize timed automata
11:00-12:00
salle 76
Timed automata are frequently used to model real-time systems. Their determinization is a key issue for several validation problems. However, not all timed automata can be determinized, and determinizability itself is undecidable. In this talk, we will present a game-based algorithm which, given a timed automaton, tries to produce a language-equivalent deterministic timed automaton, otherwise a deterministic over-approximation. Our method subsumes two recent contributions: it is at once more general than a recent determinization procedure and more precise than the existing over-approximation algorithm. Then, we will explain how this method can be adapted to be usefull for test generation. This talk is a joint work with Nathalie Bertrand, Thierry Jéron and Moez Krichen. Papers have been presented at FoSSaCs'11 and TACAS'11.
 Plus d'infos  


2012-03-13MSO+U defines languages at arbitrarily high levels of the projective hierarchy
11:00-12:00
salle 76
This work shows that for each i ∈ N there exists a ω-word language H_i definable in Monadic Second Order Logic extended with the unbounding quantifier (MSO + U) such that H_i is hard for i'th level of the projective hierarchy. Since it is not hard to see that each language expressible in MSO + U is projective, our finding solves the topological complexity of MSO + U. The result can immediately be transferred from ω-words to infinite labelled trees.

As a consequence of the topological hardness we note that no alternating automaton with a Borel acceptance condition — or even with an acceptance condition of a bounded projective complexity — can capture all of MSO + U.
 Plus d'infos  


2012-03-06Nash equilibria in concurrent games
11:00-12:00
salle 76
We consider concurrent games played on graphs, and we want to decide the existence of a Nash equilibrium (possibly with a condition on the payoffs). We propose a general transformation from multiplayer games to zero-sum game and use it to characterise the exact complexity of the Nash equilibrium problem for classical objectives.

We also extend the study to a more quantitative setting in which each player has several reachability or Büchi objectives, and a preorder on these objectives (for instance the counting order, where the aim is to maximise the number of objectives that are fulfilled).

This is joint work with Patricia Bouyer, Nicolas Markey and Michael Ummels.
 Plus d'infos  


2012-02-21Balancing weighted binary trees in linear time.
11:00-12:00
salle 76
In this talk, we consider weighted binary trees, i.e., binary trees whose leaves hold positive constants called weights. We survey different balance definitions for weighted binary trees and different algorithms to build them from a sequence of weights.

We consider the alphabetic version of the problem. In this case the leaves of the balanced alphabetic tree (read left-to-right) should be in the same order as in the original sequence. We present an incremental algorithm to build balanced alphabetic weighted trees in linear time.
 Plus d'infos  


2012-02-14Connexité dans les graphes de genre g avec obstacles: un schéma d'étiquetage.
11:00-12:00
salle 76
Nous présenterons une methode d'étiquetage compact d'un graphe G de genre g de façon à ce qu'on puisse répondre à une requête de connexité entre le sommet u et v dans G-X à partir des étiquettes de u, de v et de celles des sommets de X.
 Plus d'infos  


2012-02-07Lambda Calculus: The Differential Viewpoint
11:00-12:00
salle 76
We survey the central role of lambda calculus in theoretical computer
science, with particular interest for its connections with programming
languages, logic and category theory.
Motivated by the discovery of denotational models of Linear Logic (LL) such
as finiteness spaces, where all morphisms can be differentiated, we
introduce the differential lambda-calculus which features two ways of
applying a function to an argument: the standard one and a linear one,
implementing differentiation. This approach allows to generalize
Boudol’s resource calculus, in a framework where useful tools from
analysis, like the Taylor expansion formula, can be applied.

No prerequisites of lambda-calculus are supposed to follow the talk.
 Plus d'infos  


2012-01-31Langages de tuiles MSO définissables, monoïdes quasi-inversifs et pré-homomorphismes
11:00-12:00
salle 75
Nous présentons ici une tentative de caractérisation algébrique des langages de tuiles discrètes unidimensionnelles définissables en logique monadique du second ordre.

Ce travail est motivé par les résultats suivants. On sait que la classe des langages de tuiles définissables en MSO est particulièrement robuste. Elle est close non seulement par opération booléenne et projection, mais aussi par produit, produit itéré et résidus à droite ou a gauche (pour les tuiles positives) ou inverse (pour les tuiles quelconques). On sait aussi que cette classe est particulièrement simple. Un langage de tuile est MSO définissable si et seulement si, c'est une somme fini de produit de la forme P x R x S avec P, R et S des langages rationnels de mots.

On sait aussi que, au contraire, la classe des langages de tuiles reconnaissable par monoïde fini est particulièrement réduite. Elle correspond, en un sens, aux ensembles finis de mots bi-infinis de la forme (uv)^omega u(vu)*(vu)^omega pour u et v deux mots finis.

La question posée est donc la suivante : comment affaiblir la notion de reconnaissabilité algébrique pour obtenir tous les langages de tuiles MSO définissable ? Pour répondre à cette question, nous sommes amenés à définir les monoïdes quasi-inversifs et à étudier, sur ces monoïdes, la notion de pré-homomorphisme.

* Plus en détails:

Pour cela, nous sommes amenés à définir la notion de monoïde quasi-inversif : une sorte de monoïde presque inversif au sens où on souhaite disposer des idempotents de la forme xy pour x et y inverse l'un de l'autre, mais dans lequel on ne requiert pas la présence des inverses eux-mêmes.

Nous proposons une axiomatisation de ces monoïdes qui forment une sur-classe de la classe des monoïdes inversifs, dont nous étudions les propriétés. Nous montrons en particulier que, malgré l'absence d'inverse, on peut tout de même y définir un ordre naturel qui conserve un certain nombre des bonnes propriétés de l'ordre naturel sur les monoïdes inversifs.

Nous démontrons alors un théorème d'expansion permettant de construire, à partir de tout monoïde (fini) S, un monoïde quasi-inversif (fini) Q(S) dont S est (isomorphe à) un sous-monoïde. Fait curieux, ce résultat implique en particulier que, contrairement aux monoïdes inversifs, dans les monoïdes quasi-inversifs, il n'est pas toujours vrai que les idempotents commutent. La théorie des monoïdes quasi-inversifs n'est donc pas une sous théorie triviale de celle des monoïdes inversifs.

Les propriétés spécifiques de cette expansion, bien plus nombreuses que celles des monoïdes quasi-inversifs quelconques sont présentées. En particulier, alors que l'ordre naturel sur un monoïde quasi-inversif n'est pas, en général, compatible avec le produit, c'est par contre le cas pour tout monoïde quasi-inversif de la forme Q(S).

On montre aussi que le monoïde des tuiles positives (sous-monoïde quasi-inversif du monoïde de McAlster) sur un alphabet A se plonge dans Q(A^*) : l'expansion quasi-inversive du monoïde libre A^*.

Pour définir une notion de reconnaissabilité raisonablement puissante on propose alors de considerer des pré-homomorphismes c'est-à-dire des fonctions monotones (vis à vis de l'ordre naturel) qui ne sont que sous-additives pour le produit, i.e. des fonctions f : S -> T telles que pour tout x et y de S, si x <= y alors f(x) <= f(y) et f(xy) <= f(x) f(y). Nous montrons alors que pour tout morphisme f : A^* -> S peut-être étendu en un pré-homomorphisme de Q(A^*) dans Q(S).

Ce denier résultat, qui pourrait conduire à une notion (quasi-)algébrique de reconnaissabilité caractérisant les langages MSO définissables de tuiles positive, est alors étudié.
 Plus d'infos  


2012-01-24Topological Monadic Logic
11:00-12:00
salle 76
Topological monadic logic refers to weighted structures, i.e., structures whose elements are labelled with non-negative integers called weight. Topological monadic logic extends monadic logic with the ability to express that "there is a bound on the weights appearing on a set X" where X is a monadic variable.

We consider this logic over weighted infinite words (of length omega), and we conjecture that the satisfaction of this logic is decidable (thus extending Büchi's seminal result). In this talk we introduce several equivalent formalisms for this logic, and we present results of normal forms for this logic. We describe the Borel complexity of this logic, and compare its expressiveness with the one of the logic MSO+U. Finally, we will reduce the open conjecture to some new forms of tiling problems.
 Plus d'infos  


2012-01-17WREATH PRODUCT: AN APOLOGY
11:00-12:00
salle 76
The algebraic definition of the wreath product seems at first sight obscure and hostile. However, by considering actions of monoids/groups on trees, this often unpopular operator becomes natural and clear. The use of the wreath product to obtain decompositions of algebraic structures has its most charismatic example in the Krohn-Rhodes Theorem: every finite monoid divides a wreath product of finite simple groups and very small aperiodic monoids. This approach admets extensions to the infinite case, and the wreath product is also essential in the exotic theory of self-similar groups. We shall speak of our recent contributions to these theories, in joint work with Rhodes or Steinberg and Kambites.
 Plus d'infos  


2011-12-13Regular languages of infinite trees that are boolean combinations of open sets.
11:00-12:00
salle 76
This talk will be about boolean (not necessarily positive) combinations of open sets. I will present a decidable characterization of the regular languages of infinite trees that are boolean combination of open sets. In other words, I will present an algorithm, which inputs a regular language of infinite trees, and decides if the language is a boolean combination of open sets. This algorithm uses algebra and will be introduced as a set identities that are satisfied if and only if a language is a boolean combination of open sets and are easily decidable.
 Plus d'infos  


2011-12-06Partial-Observation Stochastic Games: How to Win when Belief Fails
11:00-12:00
salle 76
We consider two-player stochastic games played on finite graphs with reachability (and Buechi) objectives where the first player tries to ensure a target state to be visited (or visited infinitely often) almost-surely, i.e., with probability 1, or positively, i.e., with positive probability, no matter the strategy of the second player.

We classify such games according to the information and to the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation, or two-sided with (c) both players having partial observation.

On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization.

Our main results for pure strategies are as follows: (1) For one-sided games with player 2 perfect observation we show that (in contrast to full randomized strategies) belief-based strategies are not sufficient, and we present an exponential upper bound on memory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete. (2) For one-sided games with player 1 perfect observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required.

We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibits serious flaws in previous results in the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed.
 Plus d'infos  


2011-11-29Towards nominal computation
11:00-12:00
salle 76
Nominal sets are a different kind of set theory, with a more relaxed notion of finiteness. They offer an elegant formalism for describing lambda-terms modulo alpha-conversion, or automata on data words. This presentation is an attempt at defining computation in nominal sets. We present a rudimentary programming language, called Nλ. The key idea is that it includes a native type for finite sets in the nominal sense.
 Plus d'infos  


2011-11-22The Field of Reals is not omega-Automatic
11:00-12:00
salle 76
We investigate structural properties of omega-automatic presentations of infinite structures in order to sharpen our methods to determine whether a given structure is omega-automatic. We apply these methods to show that no field of characteristic 0 admits an injective omega-automatic presentation, and that uncountable fields with a definable linear order cannot be omega-automatic.
 Plus d'infos  


2011-11-15Sur les langages de triplets de mots
11:00-12:00
salle 76
On s'intéresse aux langages de triplets de mots finis de la forme (u1,u2,u3) qui ont pour vocation à représenté des mots «contextualisés». Plus précisément, le triplet de mot (u1,u2,u3) représente le mot u2 dont l’usage est restreint à un certain contexte d’utilisation définit par u1 et u3 de la façon suivante : un tel mot ne peut être concaténé, à gauche, que par un mot finissant par u1 et à droite, que par un mot commençant par u3. L'étude de ce modèle, apparemment ad hoc, et du produit (partiel) qu’il induit, nous conduit cependant à la définition d’une extension originale du monoïde libre qui semble répondre à une question de Jean-Camille Birget en 1992 : quelle structure algébrique correspond aux automates boustrophédons (ou two way automata). En développant cette théorie, on obtient en particulier, pour les langages de triplets :

- d’une notion d'automate boustrophédons déterministe canonique (minimal ?),

- d’une notion d'expression rationnel,

- d’une notion algébrique de reconnaissabilité,

toutes trois équivalentes. La théorie obtenue, qui poursuit les travaux de Rabin et Scott (1959), Shepherdson (1959), Pecuchet (1985), Birget (1989), et de nombreux autres (e.g. Vardi, 1989, Hines 1997), se révèle tout à la fois simple, conséquente et solide. Elle semble ouvrir de nombreuses perspectives aussi bien en algèbre : quelle structure algébrique générique sous-jacente à ce monoid des triplets ? en théorie des automates : quelles liens avec les pebbles two-way automata ? et, en plongeant les mots dans les mots temporisés : quelles expressions algébriques induites pour les langages temporisés ?
 Plus d'infos  


2011-11-08Analyse d'automates à pile pour XML
11:00-12:00
salle 76
Les documents XML sont habituellement représentés sous forme arborescente. Les langages de requête associés, comme XPath, sont des langages navigationnels dans ces arbres, et les automates usuels utilisent des parcours ascendants.

Lire les balises d'un document XML l'une après l'autre revient à parcourir l'arbre correspondant dans l'ordre préfixe. Les automates à pile deviennent alors plus adaptés que les automates d'arbres classiques.

Dans cet exposé, je poserai le problème consistant à répondre aux requêtes au plus tôt, selon ce type de parcours des arbres. Je montrerai qu'il se réduit à décider, pour un préfixe fixé, si tout suffixe "bien formé" est accepté. Je présenterai deux algorithmes pour ce problème, lorsque les requêtes sont données par des automates à pile.
 Plus d'infos  


2011-10-18Recognisability for infinite trees
11:00-12:00
salle 76
We develop a framework for recognisability of languages of infinite trees. This framework has the same expressive power as tree automata. We present an algebraic proof of Rabin's Tree Theorem that does not make use of automata or games.
 Plus d'infos  


2011-10-11Orientations et ordres totaux définissables en logique du second-ordre monadique
11:00-12:00
salle 178
J'examine dans quelle mesure il est possible de définir en logique du second ordre monadique, pour un graphe non orienté: une orientation, toutes les orientations, un ordre total.

Les réponses ne sont pas les mêmes avec ou sans quantifications sur les ensembles d'arêtes. Je mets en évidence des conditions combinatoires qui rendent ces définitions possibles. Certains résultats sont obtenus avec A. Blumensath.
 Plus d'infos  


2011-10-04Langages de rythmes : une approche formelle
11:00-12:00
salle 76
Nous nous intéressons ici à la modélisation des motifs rythmiques. En passant en revue les approches existantes, nous sommes amené étendre le modèle classique des mots temporisés (avec représentation en durée relative) utilisables en musiques en un modèle de mots triplements pondérés. Ce modèle permet en effet de distinguer, pour tout motif rythmique (comme pour tout processus industriel) : une introduction, un développement et une conclusion.

Cette approche, qui induit des opérateurs de composition et de transformation pertinents pour la modélisation musicale, posent plusieurs questions intéressantes de théorie des langages. Séquentialité, parallélisme, temporisation et hiérarchisation semblent par ailleurs et enfin pouvoir être abordé dans un même formalisme. De nombreux développements en perspective ?

 Plus d'infos  


2011-09-27A Class of Probabilistic Automata with a Decidable Value 1 Problem
11:00-12:00
salle 76
The value 1 problem is a decision problem for probabilistic automata over finite words: given a probabilistic automaton A, are there words accepted by A with probability arbitrarily close to 1?

This problem was proved undecidable recently, even in restricted cases.

We introduce a new class of probabilistic automata, called *leak-tight automata*, for which the value 1 problem is shown decidable (and PSPACE-complete). We construct an algorithm based on the computation of a monoid abstracting the behaviours of the automaton. The correctness proof on this algorithm relies on algebraic techniques developed by Simon.
 Plus d'infos  


2011-06-28Représentation de relations par des fonctions unaires; Vérification de propriétés au moyen d'étiquettes
11:00-12:00
amphitheatre (salle 050)
La représentation implicite des graphes, les étiquetages de connexité en présence d'obstacles, la vérification de propriétés du premier ordre au moyen d'étiquettes utilisent des représentations de relations et de propriétés de graphes au moyen de fonctions unaires. L'exposé présentera des exemples concernant les graphes planaires, des méthodes de construction d'étiquetage et des questions ouvertes.
 Plus d'infos  


2011-06-21Krivine machines and higher-order schemes
11:00-12:00
salle 76
(joint work with S. Salvati) We propose a new approach to analysing higher-order recursive
schemes. Many results in the literature use automata models
generalising pushdown automata, most notably higher-order
pushdown automata with collapse (CPDA). Instead, we propose to
use the Krivine machine model. Compared to CPDA, this model is
closer to lambda-calculus, and incorporates nicely many
invariants of computations, as for example the typing
information. The usefulness of the proposed approach is
demonstrated with new proofs of two central results in the field:
the decidability of the local and global model checking problems
for higher-order schemes with respect to the mu-calculus.
 Plus d'infos  


2011-06-14Topological Logics of Euclidean Spaces
11:00-12:00
salle 76
(Joint work with Roman Kontchakov, Yavor Nenov and Michael Zakharyaschev)

The field of Artificial Intelligence known as Qualitative Spatial Reasoning is concerned with the problem of representing and manipulating spatial information about everyday objects. In recent decades, much activity in this field has centred on "spatial logics"---formal languages whose variables range over regions of space, and whose non-logical primitives represent geometrical relations and operations involving those regions. The central problem is to determine whether the configuration described by a given formula is geometrically realizable in 2D or 3D Euclidean space. When the geometrical relations and operations are all topological in character, we speak of a "topological logic".

Topological logics have been intensively studied in Artificial Intelligence over the last two decades. The best-known of these, RCC8 and RCC5, employ variables ranging over regular closed sets, and a collection of eight (respectively, five) binary predicates standing for some basic topological relations between these sets. An important extension of RCC8, known as BRCC8, additionally features functions denoting certain operations on regular closed sets, such as complementation, agglomeration and taking common parts.

None of these languages, however, is able to express the property of connectedness---a serious limitation in practical contexts. In this talk we present new results on topological logics in which this limitation does not apply. Specifically, we consider two new predicates representing, respectively, the property of being connected and the property of having a connected interior. We outline some of the unexpected effects produced by adding these predicates to topological logics interpreted over Euclidean spaces. In particular, we show, that, for any logic featuring the BRCC8-operations and either the connectedness or interior-connectedness predicates, the realizability problem over the Euclidean plane is undecidable.
 Plus d'infos  


2011-06-07A Short History of the Theory of Preprocessing
11:00-12:30
amphitheatre (salle 050)
The talk will survey the theory of preprocessing for NP-hard problems that has emerged in recent years in the context of parameterized / multivariate algorithmics. Some general techniques for obtaining small kernels in polynomial time will be described, as well as new methods for obtaining lower bounds, recent results and research frontiers.
 Plus d'infos  


2011-05-31Comparing Workflow Specification Languages: A Matter of Views
11:00-12:00
salle 76
We address the problem of comparing the expressiveness of workflow specification formalisms using a notion of view of a workflow. Views allow to compare widely different workflow systems by mapping them to a common representation capturing the observables relevant to the comparison. Using this framework, we compare the expressiveness of several workflow specification mechanisms, including automata, temporal constraints, and pre-and-post conditions, with XML and relational databases as underlying data models. One surprising result shows the considerable power of static constraints to simulate apparently much richer workflow control mechanisms.
 Plus d'infos  


2011-05-03First-Order Logic, Collapsible Pushdown Graphs and Automaticity
11:00-12:00
salle 76
A higher-order pushdown automaton is a device endowed with a stack of nested-
stacks. Inductively an order-1 stack is that of a conventional pushdown
automaton. An order-(n+1) stack is a stack of order-n stacks. The transition
graphs of such automata are well-understood. They are intimately related to
the Caucal hierarchy, which subsumes a variety of interesting graphs and whose
members all enjoy decidable MSO theories.

It appears necessary to extend higher-order pushdown automata with additional
structure in the form of `links' if we are to obtain a model of computation
capable of generating the same class of trees as `higher-order recursion
schemes'---natural systems of rewrite rules on non-terminals bearing higher-
order types. Walukiewicz and others established this at order-2 in an ICALP
2005 paper, whilst Hague et al. generalised this to all orders in LICS 2008.
The latter paper revealed the disappointing fact that order-2 CPDA transition
graphs have undecidable MSO theories. They left open the question of first-
order logic.

Initial progress on this was made by Kartzow in a STACS 2010 paper in which he
showed that order-2 CPDA graphs are tree automatic and hence have decidable FO
theories. In this talk I will explain some somewhat surprising results that
show first-order logic to be undecidable at order-3 and above. Some of these
results are particularly strong---for example order-4 graphs generated by a
CPDA that use just order-2 links suffer undecidable first-order model-checking
problems even when we restrict ourselves to sentences with no quantifier
alternation!

I will also mention some positive results. We have rebuilt Kartzow's work via
a notion of automaticity based on nested-words. This offers some advantages
over tree-automaticity in that it allows us to capture precisely the order-2
CPDA graphs and also account for the difference between non-collapsible and
standard order-2 automata in terms of our notion of automaticity. It also
suggests a notion of prefix rewrite system that does at order 2 what
traditional rational prefix rewrite systems do for standard pushdown automata.

If time permits, I will briefly outline some future work that is planned for
next year. This is inspired by the results above and proposes replacing
collapsible pushdown stacks with iterative stacks of nested-words. We hope
this might offer a neater framework in which to work as it would restore the
inductive structure enjoyed by non-collapsible higher-order stacks.
 Plus d'infos  


2011-04-05Complexité d'énumération: méthodes logiques et algébriques
11:00-11:45
salle 76
Dans une première partie je montrerai comment représenter certains problèmes d'énumération par des formules contenant des variables libres du second ordre. On verra que la complexité d'énumération dépend du nombre de quantificateurs ainsi que de la structure sur lequel ces formules sont évaluées (degré bornée, largeur arborescente bornée ...).

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


2011-04-05Acyclicité des hypergraphes et quelques applications
11:45-12:30
salle 76
Il y a plusieurs façons non équivalentes de généraliser l'acyclicité des graphes aux hypergraphes. Nous allons présenter les quatre notions les plus répandues : la Berge, gamma, beta et alpha-acyclicité. Pour cela, nous donnerons des caractérisations de natures diverses (algorithmique, en termes d'arbre de jointure ou tout simplement d'absence de certains types de cycles). Puis nous verrons comment, dans différents contextes (logique, combinatoire, complexité), certaines de ces notions sont plus intéressantes à utiliser que d'autres.
 Plus d'infos  


2011-03-29Context-free groups and locally finite graphs of finite tree-width
11:00-12:00
salle 76
A finitely generated group G is called context-free, if the set of words which represent the identity in G (over its generators) forms a context-free language. It is easy to see that this property is an invariant of the group and does not depend on the choice of generators. Muller and Schupp proved in 1983 that a group G is context-free if and only if it is virtually free, i.e., it has a free subgroup of finite index. Over the past decades many other characterizations of context-free groups have been established. For example, by an action on trees with finite node stabilizers (Dicks 1980, Dicks and Dunwoody 1989), decidability of the MSO theory of its Cayley graph (Kuske and Lohrey 2005). A related theorem of Kuske and Lohrey characterizes context-free groups by Cayley graphs of finite tree-width.

Actually, we can state the following result:

Let Γ be a connected and locally finite graph of finite tree-width. Let G be a group acting on Γ with finitely many orbits. Assume that each node-stabilizer is finite. Then G is virtually free.

In my talk I will speak about a direct and combinatorial proof of this result which became possible due to a modification of a recent construction of Krön for a combinatorial proof of a structure theorem of Stallings (used in all other proofs for the theorem of Muller and Schupp). The talk is based on a joint work with Armin Weiß.
 Plus d'infos  


2011-03-21Démonstration automatique : techniques, outils et certification.
07:00-07:00
salle 76
Notre objectif est de permettre la vérification de programme à l'aide de méthodes fondées sur la preuve et aussi automatisées que possible. Je me concentrerai sur la preuve d'une propriété : la *terminaison*, dans des formalismes à base de récriture. J'esquisserai tout d'abord un panel de techniques pour la preuve de terminaison, adaptées à différentes extensions qui, de proche en proche, mènent de la récriture du premier ordre (non sortée, en théorie libre...) au niveau de langages de programmation courants. Ces techniques sont conçues pour établir *automatiquement* la propriété recherchée ; elles sont implantées dans un certain nombre d'outils (prouveurs) auxquels l'utilisateur doit faire confiance. Cependant, dans les faits, tous ces outils se sont un jour ou l'autre montrés défaillants, rendant délicate leur utilisation dans des domaines où le doute n'est pas permis (vérification de programmes critiques, etc.). J'exposerai alors une approche, à base de génération et d'analyse de traces de preuve, qui permet de *certifier*, par exemple dans l'assistant à la preuve Coq, que les résultats des prouveurs sont corrects. Cette approche concourt ainsi à davantage d'automatisation, notamment en autorisant la délégation de la découverte de preuve à des outils externes à Coq. Je conclurai sur les perspectives offertes par la maturité de ces techniques et approches.
 Plus d'infos  


2011-03-15Deciding emptiness for tree automata with global constraints.
11:00-12:00
salle 76
We study several classes of finite state automata running on ranked terms, extended with constraints that allow to test for equalities or disequalities between subterms. We focus on tree automata with global constraints where the tests are done depending on the states reached by the automaton on its runs. Such automata were introduced by Filiot, Talbot and Tison, 2008, in studies on semi-structured documents where they proved the NP-completeness of the membership problem and the undecidability of the universality problem. Moreover, they showed the decidability of the emptiness problem for several subclasses whith restrictions on the type or the number of (dis)equality constraints. We answer positively the full emptiness decision problem by showing that tree automata with global disequality constraints are equivalent to automata on direceted acyclic graph representations of terms (DAG). Global equality constraints may then be easily added by restrictions on the runs of the DAG automata. Then, we study the emptiness decision problem for automata with global constraints where we authorize "key constraints", that intuitively allow that all subtrees of a given type in an input tree are distincts. We give an emptiness decision procedure that allows to extend the automata with additionnal constraints, like counting constraints or local tests, while preserving decidability.
 Plus d'infos  


2011-03-08Efficient Enumeration of Conjunctive Queries over X-underbar Structures
11:00-12:00
salle 76
This talk focuses on efficient enumeration algorithms for conjunctive queries for databases over binary relations that satisfy the X-underbar property. Tree-like relations such as XPath axes or grids are natural examples of such relations. Enumeration algorithms amount to output answers to queries with a small delay between consecutive answers, while allowing preprocessing the input structure. We first present an algorithm for conjunctive queries over X-underbar structures, avoiding an exponential blowup appearing in existing algorithms. Then, we consider acyclic conjunctive queries and show that such queries admit an enumeration algorithm with a smaller delay. As an application of our method, we also show how these algorithms apply to XPath queries evaluation over XML documents. Finally, we consider conjunctive queries with possible inequalities between variables, which query evaluation turns out to be NP-hard.
 Plus d'infos  


2011-03-01Data languages and rigidly guarded logics
11:00-12:00
salle 76
In algebraic language theory, certain algebraic objects, primarily monoids, are used to analyze the structure of word and tree languages. A fundamental result states that a language of finite words is regular iff it is accepted by a finite monoid. Subclasses of regular languages, such as star-free languages, correspond to natural classes of finite monoids. Most prominently, Schutzenberger, McNaughton, and Papert showed that a regular language is first-order definable iff it is star-free iff it is accepted by an aperiodic monoid.

The study of data languages -- languages over an infinite alphabet -- is motivated by applications in verification and XML processing. In this talk I will report about a recent extension of algebraic techniques to the study of data languages. After a quick overview of some basic concepts related to data languages I will focus on an interesting class of infinite monoids, finite orbit data monoids, which has been recently proposed by Bojanczyk. I will then present a logic, called rigidly guarded monadic second-order logic, that defines exactly the languages recognized by finite orbit data monoids. A theorem akin to Schutzenberger's Theorem also carries over to data languages: one shows that a data language is definable in rigidly guarded first-order logic iff it is recognized by an aperiodic orbit finite data monoid.
 Plus d'infos  


2011-02-15Expressive Power of FO2 on finite trees
11:00-12:00
salle 76
This work belongs to a general effort for understanding the expressive power of first-order logic on finite trees. In particular we seek to obtain decidable characterizations. Meaning a decision procedure for the following problem: given a regular tree language is it definable in FO?

This particular work concerns the study of a fragment of FO: First-Order Logic using only two variables (FO2). I will present various results concerning decidable characterizations for FO2.

This is joint work with Luc Segoufin
 Plus d'infos  


2011-02-08Scheduling of Stochastically Generated Tasks
11:00-12:00
salle 76
In this talk I will present results on the problem of scheduling tasks for execution by a processor when the tasks can stochastically generate new tasks. Tasks can be of different types, and each type has a fixed, known probability of generating d tasks for each number d. We are interested in the random variables modeling the time and space needed to completely execute a task T, that is, to empty the pool of unprocessed tasks assuming that initially the pool only contains the task T. We derive tail bounds for the distributions of these variables and also provide bounds on the expected values of these variables.
 Plus d'infos  


2011-02-01La Boolean width, une largeur de graphes équivalente à la largeur de clique.
11:00-12:00
salle 76
Je présenterai cette notion, introduite par Telle et d'autres de Bergen, et ses motivations algorithmiques. C'est en fait un paramètre auxiliaire permettant d'affiner les temps de calcul de certains algorithmes plus qu'une largeur de graphe d'intérêt intrinsèque.
 Plus d'infos  


2011-01-25Analyse en moyenne d'algorithmes en théorie des langages
11:00-12:00
salle 76
Je montrerai sur deux exemples, l'algorithme de Glushkov et l'algorithme de Moore, le genre de résultats que l'on peut obtenir quand on essaye d'analyser la complexité en moyenne d'algorithmes qui manipulent des objets issus de la théorie des langages. Ce sera l'occasion de montrer quelques techniques de combinatoire analytique et de discuter des choix de distributions.
 Plus d'infos  


2011-01-18A Novel Presentation of the Decidability of Language Equivalence on Deterministic Pushdown Automata
11:00-12:00
salle 76
The aim of the talk is to present the main ideas of a novel presentation of the decidability of language equivalence on deterministic pushdown automata, which is the famous problem solved by G. Senizergues, for which C. Stirling derived a primitive recursive complexity upper bound. The new presentation is based on a reduction to trace equivalence of deterministic first order grammars; this can be also viewed as a problem in term rewriting systems.
 Plus d'infos  


2011-01-18Zero-one laws, random structures, and generic first-order logic
12:00-13:00
salle 76
In this talk I will try to explain the nature of various zero-one laws in terms of the “large scale “ or “generic” logic.

One of the most famous zero-one laws is about finite graphs: for every first-order sentence of graph theory either this sentence or its negation holds almost surely on all finite graphs. The large scale first order logic is an “asymptotic” version of the classical first order logic, where the notion of truth is more relaxed, so in this case a first order sentence holds in a given structure A if it holds “almost surely” in A. It turns out that the zero-one law above means precisely that the large scale first order theory of the complete graph C on countably many vertices (the universe of all the finite graphs!) is complete in the classical model-theoretic meaning. Furthermore, this large scale theory is precisely the standard first order theory of the random subgraphs of C, which are the famous Rado, or Erdos graphs. Here one can see exactly what are the formulas that hold almost surely on all finite graphs.

I will show that similar zero-one laws hold for Cayley graphs of arbitrary finitely generated groups and describe their large scale theories. Surprisingly, these theories are closely related to percolation on groups.

Large scale theories of groups itself (not their Cayley graphs) are much more mysterious. However, recent progress on Tarski problems allows one to describe large scale theories of arbitrary hyperbolic groups - in the large scale logic they look precisely like free groups.
 Plus d'infos  




Liste des événements répétitifs du groupe Graphes et Logique




Retour
Retour à l'index