Liste des événements uniques du groupe Séminaire Méthodes Formelles


2018-02-27TBA
11:00-12:00
178
TBA
 Plus d'infos  


2018-02-13TBA
11:00-12:00
178
TBA
 Plus d'infos  


2018-01-16TBA
11:00-12:00
178
TBA
 Plus d'infos  


2018-01-09TBA
11:00-12:00
178
TBA
 Plus d'infos  


2017-12-12La coloration de graphe dans le modèle LOCAL - Partie II
11:00-12: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  


2017-12-05La coloration de graphe dans le modèle LOCAL - Partie I
11:00-12: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 3-coloration des n-cycles 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 1-orientations en 6 couleurs
- De 6 à 3 couleurs
- Cas des graphes arbitraires
 Plus d'infos  


2017-11-28Succinct progress measures and solving parity games in quasi-polynomial time
11:00-12: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 quasi-polynomial time, where previously the best algorithms were mildly sub-exponential. We devise an alternative quasi-polynomial time algorithm based on progress measures, which allows us to reduce the space required from quasi-polynomial 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 multi-counters, 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 computer-aided 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  


2017-11-21Model Checking: the Interval Way
11:00-12:00
178
Model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based 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 "point-wise" describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted "interval-wise" 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 well-known 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 non-elementarily decidable and EXPSPACE-hard 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  


2017-11-14Reunion d'equipe MF
11:00-12:00
178
 Plus d'infos  


2017-11-07Formal methods for capturing dynamics of biological networks
11:00-12: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  


2017-10-31Rewriting Higher-order Stack Trees
11:00-12:00
178
Higher-order 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 higher-order stack operations and ground tree rewriting. We introduce a model of higher-order ground tree rewriting over trees labelled by higher-order stacks (henceforth called stack trees), which syntactically coincides with ordinary ground tree rewriting at order 1 and with the dynamics of higher-order 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 first-order 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  


2017-10-24Constructive completeness for the linear-time mu-calculus
11:00-12:00
178
Modal mu-calculus 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 linear-time case and by Walukiewicz for the branching-time one. These proofs are based on complex, non-constructive 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 linear-time mu-calculus 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 mu-calculus and automata theory. More precisely, we lift the well-known automata transformations (non-determinization for instance) to the logical level. To solve each of these smaller problems, we perform first a proof-search 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 linear-time mu-calculus.
 Plus d'infos  


2017-10-17 Timed domains: an appetizer
11:00-12: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 spatio-temporal functions.
 Plus d'infos  


2017-10-10The complexity of graph query languages
11:00-12: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 semi-structured 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 NP-complete problem. We present some results about tractable restrictions of CRPQs, as well as several open problems.
 Plus d'infos  


2017-10-03Proof complexity of constraint satisfaction problems
11:00-12: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  


2017-09-26Which classes of origin graph are generated by transducers?
11:00-12:00
178
This talk is about transductions, which are binary relations on words. We are interested in various models computing transductions (ie, transducers), namely two-way automata with outputs, streaming string transducers and string-to-string 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  


2017-07-04SAT-based Bounded Model Checking for 3-Valued Abstractions - Part II
11:00-12:00
178
Continuation of his precedent talk.
 Plus d'infos  


2017-06-27SAT-based Bounded Model Checking for 3-Valued Abstractions
11:00-12:00
178
In this talk I will present joint work with Nils Timm (and students) from the University of Pretoria on how to make model-checking 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 model-checking over a three-valued 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 efficiency-increasing heuristics which are based on the availability of structural knowledge about the original system to be model-checked. 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 "2nd-best paper of the conference", and the FSEN'17 paper was nominated among the "top three papers of the conference".
 Plus d'infos  


2017-06-13Axiomatizations for downward XPath on Data Trees
11:00-12:00
178
We give sound and complete axiomatizations for XPath with data tests by "equality" or "inequality", and containing the single "child" axis. This data-aware logic predicts over data trees, which are tree-like 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 data-oblivious 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  


2017-05-30An efficient algorithm to decide the periodicity of b-recognisable sets using MSDF convention
11:00-12:00
178
Given an integer base b>1, a set of integers is represented in base b by a language over {0,1,...,b-1}. The set is said b-recognisable if its representation is a regular language. It is known that eventually periodic sets are b-recognisable in every base b, and Cobham's theorem imply the converse: no other set is b-recognisable in every base b.

We are interested in deciding whether a b-recognisable 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 quasi-linear algorithm to solve the problem in this case.
 Plus d'infos  


2017-05-23A linear lower bound for incrementing a space-optimal integer representation in the bit-probe model
11:00-12: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 space-optimal 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 space-optimal 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 worst-case space-optimal problem is substantially different from both average-case 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  


2017-05-16Proving safety of concurrent programs
11:00-12: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  


2017-05-09WBTS: the new class of WSTS without WQO.
11:00-12: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ös-Tarski 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 so-called Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm.
 Plus d'infos  


2017-04-25On Reversible Transducers
11:00-12:00
178
Deterministic two-way transducers define the robust class of regular functions which is, among other good properties, closed under composition.
However, the best known algorithms for composing two-way transducers cause a double exponential blow-up 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 one-way setting this class is not very expressive, any two-way transducer can be made reversible through a single exponential blow-up.
As a consequence, the composition of two-way transducers can be done with a single exponential blow-up 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 non-deterministic two-way transducer by a reversible transducer with a single exponential blow-up, 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 two-way transducers, improving the exponential previous bound.
 Plus d'infos  


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


2017-03-28Time domain (for time denotational semantics)
11:00-12: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 IO-system acting over (higher-order) 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  


2017-03-21Learning probability measures
11:00-12: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  


2017-03-14On the decomposition of finite-valued streaming string transducers
11:00-12: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 two-way 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  


2017-03-07Verifying properties of functional programs: from the deterministic to the probabilistic case
11:00-12:00
178
In functional programs, also called higher-order programs, functions may take functions themselves as arguments. As a result, their model-checking relies in most approaches on semantic or type-theoretic tools. In this talk, I will explain how an analysis based on linear logic of a model-checking result of 2009 by Kobayashi and Ong led Melliès and I to the construction of a model for model-checking. 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 model-checking results of the deterministic case to quantitative logics and functional programs with recursion.
 Plus d'infos  


2017-02-28Digital Currencies
11:00-12: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 crypto-currencies 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  


2017-02-14Emptiness of nonzero automata is decidable
11:00-12: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 non-deterministically 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 almost-surely 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  


2017-01-24Faster algorithms for program analysis
11:00-12: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 tree-width 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 tree-width 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 mean-payoff 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 state-of-the-art 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.ibsen-jensen.com for the papers). No prior specialised knowledge is necessary to follow the talk.
 Plus d'infos  


2017-01-10Why liveness for timed automata is hard, and what we can do about it
11:00-12: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 NP-hard. 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  


2016-12-13Sound negotiations and static analysis
11:00-12: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. 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
 Plus d'infos  


2016-12-01Translating LTL to Probabilistic Automata
11:00-12: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  


2016-11-29Deciding semantic finiteness of first-order grammars w.r.t. bisimulation equivalence
11:00-12: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 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).
 Plus d'infos  


2016-11-22Subword Based Abstractions of Formal Languages
11:00-12:00
178
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.
 Plus d'infos  


2016-11-15Systems with Parametric Thread Creation
11:00-12:00
178
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.
 Plus d'infos  


2016-11-08Parameterized verification of networks of many identical processes
11:00-12: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 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.
 Plus d'infos  


2016-10-25Semantics models for timed programing languages
11:00-12: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 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.
 Plus d'infos  


2016-10-18Humanoid robotics and motion abstractions
11:00-12: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  


2016-10-11Walking the Boundary Between Tractability and Intractability
11:00-12: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 template-restricted constraint satisfaction problem and variants thereof; and, work on model checking first-order logic with respect to different classes of sentences.
 Plus d'infos  


2016-10-04Evaluations de requêtes au moyen d'automates programmés (Query evaluations by fly-automata)
11:00-12:00
178
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.
 Plus d'infos  


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


2016-07-05Double-exponential and triple-exponential bounds for choosability problems parameterized by treewidth
11:00-12:00
178
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.
 Plus d'infos  


2016-06-28Nesting Depth of Operators in Graph DatabaseQueries: Expressiveness vs. Evaluation Complexity
11:00-12: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 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**
 Plus d'infos  


2016-06-07Data Communicating Processes with Unreliable Channels
11:00-12: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 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.
 Plus d'infos  


2016-05-31The Complexity of All-switches Strategy Improvement
11:00-12:00
76
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?
 Plus d'infos  


2016-05-18Regular Abstractions of One Counter Languages
11:00-12: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 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).
 Plus d'infos  


2016-05-10Deciding Maxmin Reachability in Half-Blind Stochastic Games
11:00-12:00
76
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.
 Plus d'infos  


2016-05-03Semantic acyclicity of conjunctive queries
11:00-12:00
76
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.
 Plus d'infos  


2016-04-19Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete
11:00-12:00
76
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
 Plus d'infos  


2016-04-14The Logic of Counting Query Answers: A Study via Existential Positive Queries
11:00-12: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 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).
 Plus d'infos  


2016-04-12One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries
11:00-12: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 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.
 Plus d'infos  


2016-04-05Towards an algebraic theory of rational word functions
11:00-12:00
76
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.
 Plus d'infos  


2016-03-29Programmation réactive par tuilage
11:00-12: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  


2016-03-22For graphs of bounded tree width, recognisability equals definability in MSO.
14:15-16: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 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.
 Plus d'infos  


2016-03-08The Complexity of Coverability in nu-Petri Nets
11:00-12:00
76
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.
 Plus d'infos  


2016-03-01Reasoning about distributed systems: WYSIWYG
11:00-12:00
76
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.
 Plus d'infos  


2016-02-16Sensing cost for automata and synthesis
11:00-12: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 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.
 Plus d'infos  


2016-02-09A Generalised Twinning Property for Minimisation of Cost Register Automata.
11:00-12:00
76
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.
 Plus d'infos  


2016-02-02A Class of Zielonka Automata with a Decidable Controller Synthesis Problem
11:00-12: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 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.
 Plus d'infos  


2016-01-12The language complexity of solutions of equations in free semigroups and free groups
11:00-12: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




Retour
Retour à l'index