| Date | Orateur | Titre |
|---|
| mardi 13 décembre 2016 | Anca Muscholl (LaBRI)
| Sound negotiations and static analysis |
| Negotiations are a graphical formalism for describing multiparty distributed cooperation, proposed by Desel and Esparza. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed.
In a former paper, Esparza and Desel have shown that deciding soundness of arbitrary negotiations is PSPACE-complete, and in PTIME for deterministic negotiations. They also considered an intermediate subclass of non-deterministic negotiations, but left the complexity of the soundness problem open.
We first consider the soundness problem beyond deterministic negotiations: we show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.
Then we show how to use our algorithmic results to provide polynomial algorithms for some analysis problems of workflow nets with data.
Joint work with J. Esparza, D. Kuperberg and I. Walukiewicz |
| jeudi 01 décembre 2016 | Mahesh Viswanathan (University of Illinois)
| Translating LTL to Probabilistic Automata |
| Starting with the seminal work of Sistla, Vardi, and Wolper (1985),
there has been a lot of interest in discovering efficient translations
of Linear Temporal Logic (LTL) formulae into small automata. The
reason for this is that logic to automata translations directly impact
the complexity of runtime monitoring, verification, and synthesis of
systems. While much of the work has focused on translations from LTL
to nondeterministic and deterministic automata, in this talk we will
present new constructions of probabilistic automata for LTL. We will
discuss the consequences of this translation to the asymptotic
complexity of problems in monitoring and verification of stochastic
systems.
Joint work with Dileep Kini |
| mardi 29 novembre 2016 | Petr Jancar (Technical University of Ostrava)
| Deciding semantic finiteness of first-order grammars w.r.t. bisimulation equivalence |
| The plan is to explain the main ideas of the MFCS'16 paper http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=6464,
by figures (and without formalities).
The presented decidability proof for semantic finiteness (or "regularity") of first-order grammars (that encompass pushdown automata)
w.r.t. bisimulation equivalence relies on the decidability of bisimulation equivalence (which was first proven by Senizergues).
|
| mardi 22 novembre 2016 | Georg Zetzsche (ENS Cachan)
| Subword Based Abstractions of Formal Languages |
| A successful idea in the area of verification is to consider finite-state abstractions of infinite-state systems. A prominent example is the fact that many language classes satisfy a Parikh's theorem, i.e. for each language, there exists a finite automaton that accepts the same language up to the order of letters. Hence, provided that the abstraction preserves pertinent properties, this allows us to work with finite-state systems, which are much easier to handle.
While Parikh-style abstractions have been studied very intensely over the last decades, recent years have seen an increasing interest in abstractions based on the subword ordering. Examples include the set of (non necessarily contiguous) subwords of members of a language (the downward closure), or their superwords (the upward closure). Whereas it is well-known that these closures are regular for any language, it is often not obvious how to compute them. Another type of subword based abstractions are piecewise testable separators. Here, a separators acts as an abstraction of a pair of languages.
This talk will present approaches to computing closures, deciding separability by piecewise testable languages, and a (perhaps surprising) connection between these problems. If time permits, complexity issues will be discussed as well. |
| mardi 15 novembre 2016 | Igor Walukiewicz (LaBRI)
| Systems with Parametric Thread Creation |
| We consider multi-threaded systems which combine recursion, or even higher-order recursion, with dynamic thread creation. Communication between threads is via global variables as well as via local variables that are shared between a thread and its sub-threads. Reading and writing are atomic operations, while we do not allow locks or operations of the type compare-and-set. The resulting systems are still too expressive to be decidable. As an abstraction, we therefore replace thread creation with parametric thread creation and show for the resulting systems, that the reachability problem is decidable.
This is joint work with Anca Muscholl and Helmut Seidl. |
| mardi 08 novembre 2016 | Paulin Fournier (LaBRI)
| Parameterized verification of networks of many identical processes |
| I'll give an overview of my pd thesis result on parameterized verification of networks composed of many identical processes for which the number of processes is the parameter.
I'll present the decidability of the parameterized reachability problem in selective networks, where the messages only reach a subset of the components. This result is obtained thanks to a reduction to a new model of distributed two-player games for which we prove decidability in coNP of the game problem. Finally, I will present local strategies that enforce all processes to resolve the non-determinism only according to their own local knowledge. Under this assumption of local strategy, we were able to show that the parameterized reachability and synchronization problems are NP-complete. |
| mardi 25 octobre 2016 | David Janin (LaBRI)
| Semantics models for timed programing languages |
| In this talk, I consider temporally causal functions of timed streams, i.e. functions that produce output values at a given instant that only depends on the input values that have been received till that instant.
Defining partial timed streams that form a directed complete partial order (DCPO), I will show how causal functions are nicely captured as limits of continuous and synchronous functions over these DCPO offering thus a denotational model of causal timed functions. Relaxing synchronous hypothesis to pre-synchronous hypothesis, I will show how every causal function admits a lattice of possible denotations such that:
- the least element can be understood as the latest semantics of that function: output values are computed when they need to be outputted,
- the greatest element can be understood as a the earliest semantics of that function: output values are computed as soon as all the input values they depend have been received.
- other elements in between can be understood as the various possible computation schedules that can still be followed in order to run the causal function.
The categorical properties of these continuous functions will then be detailed, offering various relevant operators for programing with these functions.
Last, I will show that a notion of causal function residual is available so that a minimal (possibly continuous) IO-automaton can be associated to every causal functions, providing thus a clear operation (latest) semantics. Open perspectives or questions will conclude this presentation. |
| mardi 18 octobre 2016 | Nicolas Perrin (Institut des Systèmes Intelligents et de Robotique (ISIR) )
| Humanoid robotics and motion abstractions |
| Humans typically do not realize how much intelligence is required to perform usual motions.
One of the reasons why we are so good at motion control seems to be that we can abstract continuous inputs and outputs and their relationships with great flexibility, and perhaps reason almost symbolically on these abstractions.
This observation leads to the temptation to tackle humanoid robot motion problems with discrete abstractions and formal methods. |
| mardi 11 octobre 2016 | Hubie Chen (Universidad del País Vasco)
| Walking the Boundary Between Tractability and Intractability |
| I will give an overview of some of my past and expected future research. I will focus on complexity classification theorems — which classify (or attempt to classify) all problems in some problem family of interest — and their interactions with other areas of theoretical computer science. In particular, I will discuss work on the template-restricted constraint satisfaction problem and variants thereof; and, work on model checking first-order logic with respect to different classes of sentences. |
| mardi 04 octobre 2016 | Bruno Courcelle (LaBRI)
| Evaluations de requêtes au moyen d'automates programmés (Query evaluations by fly-automata) |
| Les formules de la logique du second-ordre monadique définissent des ensembles de p-uplets d'ensembles
sur lesquels on peut faire du comptage et des recherches de cardinalité.
On considère dans cet exposé des combinaisons de comptages et de cardinalités.
On utilise pour cela deux types de déterminisation des automates.
Exposé en français. Les transparents sont en anglais. |
| mardi 12 juillet 2016 | Mark 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 2016 | Valia 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 2016 | M. 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 2016 | John 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 2016 | Narayan 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 2016 | Edon 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 2016 | Diego 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 2016 | Ranko 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 2016 | Hubie 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 2016 | Hubie 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 2016 | Nathan 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 2016 | David 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 2016 | Mikolaj 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 2016 | Sylvain 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 2016 | Paul 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 2016 | Denis 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 2016 | Laure 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 2016 | Hugo 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 2016 | Laura 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. |