Séminaire de l'équipe Méthodes Formelles (MF)

Le séminaire MF a lieu salle 076 presque tous les mardis à 11H.

Pour proposer un séminaire, le calendrier vous aidera à choisir une date disponible.

Pour s'abonner ou se désabonner de la liste de diffusion.


Prochains exposés

DateOrateurTitre



Précédents exposés depuis janvier 2016

DateOrateurTitre
mardi 12 juillet 2016Mark Lawson (Heriot Watt University) Non commutative booléen algebras
I shall explain what the title of the talk means and hint at connections with multiple valued logic.
mardi 05 juillet 2016Valia Mitsou (MTA SZTAKI) Double-exponential and triple-exponential bounds for choosability problems parameterized by treewidth
Choosability, introduced by Erdos, Rubin, and Taylor [Congr. Number. 1979], is a well-studied concept in graph theory: we say that a graph is $c$-choosable if for any assignment of a list of $c$ colors to each vertex, there is a proper coloring where each vertex uses a color from its list. We study the complexity of deciding choosability on graphs of bounded treewidth. It follows from earlier work that 3-choosability can be decided in time $2^{2^{O(w)}}·n^{O(1)}$ on graphs of treewidth $w$. We complement this result by a matching lower bound giving evidence that double-exponential dependence on treewidth may be necessary for the problem: we show that an algorithm with running time $2^{2^{o(w)}}·n^{O(1)}$ would violate the Exponential-Time Hypothesis (ETH). We consider also the optimization problem where the task is to delete the minimum number of vertices to make the graph 4-choosable and demonstrate that dependence on treewidth becomes triple-exponential for this problem: it can be solved in time $2^{2^{2^{O(w)}}}·n^{O(1)}$ on graphs of treewidth $w$, but an algorithm with running time $2^{2^{2^{o(w)}}}·n^{O(1)}$ would violate ETH. The significance of the results is that these problems are apparently the first fairly natural graph-theoretic problems that require double-exponential or triple-exponential dependence on treewidth. Joint work with Dániel Marx.
mardi 28 juin 2016M. Praveen (CMI Chennai) Nesting Depth of Operators in Graph DatabaseQueries: Expressiveness vs. Evaluation Complexity
Expressiveness and efficient algorithms for query evaluation are conflicting goals while designing languages for querying graph structured data. To better handle dynamically changing data, recent work has been done on designing query languages that can compare values stored in the graph database, without hard coding the values in the query. The main idea is to allow variables in the query and bind the variables to values when evaluating the query. For query languages that bind variables only once, query evaluation is usually NP-complete. There are query languages that allow binding inside the scope of Kleene star operators, which can themselves be in the scope of bindings and so on. Uncontrolled nesting of binding and iteration within one another results in query evaluation being PSPACE-complete. In this talk, we present a way to syntactically control the nesting depth of iterated bindings, and study how this affects the expressiveness and complexity of query evaluation. This is joint work with B. Sreevathsan. **Séminaire en salle 178**
mardi 07 juin 2016 Aiswarya Cyriac (CMI Chennai) Data Communicating Processes with Unreliable Channels
We extend the classical model of lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration. This a joint work with Parosh Abdulla and Mohammed Faouzi Atig.
mardi 31 mai 2016John Fearnley (University of Liverpool) The Complexity of All-switches Strategy Improvement
We study all-switches strategy improvement algorithms for parity, mean-payoff, discounted-payoff, and simple stochastic games. While these algorithms are now known to take exponential time in the worst case, we follow a recent line of work on the simplex method, and study them from a computational complexity point of view. We show that it is PSPACE-complete to decide the following problems: (1) given an edge e, will all-switches strategy improvement ever switch e? (2) given an edge e, is e in the optimal strategy found by all-switches strategy improvement?
mercredi 18 mai 2016Narayan Kumar (CMI Chennai) Regular Abstractions of One Counter Languages
We study the complexity of the following problems: Given a one counter automaton A 1) construct an NFA that accepts the upward closure of the language of A (w.r.t. subword ordering) 2) construct an NFA that accepts the downward closure of the language of A 3) construct an NFA that accepts a language whose Parikh-image is the Parikh-image of the language of A. Joint work with M.F. Atig (Uppsala), D. Chistikov (Oxford), P. Hofman (Cachan), P. Saivasan (Kaiserlautern) and G. Zetzsche (Cachan).
mardi 10 mai 2016Edon Kelmendi (LaBRI) Deciding Maxmin Reachability in Half-Blind Stochastic Games
Two-player, turn-based, stochastic games with reachability conditions are considered, where the maximizer has no information (he is blind) and is restricted to deterministic startegies whereas the minimizer is perfectly informed. We ask the question of whether the game has maxmin 1 in other words we ask whether for all epsilon>0 there exists a deterministic strategy for the (blind) maximizer such that against all the strategies of the minimizer, it is possible to reach the set of final states with probability larger than 1-epsilon. This problem is undecidable in general, but we define a class of games, called leaktight half-blind games where the problem becomes decidable. We also show that mixed strategies in general are stronger for both players and that optimal strategies for the minimizer might require infinite-memory.
mardi 03 mai 2016Diego Figueira (CNRS / LaBRI) Semantic acyclicity of conjunctive queries
The evaluation problem for Conjunctive Queries (CQ) is known to be NP-complete in combined complexity and W[1]-complete in parameterized complexity. However, acyclic CQs and more generally CQs of bounded tree-width can be evaluated in polynomial time in combined complexity and they are fixed-parameter tractable. We study the problem of whether a CQ can be rewritten into an equivalent CQ of bounded tree-width, in the presence of unary functional dependencies. We show that this problem is decidable in doubly exponential time, or in exponential time for a restricted class of queries. When it exists, the algorithm also yields a witness query. This is a work that will appear in LICS this summer.
mardi 19 avril 2016Ranko Lazic (Warwick University) Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete
Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space. Joint work with Matthias Englert and Patrick Totzke, available from: http://arxiv.org/abs/1602.00477
jeudi 14 avril 2016Hubie Chen (Ikerbasque) The Logic of Counting Query Answers: A Study via Existential Positive Queries
We consider the computational complexity of the problem of counting the number of answers to a logical formula on a finite structure. We present two contributions. First, in the setting of parameterized complexity, we present a classification theorem on classes of existential positive queries. In particular, we prove that (relative to the problem at hand) any class of existential positive formulas is interreducible with a class of primitive positive formulas. In the setting of bounded arity, this allows us to derive a trichotomy theorem indicating the complexity of any class of existential positive formulas, as we previously proved a trichotomy theorem on classes of primitive positive formulas. This new trichotomy theorem generalizes and unifies a number of existing classification results in the literature, including classifications on model checking primitive positive formulas, model checking existential positive formulas, and counting homomorphisms. Our second contribution is to introduce and study an extension of first-order logic in which algorithms for the counting problem at hand can be naturally and conveniently expressed. In particular, we introduce a logic which we call #-logic where the evaluation of a so-called #-sentence on a structure yields an integer, as opposed to just a propositional value (true or false) as in usual first-order logic. We discuss the width of a formula as a natural complexity measure and show that this measure is meaningful in #-logic and that there is an algorithm that minimizes width in the "existential positive fragment" of #-logic. This is joint work with Stefan Mengel (CNRS).
mardi 12 avril 2016Hubie Chen (Ikerbasque) One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries
We study the classical problem of conjunctive query evaluation, here restricted according to the set of permissible queries. In this work, this problem is formulated as the relational homomorphism problem over a set of structures A, wherein each instance must be a pair of structures such that the first structure is an element of A. This problem generalizes the graph homomorphism problem of deciding, given a pair of graphs, whether or not there is a homomorphism from the first to the second. We present a comprehensive complexity classification of these problems, which strongly links graph-theoretic properties of A to the complexity of the corresponding homomorphism problem. - In particular, we define a binary relation on graph classes and completely describe the resulting hierarchy given by this relation; this description involves defining a new graph-theoretic measure called stack depth which may be of independent interest. The binary relation is defined in terms of a notion which we call graph deconstruction and which is a variant of the well-known notion of tree decomposition. The hierarchy that results is reminiscent of that identified by Blumensath and Courcelle (LMCS 2010). - We then use this graph hierarchy to infer a complexity hierarchy of homomorphism problems which is comprehensive up to a computationally very weak notion of reduction, namely, a parameterized form of quantifier-free reductions. We obtain a significantly refined complexity classification of left-hand side restricted homomorphism problems, as well as a unifying, modular, and conceptually clean treatment of existing complexity classifications, such as the classifications by Grohe-Schwentick-Segoufin (STOC 2001) and Grohe (FOCS 2003, JACM 2007). In this talk, we will also briefly discuss parameterized complexity classes that we introduced/studied which capture some of the complexity degrees identified by our classification. This talk is based on joint work with Moritz M"uller that appeared in PODS ’13 and CSL-LICS ’14.
mardi 05 avril 2016Nathan Lhote (LaBRI) Towards an algebraic theory of rational word functions
In formal language theory, several different models characterize regular languages, such as finite automata, congruences of finite index, or monadic second-order logic (MSO). Moreover, several fragments of MSO have effective characterizations based on algebraic properties. When we consider transducers instead of automata, such characterizations are much more challenging, because many of the properties of regular languages do not generalize to regular word functions. In this paper we consider word functions that are definable by one-way transducers (rational functions). We show that the canonical bimachine of Reutenauer and Schützenberger preserves certain algebraic properties of rational functions, similar to the case of word languages. In particular, we give an effective characterization of functions that can be defined by an aperiodic one-way transducer.
mardi 29 mars 2016David Janin (LaBRI) Programmation réactive par tuilage
Ou comment faire de la programmation événementielle, temps réel et concurrente, sans évènements, sans produit concurrent et donc sans deadlock.. Travail en cours avec Simon Archipoff
mardi 22 mars 2016Mikolaj Bojanczyk (University of Warsaw) For graphs of bounded tree width, recognisability equals definability in MSO.
We prove a conjecture of Bruno Courcelle, which states that a graph property is definable in MSO with modular counting predicates on graphs of constant treewidth if, and only if it is recognizable in the sense that constant-width tree decompositions of graphs satisfying the property can be recognized by tree automata. In our proof, we show that for every k there is an mso transduction which computes tree decompositions for graphs of tree-width at most k. One of the ingredients is the Factorisation Forest Theorem of Imre Simon.
mardi 08 mars 2016Sylvain Schmitz (LSV - ENS Cachan) The Complexity of Coverability in nu-Petri Nets
We show that the coverability problem in nu-Petri nets is complete for 'double Ackermann' time, thus closing an open complexity gap between an Ackermann lower bound and a hyper-Ackermann upper bound. The coverability problem captures the verification of safety properties in this nominal extension of Petri nets with name management and fresh name creation. Our completeness result establishes nu-Petri nets as a model of intermediate power among the formalisms of nets enriched with data, and relies on new algorithmic insights brought by the use of well-quasi-order ideals. Joint work with Ranko Lazic, preprint available from https://hal.inria.fr/hal-01265302.
mardi 01 mars 2016Paul Gastin (LSV - ENS Cachan) Reasoning about distributed systems: WYSIWYG
There are two schools of thought on reasoning about distributed systems: one following interleaving based semantics, and one following partial-order/graph based semantics. We will compare these two approaches and argues in favour of the latter. An introductory treatment of tree automata techniques (via split-width) to reason about distributed systems is also provided.
mardi 16 février 2016Denis Kuperberg (TU Munich) Sensing cost for automata and synthesis
I will present a complexity measure named sensing cost, designed for automata and transducters. It measures the average amount of information from the environment that must be read by the system at each time instant, in a random environment. It is then natural to look for minimally sensing automata for a given language, or minimally-sensing transducers as solutions of synthesis problems. I will present results along these lines, as well as open problems that remain to be tackled. This is joint work with Shaull Almagor and Orna Kupferman.
mardi 09 février 2016Laure Daviaud (LIP - ENS Lyon) A Generalised Twinning Property for Minimisation of Cost Register Automata.
Weighted automata extend finite-state automata by associating with transitions weights from a semiring S, defining functions from words to S. Recently, cost register automata have been introduced as an alternative model to describe any function realised by a weighted automaton by means of a deterministic machine. Unambiguous weighted automata over a group G can equivalently be described by cost register automata whose registers take their values in G, and are updated by operations of the form x:=y.c, with c in G, and x,y registers. This class is denoted by CRA(G). In this talk, I will introduce a twinning property and a bounded variation property parametrised by an integer k, such that the corresponding notions introduced originally by Choffrut for finite-state transducers are obtained for k=1. Our main result links these notions with the register complexity of CRA(G). More precisely, we prove that given an unambiguous weighted automaton W over an infinitary group G realizing some function f, the three following properties are equivalent: i) W satisfies the twinning property of order k, ii) f satisfies the k-bounded variation property, iii) f can be described by a CRA(G) with at most k registers. Actually, this result is proved in a more general setting, considering machines over the semiring of finite sets of elements from G and is extended to prove a similar result for finite-valued finite-state transducers. Finally, the effectiveness of the constructions leads to decidability/complexity results about the register complexity (i.e. what is the minimal number of registers needed to compute a given function) of cost register automata. This is a joint work with Pierre-Alain Reynier and Jean-Marc Talbot.
mardi 02 février 2016Hugo Gimbert (CNRS / LaBRI) A Class of Zielonka Automata with a Decidable Controller Synthesis Problem
The decidability of the distributed version of the Ramadge and Wonham control problem, where both the plant and the controllers are modelled as Zielonka automata is a challenging open problem. There exists three classes of plants for which the existence of a correct controller has been shown decidable in the distributed setting: when the dependency graph of actions is series-parallel, when the processes are connectedly communicating and when the dependency graph of processes is a tree. We generalize these three results by showing that a larger class of plants, called broadcast plants, has a decidable controller synthesis problem. We give new examples of plants for which controller synthesis is decidable.
mardi 12 janvier 2016Laura Ciobanu (University of Neuchâtel, Switzerland) The language complexity of solutions of equations in free semigroups and free groups
We show that, given a word equation over a finitely generated free group (or semigroup), the set of all solutions in reduced words forms an EDT0L language. In particular, it is an indexed language in the sense of Aho. This is joint work with Murray Elder and Volker Diekert.



Archives des années précédentes




Responsables

Diego Figueira, Gabriele Puppis