![[.ics]](small_ics.png)
| Orateur | Bruno Courcelle (LaBRI, Université Bordeaux 1, ) |
| Date | Mardi 28 juin 2011 |
| Salle | Amphithéâtre du LaBRI |
| Titre | Représentation de relations par des fonctions unaires; Vérification de propriétés au moyen d'étiquettes |
| Résumé | 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. |
| Orateur | Igor Walukiewicz (CNRS, LaBRI, ) |
| Date | Mardi 21 juin 2011 |
| Salle | salle 76 |
| Titre | Krivine machines and higher-order schemes |
| Résumé | (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. |
| Orateur | Ian Pratt-Hartmann (University of Manchester, ) |
| Date | Mardi 14 juin 2011 |
| Salle | salle 76 |
| Titre | Topological Logics of Euclidean Spaces |
| Résumé | (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. |
| Orateur | Michael Fellows (Charles Darwin University, ) |
| Date | Mardi 7 juin 2011 |
| Salle | Amphithéâtre du LaBRI |
| Titre | A Short History of the Theory of Preprocessing |
| Résumé | 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. |
| Orateur | Pierre Bourhis (Université Paris Sud, ) |
| Date | Mardi 31 mai 2011 |
| Salle | salle 76 |
| Titre | Comparing Workflow Specification Languages: A Matter of Views |
| Résumé | 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. |
| Orateur | Christopher Broadbent (Oxford University, ) |
| Date | Mardi 3 mai 2011 |
| Salle | salle 76 |
| Titre | First-Order Logic, Collapsible Pushdown Graphs and Automaticity |
| Résumé | 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. |
| Orateur | David Duris (IUT Paris 5, équipe de logique mathématique de Paris 7, ) |
| Date | Mardi 5 avril 2011 |
| Salle | salle 76 |
| Titre | Acyclicité des hypergraphes et quelques applications |
| Résumé | 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. |
| Orateur | Yann Strozecki (Toronto university, ) |
| Date | Mardi 5 avril 2011 |
| Salle | salle 76 |
| Titre | Complexité d'énumération: méthodes logiques et algébriques |
| Résumé | 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. |
| Orateur | Volker Diekert (FMI, Stuttgart university, ) |
| Date | Mardi 29 mars 2011 |
| Salle | salle 76 |
| Titre | Context-free groups and locally finite graphs of finite tree-width |
| Résumé | 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ß. |
| Orateur | Xavier Urbain (ENSIIE, INRIA Saclay Ile de France, LRI, ) |
| Date | Mardi 22 mars 2011 |
| Salle | salle 76 |
| Titre | Démonstration automatique : techniques, outils et certification. |
| Résumé | 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. |
| Orateur | Camille Vacher (LSV, ENS Cachan, ) |
| Date | Mardi 15 mars 2011 |
| Salle | salle 76 |
| Titre | Deciding emptiness for tree automata with global constraints. |
| Résumé | 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. |
| Orateur | Olivier Gauwin (University of Mons, ) |
| Date | Mardi 8 mars 2011 |
| Salle | salle 76 |
| Titre | Efficient Enumeration of Conjunctive Queries over X-underbar Structures |
| Résumé | 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. |
| Orateur | Gabriele Puppis (Oxford University, ) |
| Date | Mardi 1 mars 2011 |
| Salle | salle 76 |
| Titre | Data languages and rigidly guarded logics |
| Résumé | 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. |
| Orateur | Thomas Place (LSV, ENS Cachan, ) |
| Date | Mardi 15 février 2011 |
| Salle | Salle 76 |
| Titre | Expressive Power of FO2 on finite trees |
| Résumé | 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 |
| Orateur | Tomas Brazdil (Masaryk University, ) |
| Date | Mardi 8 février 2011 |
| Salle | salle 76 |
| Titre | Scheduling of Stochastically Generated Tasks |
| Résumé | 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. |
| Orateur | Bruno Courcelle (LaBRI, ) |
| Date | Mardi 1 février 2011 |
| Salle | salle 73 |
| Titre | La "Boolean width", une largeur de graphes équivalente à la largeur de clique. |
| Résumé | 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. |
| Orateur | Cyril Nicaud (Université Paris-Est - Marne-la-Vallée, ) |
| Date | Mardi 25 janvier 2011 |
| Salle | salle 76 |
| Titre | Analyse en moyenne d'algorithmes en théorie des langages |
| Résumé | 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. |
| Orateur | Petr Jancar (Center of Applied Cybernetics, ) |
| Date | Mardi 18 janvier 2011 |
| Salle | salle 76 |
| Titre | A Novel Presentation of the Decidability of Language Equivalence on Deterministic Pushdown Automata |
| Résumé | 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. |
| Orateur | Alexei Miasnikov (Stevens Institute - McGill University, ) |
| Date | Mardi 18 janvier 2011 |
| Salle | salle 76 |
| Titre | Zero-one laws, random structures, and generic first-order logic |
| Résumé | 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. |
| Orateur | Michele Abrusci (Universita Roma 3, ) |
| Date | Mardi 14 décembre 2010 |
| Salle | salle 76 |
| Titre | Connecteurs multiplicatifs généralisés dans la logique non-commutative |
| Résumé | On va montrer les lignes d'une possible extension à la logique non-commutative de la notion de connecteur multiplicatif généralisé qui a été introduite en 1987 par Jean-Yves Girard dans l'article "Multiplicatives" et qui a été le premier cas de définition de connecteur sans se référer à une "sémantique". |
| Orateur | Laurent Bienvenu (Liafa, ) |
| Date | Mardi 7 décembre 2010 |
| Salle | salle 76 |
| Titre | Lemme local de Lovasz et sa preuve constructive par Moser et Tardos |
| Résumé | Le lemme local de Lovasz est un théorème important de combinatoire/probabilités discrètes, exprimant le fait qu'une conjonction d'évènements "quasi-indépendants" (dans un certain sens que l'on discutera) a une probabilité non-nulle. Jusqu'à très récemment, la preuve de ce théorème était non-constructive: à supposer que les évènements dépendent d'un ensemble de variables V, le lemme local de Lovasz indique qu'il existe une instantiation des variables satisfaisant la conjonction des évènements, mais ne permet pas de trouver algorithmiquement une telle instantiation. C'est ce problème qu'ont résolu Moser et Tardos en 2009, en donnant un algorithme probabiliste pour trouver une instantiation de façon efficace. Dans cet exposé, on donnera les grandes lignes de la (très élégante) preuve de ce résultat. |
| Orateur | Lukasz Kaiser (Liafa, ) |
| Date | Mardi 30 novembre 2010 |
| Salle | salle 76 |
| Titre | New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures |
| Résumé | We present a new algorithm for model-checking weak monadic second-order logic on inductive structures, a class of structures of bounded clique width. Our algorithm directly manipulates formulas and checks them on the structure of interest, thus avoiding both the use of automata and the need to interpret the structure in the binary tree. In addition to the algorithm, we give a new proof of decidability of weak MSO on inductive structures which follows Shelah's composition method. Generalizing this proof technique, we obtain decidability of weak MSO extended with the unbounding quantifier on the binary tree, which was open before. We also present preliminary experimental results. |
| Orateur | Sylvain Schmitz (LSV, ENS Cachan, ) |
| Date | Mardi 23 novembre 2010 |
| Salle | salle 76 |
| Titre | Ackermann and Primitive-Recursive Bounds with Dickson's Lemma |
| Résumé | Dickson's Lemma is a simple yet powerful tool widely used in termination proofs, especially when dealing with counters or related data structures. However, most computer scientists do not know how to derive complexity upper bounds from such termination proofs, and the existing literature is not very helpful in these matters. We propose a new analysis of the length of bad sequences over (N^k,leq) and explain how one may derive complexity upper bounds from termination proofs. Our upper bounds improve earlier results and are essentially tight. |
| Orateur | Maxime Senot (LIFO, université d'Orléan, ) |
| Date | Mardi 26 octobre 2010 |
| Salle | salle 76 |
| Titre | Construction géométrique pour résoudre Q-SAT en temps et espace bornés. |
| Résumé | Il est possible de mener des calculs complexes avec des particules se déplaçant à vitesse constante sur la droite euclidienne et avec leurs collisions. A partir de cela a été défini un modèle abstrait et géométrique de calcul, les machines à signaux, qui sont à espace et temps continus. Les calculs sont alors représentés par des diagrammes espace-temps en 2 dimensions. Après avoir introduit et défini ce modèle, nous montrerons comment il nous permet de résoudre en temps et espace bornés le problème de satisfaisabilité des formules booléennes quantifiées, Q-SAT, qui est PSPACE-complet. Nous proposerons également une notion de complexité plus pertinente et mieux adaptée aux machines à signaux, prenant en compte le parallélisme inhérent un modèle, et qui sera en temps quadratique notre solution de Q-SAT. |
| Orateur | Jean-Eric Pin (Liafa, ) |
| Date | Mardi 5 octobre 2010 |
| Salle | salle 178 |
| Titre | La notion abstraite de reconnaissance: algèbre, logique et topologie (joint work with M. Gehrke and S. Grigorieff) |
| Résumé | Nous proposons une nouvelle approche de la notion de reconnaissance, qui diffère des définitions classiques par trois aspects particuliers. Tout d'abord, notre approche n'utilise pas du tout les automates. Ensuite, elle s'applique à des algèbres de Boole de parties plutôt qu'à des ensembles pris individuellement. Enfin elle repose sur la topologie. Nous montrons l'existence d'un reconnaisseur minimal dans un cadre très général qui s'applique en particulier à n'importe quelle algèbre de Boole de parties d'un espace discret. Nos résultats principaux montrent que ce reconnaisseur minimal est un espace uniforme dont la complétion est le dual de l'algèbre de Boole considérée pour la dualité de Stone-Priestley. Dans le cas d'une algèbre de Boole de langages fermée par quotient, cette complétion, appelée l'espace syntactique de l'algèbre de Boole, est un monoïde compact si et seulement si tous les langages de l'algèbre de Boole sont reconnaissables. Dans le cas des langages reconnaissables, on retrouve ainsi les notions de monoïde syntactique et de monoïde profini libre. Pour les langages non reconnaissables, l'espace syntactique est toujours un espace compact mais n'est plus un monoïde. Par ailleurs, nous donnons une description équationnelle des algèbres de Boole fermées par quotient, qui étend aux langages non reconnaissables les résultats connus sur les langages reconnaissables. Finalement, nous généralisons tous ces résultats des algèbres de Boole aux treillis, cas dans lequel les structures topologiques sont partiellement ordonnées. |