
Liste des événements uniques du groupe Séminaire Méthodes Formelles
20171212  La coloration de graphe dans le modèle LOCAL  Partie II 
11:0012:00 178 
Partie II:
 Coloration rapide des cycles
 Borne inférieure en log* sur la coloration des cycles (preuve de Linial)
 Une preuve alternative fondé sur le théorème de Ramsey
 Etat de l'art 
 Plus d'infos 

20171205  La coloration de graphe dans le modèle LOCAL  Partie I 
11:0012:00 178 
L'objectif de cette série d'exposés est de faire découvrir un résultat aussi élégant que surprenant du calcul distribué, à savoir la 3coloration des ncycles en temps log*(n). On démontrera l'optimalité de ce résultat ainsi que ces généralisations au cas des graphes arbitraires.
Partie I:
 Le modèle LOCAL
 Le problème de la coloration
 Coloration des 1orientations en 6 couleurs
 De 6 à 3 couleurs
 Cas des graphes arbitraires 
 Plus d'infos 

20171128  Succinct progress measures and solving parity games in quasipolynomial time 
11:0012:00 178 
The recent breakthrough paper by Calude et al. (a winner of STOC 2017 Best Paper Award) has given the first algorithm for solving parity games in quasipolynomial time, where previously the best algorithms were mildly subexponential. We devise an alternative quasipolynomial time algorithm based on progress measures, which allows us to reduce the space required from quasipolynomial to nearly linear. Our key technical tools are a novel concept of ordered tree coding, and a succinct tree coding result that we prove using bounded adaptive multicounters, both of which are interesting in their own right.
Apart from presenting our technical work on succinct progress measures, I will survey the relevance of parity games to the theory and practice of computeraided verification and synthesis, their surprising impact on broader theoretical computer science, the history of results and techniques used for solving parity games, and the recent advances in the state of the art.
This is joint work with Marcin Jurdzinski. 
 Plus d'infos 

20171121  Model Checking: the Interval Way 
11:0012:00 178 
Model checking with interval temporal logics is emerging as a viable alternative to model checking with standard pointbased temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modelled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted "pointwise" describe how the system evolves statebystate, and predicate properties of system states, those which are interpreted "intervalwise" express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). The most wellknown interval temporal logic is Halpern and Shoham's modal logic of time intervals HS, which features one modality for each possible ordering relation between a pair of intervals, apart from equality. In the seminar, we provide an overview of the main results on model checking with HS and its fragments under the homogeneity assumption. In particular, we show that the problem turns out to be nonelementarily decidable and EXPSPACEhard for full HS, but it is often computationally much better for its fragments. Then, we briefly compare the expressiveness of HS in model checking with that of LTL, CTL, CTL*. We conclude by discussing a recent generalization of the proposed MC framework that allows one to use regular expressions to define the behavior of proposition letters over intervals in terms of the component states. 
 Plus d'infos 

20171107  Formal methods for capturing dynamics of biological networks 
11:0012:00 178 
Computational models of biological networks aim at reporting the indirect influences between the different molecular entities acting within the cell (genes, RNA, proteins, ...). In this talk, I will give an overview of methods for the formal assessment of dynamics of biological networks by static analysis. After an introduction to Boolean networks and their relevance for modelling cell signalling and gene regulatory networks, I'll present an abstract interpretation of their trajectories based on a causal analysis. Then, I'll show how we can combine this abstraction with SAT approches to address systems biology challenges, such as model identification and cell reprogramming. 
 Plus d'infos 

20171031  Rewriting Higherorder Stack Trees 
11:0012:00 178 
Higherorder pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the satisfaction of any formula written in monadic second order logic (respectively first order logic with reachability predicates) can be decided on such a graph.
The purpose of this talk is to propose a common extension to both higherorder stack operations and ground tree rewriting. We introduce a model of higherorder ground tree rewriting over trees labelled by higherorder stacks (henceforth called stack trees), which syntactically coincides with ordinary ground tree rewriting at order 1 and with the dynamics of higherorder pushdown automata over unary trees. The rewriting system is obtained through the definition of DAGs of operations.
Our contribution is twofold (apart from the definition of the model):
 define a automaton model over DAGs of operations, and show it is closed under iteration.
 showing that the model checking problem for firstorder logic with reachability is decidable for the infinite graphs generated by stack tree rewriting systems. This last proof uses the technique of finite set interpretations presented by Colcombet and Loding. 
 Plus d'infos 

20171024  Constructive completeness for the lineartime mucalculus 
11:0012:00 178 
Modal mucalculus is one of the central logics for verification. In his seminal paper, Kozen proposed an axiomatization for this logic, which was proved to be complete, 13 years later, by Kaivola for the lineartime case and by Walukiewicz for the branchingtime one. These proofs are based on complex, nonconstructive arguments, yielding no reasonable algorithm to construct proofs for valid formulas. The problematic of constructiveness becomes central when we consider proofs as certificates, supporting the answers of verification tools. We provide a new completeness argument for the lineartime mucalculus which is constructive, i.e. it builds a proof for every valid formula. To achieve this, we decompose this difficult problem into several easier ones, taking advantage of the correspondence between the mucalculus and automata theory. More precisely, we lift the wellknown automata transformations (nondeterminization for instance) to the logical level. To solve each of these smaller problems, we perform first a proofsearch in a circular proof system, then we transform the obtained circular proofs into proofs in Kozen's axiomatization. This yields a constructive proof for the full lineartime mucalculus. 
 Plus d'infos 

20171017  Timed domains: an appetizer 
11:0012:00 178 
we develop a general theory of timed domains and timed morphisms that aims at offering a versatile and sound mathematical framework for the study of timed denotational semantics of networks of timed programs. The proposed compositional semantic model accounts for the fact that every non trivial computation step necessarily takes some non zero time. This is achieved by defining timed domains as classical domains (directed complete posets) where time appears everywhere: every increase of knowledge necessarily refers to the passage of time. Timed morphisms are defined as functions between timed domains which uniformly act on the underlying time scales. The resulting category is a (bi)cartesian closed category with (mostly) internal henceforth timed least fixpoint operators. Moreover, by allowing (almost) arbitrary posets as time scales, the proposed frame work also covers typical features of parallel or concurrency theory such as parallel, indenpendant or conflicting computations. In other words, timed domains and timed morphisms provide a fully featured mathematical framework for the study of computable spatiotemporal functions. 
 Plus d'infos 

20171010  The complexity of graph query languages 
11:0012:00 178 
A graph database is a directed graph where each edge is additionally labeled with a symbol from a finite alphabet. Several data models, such as the ones occurring in the Semantic Web or semistructured data, can be naturally captured via graph databases. In this context, one is not only interested in traditional queries, such as conjunctive queries, but also in navigational queries that take the topology of the data into account.
In this talk, we consider one of the most prominent navigational query languages, namely, the class of conjunctive regular path queries (CRPQs). This class extends the class of conjunctive queries with the ability of checking the existence of a path between two nodes, whose label matches a given regular expression. As in the case of conjunctive queries, evaluating CRPQs is an NPcomplete problem. We present some results about tractable restrictions of CRPQs, as well as several open problems. 
 Plus d'infos 

20171003  Proof complexity of constraint satisfaction problems 
11:0012:00 178 
Many natural computational problems, such as satisfiability and systems of equations, can be expressed in a unified way as constraint satisfaction problems (CSPs). In this talk I will show that the usual reductions preserving the complexity of the constraint satisfaction problem preserve also its proof complexity. As an application, I will present two gap theorems, which say that CSPs that admit small size refutations in some classical proof systems are exactly the constraint satisfaction problems which can be solved by Datalog.
This is joint work with Albert Atserias. 
 Plus d'infos 

20170926  Which classes of origin graph are generated by transducers? 
11:0012:00 178 
This talk is about transductions, which are binary relations on words. We are interested in various models computing transductions (ie, transducers), namely twoway automata with outputs, streaming string transducers and stringtostring MSO transductions. We observe that each of these formalisms provides more than just a set of pairs of words. Indeed, one can also reconstruct origin information, which says how positions of the output string originate from positions of the input string. On the other hand, it is also possible to provide any pair of words in a relation with an origin mapping, indicating an origin input position for each output position, in a similar way. This defines a general object called origin graph. We first show that the origin semantic is natural and corresponds to the intuition we have of the run of a transducer, and is stable from translation from one model to another. We then characterise the families of origin graphs which corresponds to the semantics of streaming string transducers.
This is joint work with Mikolaj Bojanczyk, Laure Daviaud and Bruno Guillon, and has been published to ICALP17. 
 Plus d'infos 

20170704  SATbased Bounded Model Checking for 3Valued Abstractions  Part II 
11:0012:00 178 
Continuation of his precedent talk. 
 Plus d'infos 

20170627  SATbased Bounded Model Checking for 3Valued Abstractions 
11:0012:00 178 
In this talk I will present joint work with Nils Timm (and students) from the University of Pretoria on how to make modelchecking of concurrent systems more effective and more efficient. In the first part of the talk, which is based on our SBMF'16 paper, I show how bounded modelchecking over a threevalued truth domain {T:true, F:false, U:unknown} can be translated into a classical Boolean satisfiability problem which can then be given to any classical SAT solver. In the second part of the talk, which is based on our recent FSEN'17 paper, I speak about efficiencyincreasing heuristics which are based on the availability of structural knowledge about the original system to be modelchecked. On the basis of such structural knowledge the SAT solver can be guided into 'promising' search paths, whereby the probability of unnecessarily exploring fruitless paths is considerably diminished. The SBMF'16 paper was acknowledged as the "2ndbest paper of the conference", and the FSEN'17 paper was nominated among the "top three papers of the conference". 
 Plus d'infos 

20170613  Axiomatizations for downward XPath on Data Trees 
11:0012:00 178 
We give sound and complete axiomatizations for XPath with data tests by "equality" or "inequality", and containing the single "child" axis. This dataaware logic predicts over data trees, which are treelike structures whose every node contains a label from a finite alphabet and a data value from an infinite domain. The language allows us to compare data values of two nodes but cannot access the data values themselves (i.e., there is no comparison by constants).
Our axioms are in the style of equational logic, extending the axiomatization of dataoblivious XPath, by B. ten Cate, T. Litak and M. Marx. We axiomatize the full logic with tests by "equality" and "inequality", and also a simpler fragment with "equality" tests only. Our axiomatizations apply both to node expressions and path expressions. The proof of completeness relies on a novel normal form theorem for XPath with data tests. 
 Plus d'infos 

20170530  An efficient algorithm to decide the periodicity of brecognisable sets using MSDF convention 
11:0012:00 178 
Given an integer base b>1, a set of integers is represented in base b by a language over {0,1,...,b1}. The set is said brecognisable if its representation is a regular language. It is known that eventually periodic sets are brecognisable in every base b, and Cobham's theorem imply the converse: no other set is brecognisable in every base b.
We are interested in deciding whether a brecognisable set of integers (given as a finite automaton) is eventually periodic. Honkala showed in 1986 that this problem is decidable and recent developments give efficient decision algorithms. However, they only work when the integers are written with the least significant digit first.
In this work, we consider here the natural order of digits (Most Significant Digit First) and give a quasilinear algorithm to solve the problem in this case. 
 Plus d'infos 

20170523  A linear lower bound for incrementing a spaceoptimal integer representation in the bitprobe model 
11:0012:00 178 
We present the first linear lower bound for the number of bits required to be accessed in the worst case to increment an integer in an arbitrary spaceoptimal binary representation. The best previously known lower bound was logarithmic. It is known that a logarithmic number of read bits in the worst case is enough to increment some of the integer representations that use one bit of redundancy, therefore we show an exponential gap between spaceoptimal and redundant counters.
Our proof is based on considering the increment procedure for a space optimal counter as a permutation and calculating its parity. For every space optimal counter, the permutation must be odd, and implementing an odd permutation requires reading at least half the bits in the worst case. The combination of these two observations explains why the worstcase spaceoptimal problem is substantially different from both averagecase approach with constant expected number of reads and almost space optimal representations with logarithmic number of reads in the worst case.
https://arxiv.org/abs/1607.00242 ; ICALP 2017 
 Plus d'infos 

20170516  Proving safety of concurrent programs 
11:0012:00 178 
This talk will be based on the paper from POPL 2017:
Thread Modularity at Many Levels: a pearl of compositional verification
by
Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski
In the paper the authors consider the problem of proving safety of (parametrized) concurrent programs. They do not propose new techniques but rather revisit some existing ones. I have found putting these techniques next to each other very interesting and thought provoking. Since the considered problem is a fundamental problem for verification, I think it is worth to see this work at the seminar.
This will not be a survey talk. Technically the talk will be very easy, as the results are straightforward. The goal is to present a view point on the problem that I have got from reading the paper. 
 Plus d'infos 

20170509  WBTS: the new class of WSTS without WQO. 
11:0012:00 76 
We present the ideal framework [FG09a,BFM14] which was recently used to obtain new deep results on Petri nets and extensions. If time, we will present the proof of the famous but unknown ErdösTarski theorem. We argue that the theory of ideals prompts a renewal of the theory of WSTS by providing a way to define a new class of monotonic systems, the socalled Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm. 
 Plus d'infos 

20170425  On Reversible Transducers 
11:0012:00 178 
Deterministic twoway transducers define the robust class of regular functions which is, among other good properties, closed under composition.
However, the best known algorithms for composing twoway transducers cause a double exponential blowup in the size of the inputs.
We introduce a class of transducers for which the composition has polynomial complexity. It is the class of reversible transducers, for which the computation steps can be reversed deterministically.
While in the oneway setting this class is not very expressive, any twoway transducer can be made reversible through a single exponential blowup.
As a consequence, the composition of twoway transducers can be done with a single exponential blowup in the number of states.
A uniformization of a relation is a function with the same domain and which is included in the original relation.
Our main result actually states that we can uniformize any nondeterministic twoway transducer by a reversible transducer with a single exponential blowup, improving the known result by de Souza which has a quadruple exponential complexity.
As a side result, our construction also gives a quadratic transformation from copyless streaming string transducers to twoway transducers, improving the exponential previous bound. 
 Plus d'infos 

20170404  Automata theory and game semantics of higherorder computation 
11:0012:00 178 
I will give a survey of various classes of automata that have
been used to capture the game semantics of higherorder programs
and, consequently, obtain decidability results for contextual equivalence. 
 Plus d'infos 

20170328  Time domain (for time denotational semantics) 
11:0012:00 178 
Directed complete partial orders (cpos) are used in denotational semantics for describing the way each value is incrementally computed, passing from a completely unknown value to a completely known value. Then, continuous functions between cpos propagate increase of knowledge on their inputs to increase of knowledge on their outputs.
In this talk, we define the notion timed cpo by means of a cut function that tells what part of any value is known before any given instant. In the induced partial order, the increase of knowledge explicitly refers to the passage of time. It follows that continuous functions between timed cpos provide denotational semantics model candidates for timed IOsystem acting over (higherorder) time evolving values, e.g. timed streams, but also bounded below values, partial inductive structures, timed functions, etc.
Definitions, examples and (closure) properties of these timed cpos and their continuous functions are provided throughout. 
 Plus d'infos 

20170321  Learning probability measures 
11:0012:00 178 
Suppose we have a probabilistic algorithm given as a black box and we have access to an output of this algorithm. There are two  related  questions one could ask. (1) Is it possible to make a plausible guess as to which algorithm is in the box? (2) Can we use the output of this algorithm as a random number generator by extracting `pure’ randomness from it? We will look at these questions from the point of view of computability and algorithmic learning theory. [Based on joint work with S. Figueira, B. Monin, and A. Shen] 
 Plus d'infos 

20170314  On the decomposition of finitevalued streaming string transducers 
11:0012:00 178 
I will present some preliminary results towards a proof of a decomposition theorem for streaming string transducers (SSTs). Roughly, the conjectured decomposition theorem states that every SST that associates at most k outputs to each input can be effectively decomposed as a finite union of functional SSTs. Such a result would imply, among other things, the decidability of the equivalence problem for the considered class of transducers as well as a correspondence with the classical twoway transducers. I will present a proof of this decomposition theorem in the special case of SSTs with 1 register. The proof heavily relies on a combinatorial result by Kortelainen concerning word equations with iterated factors. 
 Plus d'infos 

20170307  Verifying properties of functional programs: from the deterministic to the probabilistic case 
11:0012:00 178 
In functional programs, also called higherorder programs, functions may take functions themselves as arguments. As a result, their modelchecking relies in most approaches on semantic or typetheoretic tools. In this talk, I will explain how an analysis based on linear logic of a modelchecking result of 2009 by Kobayashi and Ong led Melliès and I to the construction of a model for modelchecking. This model is such that, when interpreting a term with recursion representing the tree of traces of a functional program, its denotation determines whether it satisfies a MSO property of interest. A related and similar model was obtained independently by Salvati and Walukiewicz.
In the second part of the talk, I will discuss the verification of termination for functional programs with recursion and probabilistic choice. Dal Lago and I defined recently a type system which is such that typable programs terminate with probability 1. In other terms, their set of diverging executions is negligible. If time allows, I will sketch ideas towards an extension of the modelchecking results of the deterministic case to quantitative logics and functional programs with recursion. 
 Plus d'infos 

20170228  Digital Currencies 
11:0012:00 178 
Electronic money is a quite old problem in cryptology (Chaum, 1982) but recent discoveries lead to the birth of a new type of digital currency such as Bitcoins or Ethereum. Most of the new cryptocurrencies are based on the concept of Blockchain which is used to maintain a trusted consensus in a distributed manner thanks to cryptographic primitives.
This talk will summarize the main concepts and mechanisms used to ensure the security of Bitcoins and Blockchain. 
 Plus d'infos 

20170214  Emptiness of nonzero automata is decidable 
11:0012:00 178 
Zero automata are a probabilistic extension of parity automata on infinite trees.
Bojanczyk has shown recently that the satisfiability of a certain probabilistic variant of MSO, called TMSO+zero reduces to the emptiness problem for zero automata.
These automata perform random walks on the input (binary) tree: when the automaton is in a state q on a node labelled with a, it selects nondeterministically a transition (q,a,r_0,r_1) and moves with equal probability 1/2 either to the left node in state r_0 or to the right node in state r_1..
The acceptance condition of zero automata impose conditions not only on the parity of individual branches of the run but as well on some other properties of runs that should occur almostsurely or with positive probability.
We introduce a variant of zero automata called nonzero automata and we show that i) for every zero automaton there is an equivalent nonzero automaton of quadratic size ii) the emptiness problem of nonzero automata is decidable, with complexity {sc np}. These results imply that TMSO+zero has decidable satisfiability.
Joint work with Mikolaj Danger Bojanczyk and Edon Kelmendi 
 Plus d'infos 

20170124  Faster algorithms for program analysis 
11:0012:00 178 
The talk is based on joint work with Krishnendu Chatterjee, Amir Kafshdar Goharshady, Prateesh Goyal, and Andreas Pavlogiannis.
The talk is about solving graph problems (focusing on graph problems that are often reduced to in program analysis) faster when the graphs are composed of control flow graphs of methods in programs. Using that control flow graphs of methods typically have constant treewidth we consider when the program either (i) has a single method, (ii) has many methods, or (iii) concurrent threads, each on a single method. For cases (ii) and (iii), we consider the Algebraic Path Problem (APP), which is a very general problem, with many interesting special cases, such as (1) reachability and shortest path (with positive and negative weights), (2) the IDE/IDFS frameworks of program analysis and (3) most probable path. Since APP has already been optimally solved for single methods/constant treewidth graphs, up to factors of log^* n (n is the number of states), in (i), if time permits, we will consider other weighted graph problems that has been reduced to in program analysis (but which are not special cases of APP), specifically finding the cycle with the least mean of weights (the minimum meanpayoff problem) and for a given start node v, finding the minimum number c and a path from v where all prefix sums of the weights of the path are greater than c (the minimum initial credit problem). In all cases, we give simple algorithms which are faster than the stateoftheart in theory and practice.
The talk is based on my POPL papers from 2015 and 2016, and, if time permits, my CAV paper from 2015 (see e.g. my homepage at http://rasmus.ibsenjensen.com for the papers). No prior specialised knowledge is necessary to follow the talk. 
 Plus d'infos 

20170110  Why liveness for timed automata is hard, and what we can do about it 
11:0012:00 178 
The liveness problem for timed automata asks if a given automaton has an infinite run visiting an accepting state infinitely often. In this talk, we will show that if P is not equal to NP, the liveness problem is "more difficult" than the reachability problem  more precisely, we will exhibit a family of automata for which reachability is in P whereas liveness is NPhard. We will then present a new algorithm to solve the liveness problem, and compare it with existing solutions.
Joint work with F. Herbreteau, T.T. Tran and I. Walukiewicz. 
 Plus d'infos 

20161213  Sound negotiations and static analysis 
11:0012:00 178 
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. Welldesigned 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 PSPACEcomplete, and in PTIME for deterministic negotiations. They also considered an intermediate subclass of nondeterministic 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 nondeterministic negotiations is in PTIME, and that checking soundness is already NPcomplete 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 
 Plus d'infos 

20161201  Translating LTL to Probabilistic Automata 
11:0012:00 76 
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 
 Plus d'infos 

20161129  Deciding semantic finiteness of firstorder grammars w.r.t. bisimulation equivalence 
11:0012:00 178 
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 firstorder grammars (that encompass pushdown automata)
w.r.t. bisimulation equivalence relies on the decidability of bisimulation equivalence (which was first proven by Senizergues).

 Plus d'infos 

20161122  Subword Based Abstractions of Formal Languages 
11:0012:00 178 
A successful idea in the area of verification is to consider finitestate abstractions of infinitestate 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 finitestate systems, which are much easier to handle.
While Parikhstyle 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 wellknown 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. 
 Plus d'infos 

20161115  Systems with Parametric Thread Creation 
11:0012:00 178 
We consider multithreaded systems which combine recursion, or even higherorder 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 subthreads. Reading and writing are atomic operations, while we do not allow locks or operations of the type compareandset. 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. 
 Plus d'infos 

20161108  Parameterized verification of networks of many identical processes 
11:0012:00 178 
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 twoplayer 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 nondeterminism 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 NPcomplete. 
 Plus d'infos 

20161025  Semantics models for timed programing languages 
11:0012:00 178 
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 presynchronous 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) IOautomaton can be associated to every causal functions, providing thus a clear operation (latest) semantics. Open perspectives or questions will conclude this presentation. 
 Plus d'infos 

20161018  Humanoid robotics and motion abstractions 
11:0012:00 178 
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. 
 Plus d'infos 

20161011  Walking the Boundary Between Tractability and Intractability 
11:0012:00 178 
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 templaterestricted constraint satisfaction problem and variants thereof; and, work on model checking firstorder logic with respect to different classes of sentences. 
 Plus d'infos 

20161004  Evaluations de requêtes au moyen d'automates programmés (Query evaluations by flyautomata) 
11:0012:00 178 
Les formules de la logique du secondordre monadique définissent des ensembles de puplets 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. 
 Plus d'infos 

20160712  Non commutative booléen algebras 
11:0012:00 76 
I shall explain what the title of the talk means and hint at connections with multiple valued logic. 
 Plus d'infos 

20160705  Doubleexponential and tripleexponential bounds for choosability problems parameterized by treewidth 
11:0012:00 178 
Choosability, introduced by Erdos, Rubin, and Taylor [Congr. Number. 1979], is a wellstudied 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 3choosability 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 doubleexponential 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 ExponentialTime Hypothesis (ETH).
We consider also the optimization problem where the task is to delete the minimum number of vertices to make the graph 4choosable and demonstrate that dependence on treewidth becomes tripleexponential 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 graphtheoretic problems that require doubleexponential or tripleexponential dependence on treewidth.
Joint work with Dániel Marx. 
 Plus d'infos 

20160628  Nesting Depth of Operators in Graph DatabaseQueries: Expressiveness vs. Evaluation Complexity 
11:0012:00 178 
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 NPcomplete. 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 PSPACEcomplete. 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** 
 Plus d'infos 

20160607  Data Communicating Processes with Unreliable Channels 
11:0012:00 salle 178 
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 boundedphase 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. 
 Plus d'infos 

20160531  The Complexity of Allswitches Strategy Improvement 
11:0012:00 76 
We study allswitches strategy improvement algorithms for parity, meanpayoff, discountedpayoff, 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 PSPACEcomplete to decide the following problems: (1) given an edge e, will allswitches strategy improvement ever switch e? (2) given an edge e, is e in the optimal strategy found by allswitches strategy improvement? 
 Plus d'infos 

20160518  Regular Abstractions of One Counter Languages 
11:0012:00 salle 75 
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 Parikhimage is the Parikhimage 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). 
 Plus d'infos 

20160510  Deciding Maxmin Reachability in HalfBlind Stochastic Games 
11:0012:00 76 
Twoplayer, turnbased, 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 1epsilon. This problem is undecidable in general, but we define a class of games, called leaktight halfblind 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 infinitememory. 
 Plus d'infos 

20160503  Semantic acyclicity of conjunctive queries 
11:0012:00 76 
The evaluation problem for Conjunctive Queries (CQ) is known to be NPcomplete in combined complexity and W[1]complete in parameterized complexity. However, acyclic CQs and more generally CQs of bounded treewidth can be evaluated in polynomial time in combined complexity and they are fixedparameter tractable.
We study the problem of whether a CQ can be rewritten into an equivalent CQ of bounded treewidth, 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. 
 Plus d'infos 

20160419  Reachability in TwoDimensional Unary Vector Addition Systems with States is NLComplete 
11:0012:00 76 
Blondin et al. showed at LICS 2015 that twodimensional 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 guessandverify 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 pseudopolynomial length always exist. Hence, when the input vectors are given in unary, the improved guessandverify algorithm requires only logarithmic space.
Joint work with Matthias Englert and Patrick Totzke, available from: http://arxiv.org/abs/1602.00477 
 Plus d'infos 

20160414  The Logic of Counting Query Answers: A Study via Existential Positive Queries 
11:0012:00 Salle 76 
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 firstorder 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 socalled #sentence on a structure yields an integer, as opposed to just a propositional value (true or false) as in usual firstorder 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). 
 Plus d'infos 

20160412  One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries 
11:0012:00 76 
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 graphtheoretic 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 graphtheoretic 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 wellknown 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 quantifierfree reductions. We obtain a significantly refined complexity classification of lefthand side restricted homomorphism problems, as well as a unifying, modular, and conceptually clean treatment of existing complexity classifications, such as the classifications by GroheSchwentickSegoufin (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 CSLLICS ’14. 
 Plus d'infos 

20160405  Towards an algebraic theory of rational word functions 
11:0012:00 76 
In formal language theory, several different models characterize regular languages, such as finite automata, congruences of finite index, or monadic secondorder 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 oneway 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 oneway transducer. 
 Plus d'infos 

20160329  Programmation réactive par tuilage 
11:0012:00 76 
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 
 Plus d'infos 

20160322  For graphs of bounded tree width, recognisability equals definability in MSO. 
14:1516:00 75 
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 constantwidth 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 treewidth at most k. One of the ingredients is the Factorisation Forest Theorem of Imre Simon. 
 Plus d'infos 

20160308  The Complexity of Coverability in nuPetri Nets 
11:0012:00 76 
We show that the coverability problem in nuPetri nets is complete for 'double Ackermann' time, thus closing an open complexity gap between an Ackermann lower bound and a hyperAckermann 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 nuPetri 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 wellquasiorder ideals.
Joint work with Ranko Lazic, preprint available from https://hal.inria.fr/hal01265302. 
 Plus d'infos 

20160301  Reasoning about distributed systems: WYSIWYG 
11:0012:00 76 
There are two schools of thought on reasoning about distributed systems: one following interleaving based semantics, and one following partialorder/graph based semantics. We will compare these two approaches and argues in favour of the latter. An introductory treatment of tree automata techniques (via splitwidth) to reason about distributed systems is also provided. 
 Plus d'infos 

20160216  Sensing cost for automata and synthesis 
11:0012:00 76 
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 minimallysensing 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. 
 Plus d'infos 

20160209  A Generalised Twinning Property for Minimisation of Cost Register Automata. 
11:0012:00 76 
Weighted automata extend finitestate 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 finitestate 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 kbounded 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 finitevalued finitestate 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 PierreAlain Reynier and JeanMarc Talbot. 
 Plus d'infos 

20160202  A Class of Zielonka Automata with a Decidable Controller Synthesis Problem 
11:0012:00 76 
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 seriesparallel, 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. 
 Plus d'infos 

20160112  The language complexity of solutions of equations in free semigroups and free groups 
11:0012:00 76 
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. 
 Plus d'infos 

Liste des événements répétitifs du groupe Séminaire Méthodes Formelles
RetourRetour à l'index
 