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

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

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

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


Prochains exposés

DateOrateurTitre



Précédents exposés depuis janvier 2017

DateOrateurTitre
mardi 03 juillet 2018Filip Murlak (University of Warsaw) Ontology-mediated query answering for expressive description logics, or yet another family of (potentially) decidable fragments of first-order logic
Evaluating queries in the presence of background knowledge has been extensively studied in several communities. In database theory, it is known as query answering under integrity constraints: given a finite database instance and a set of constraints, determine answers to a query that are certain to hold over any extension of the given instance that satisfies the constraints. In the knowledge representation community, the database instance and the set of constraints are treated as a single object, called an ontology, but otherwise the problem remains the same, except that different kinds of constraints are interesting. While in database theory constraints are usually very simple, like functionality of relations, or inclusions between relations, in knowledge representation more expressive logics are used. I will focus on so called description logics, which are a family of extensions of modal logic. I will cover some basic techniques, a highly non-trivial result by Rudolph and Glimm (2010), as well as some recent results obtained with Tomek Gogacz (U Warsaw) and Yazmin Ibanez-Garcia (TU Wien).
mardi 26 juin 2018Sébastien Labbé (LaBRI) On Jeandel-Rao aperiodic tilings
In 2015, Jeandel and Rao showed by exhaustive computer search that every Wang tile set of cardinality <=10 either admit a periodic tiling of the plane or admit no tiling of the plane at all. Moreover, they found a Wang tile set of cardinality 11 which admits tilings of the plane but never periodically. Their algorithm is based on the representation of Wang tilings as the execution of a transducer on biinfinite sequences. In this talk, we present an alternate definition of the aperiodic tilings of Jeandel-Rao as the coding of a $mathbb{Z}^2$-action on the torus. We conjecture that it is a complete characterization.
mardi 19 juin 2018František Blahoudek (Masaryk University) Semi-deterministic automata: How to obtain and complement them
Semi-deterministic Büchi automata (sDBA) are useful for example in model checking of probabilistic systems or in termination analysis. While in probabilistic model checking sDBA represent the set of behaviours of interest, in termination analysis they represent terminating behaviours of programs and are often complemented to perform a language difference. In my talk, I first introduce the class of semi-deterministic Büchi automata (sDBA). Then I will explain how can we convert nondeterministic Büchi automata (NBA) into sDBA, followed by a discussion on how to efficiently convert generalized Büchi automata into sDBA. After we learn how to build sDBA, I will introduce a complementation algorithm sDBA. The algorithm produces a complement automata with at most 4^n states while the best upper bound on complementation of NBA is O((0.76n)^n). Further, our algorithm produces automata with a very low degree of nondeterminism, indeed, the resulting automata are even unambiguous.
mardi 12 juin 2018Bruno Guillon (University of Milan) Undecidability of MSO+“ultimately periodic”
We prove that MSO on omega-words becomes undecidable if allowing to quantify over sets of positions that are ultimately periodic, i.e., sets X such that for some positive integer p, ultimately either both or none of positions x and x+p belong to X. We obtain it as a corollary of the undecidability of MSO on omega-words extended with the second-order predicate U1(X) which says that the distance between consecutive positions in a set X of naturals is unbounded. This is achieved by showing that adding U1 to MSO gives a logic with the same expressive power as MSO+U, a logic on omega-words with undecidable satisfiability. This is joint work with Mikolaj Bojanczyk, Laure Daviaud, Vincent Penelle and Sreejith.
mardi 05 juin 2018Laure Daviaud (University of Warwick) A pseudo-quasi-polynomial algorithm for mean-payoff parity games
In a mean-payoff parity game, one of the two players aims both to achieve a qualitative parity objective and to minimize a quantitative long-term average of payoffs (aka. mean payoff). The game is zerosum and hence the aim of the other player is to either foil the parity objective or to maximize the mean payoff. I will present a pseudo-quasi-polynomial algorithm for solving mean-payoff parity games. All algorithms for the problem that have been developed for over a decade have a pseudo-polynomial and an exponential factors in their running times; in the running time of our algorithm the latter is replaced with a quasi-polynomial one.
mardi 22 mai 2018K. Narayan Kumar (Chennai Mathematical Institute) Verification of Asynchronous Programs with Nested Locks
We consider asynchronous programs consisting of multiple recursive threads (modeled as pushdown systems) running in parallel. Each of the threads is equipped with a multi-set. The threads can create tasks and post them onto the multi-sets or read a task from their own. In addition, they can synchronize through a finite set of locks. We examine the decidability of the state reachability problem for this model. The problem is already known to be undecidable for a system consisting of two recursive threads (and no tasks) and we examine a decidable subclass. In the first half of the talk we survey, quickly, the previous results for recursive programs communicating via locks and in the second half we will describe our results on the asynchronous program model. Based on Joint work with M.F. Atig, A. Bouajjani and P. Saivasan.
mardi 15 mai 2018Madhavan Mukund (Chennai Mathematical Institut) Modelling replicated data stores with multiple correctness levels
Replicated data stores typically sacrifice strong consistency guarantees in favour of availability and partition tolerance. These data stores usually provide specific weaker consistency guarantees, such as eventual consistency, monotonic reads or causal consistency. Recently, there have been proposals for data stores that support multiple consistency guarantees. An example is a speculative response based on a quick local check, followed by either a confirmation or an "apology" after a more detailed reconciliation of updates. A typical situation is an online purchase where the order is initially confirmed and later you are told the item is out of stock. We describe a formal semantics for replicated data-stores with multiple correctness levels and explore decidability issues. This is ongoing joint work with Ahmed Bouajjani, Constantin Enea, Gautham Shenoy R and S P Suresh.
mardi 24 avril 2018Armin Weiß (Stuttgart University) The isomorphism problem for virtually free group
Since Muller and Schupp's result it is well-known that the finitely generated virtually free groups are precisely the context-free groups. The isomorphism problem for virtually free groups, has shown to be decidable by Kristic. In the special case that the input groups are either given as context-free grammars for their word problems or as so-called virtually free presentations, it is primitive recursive by the work of Sénizergues. In this talk I will present an elementary time solution for these two special cases. The proof is based on analyzing the structure trees assigned to the Cayley graphs of the input groups. By Bass-Serre theory this yields graphs of groups which can be tested for isomorphism as in Kristic's algorithm. The talk is based on joint work with Géraud Sénizergues and Volker Diekert.
mardi 17 avril 2018Pierre Ohlmann (IRIF, Paris 7) Arithmetic circuits as automata, and applications
We give a syntactic correspondence between non-associative arithmetic circuits and acyclic weighted tree automata. We may then export results from automata theory to non-associative circuits and characterize the size of a minimal circuit for a given polynomial as the rank of a Hankel matrix. We will then show how this can be used to re-obtain Nisan's theorem on Algebraic Branching Programs as well as recent results on Unique Parse Tree circuits. Lastly, we will highlight a new way of obtaining lower bounds for general (associative) arithmetic circuits.
mardi 10 avril 2018Nathanaël Fijalkow (LaBRI) The State Complexity of Alternating Automata
We study the complexity of languages of finite words using automata theory. To go beyond the class of regular languages, we consider infinite automata and the notion of state complexity defined by Karp. We look at alternating automata as introduced by Chandra, Kozen and Stockmeyer: such machines run independent computations on the word and gather their answers through boolean combinations. We devise a lower bound technique relying on boundedly generated lattices of languages, and give two applications of this technique. The first is a hierarchy theorem, stating that there are languages of arbitrarily high polynomial alternating state complexity, and the second is a linear lower bound on the alternating state complexity of the prime numbers written in binary. This second result strengthens a result of Hartmanis and Shank from 1968, which implies an exponentially worse lower bound for the same model. To be presented at LICS'18.
mardi 03 avril 2018Louis-Marie Dando (LaBRI) On Rotating Q-Automata
I present results on rotating Q-automata, which are (memoryless) automata with weights in Q that can read the input tape from left to right several times. We show that the series realized by valid rotating Q-automata are Q-Hadamard series (which are the closure of Q-rational series by pointwise inverse), and that every Q-Hadamard series can be realized by such an automaton. We prove that, although validity of rotating Q-automata is undecidable, the equivalence problem is decidable on rotating Q-automata. Finally, we prove that every valid two-way Q -automaton admits an equivalent rotating Q-automaton. The conversion, which is effective, implies the decidability of equivalence of two-way Q-automata.
mardi 27 mars 2018Valia Mitsou (Université Paris Diderot, IRIF) Limitations of treewidth for problems beyond NP.
***Joint seminar with Graphes et Optimisation*** In this seminar, we will take a closer look at the parameterized complexity of existsforallSAT, the prototypical complete problem of the class $Sigma^p_2$, the second level of the polynomial hierarchy. We will provide tight fine-grained bounds on the complexity of this problem with respect to the most important structural graph parameters. Specifically we will show that existsforallSAT cannot be solved in time $2^{2^{o(tw)}}$ under the Exponential Time Hypothesis. More strongly, we establish the same bound with respect to the formula’s primal vertex cover, a much more restrictive measure. Our reduction is a 'textbook' reduction that could be used in order to provide similar lower bounds for problems in the second level of the polynomial hierarchy.
mardi 20 mars 2018Dominik Velan (Masaryk University) Asymptotic Bounds on Termination Time in VASS
Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parametrized systems, and are also used as abstract models of programs in resource bound analysis. We study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obtaining polynomial bounds on termination time. First, I will present a characterization for VASS with linear asymptotic complexity. I will also show that if a complexity of a VASS is not linear, it is at least quadratic. Second, I will talk about classification of VASS according to quantitative properties of their cycles. I will show that certain singularities in these properties are the key reason for their non-polynomial asymptotic complexity. In absence of singularities, I will show that the asymptotic complexity is always polynomial and of the form Theta(n^k), for some integer k <= d. I will present a polynomial-time algorithm computing the integer k. The results are based on insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis.
mardi 13 mars 2018Jérôme Leroux (LaBRI) Polynomial Vector Addition Systems With States
The reachability problem for vector addition systems is one of the most difficult and central problem in theoretical computer science. The problem is known to be decidable, but despite instance investigations during the last four decades, the exact complexity is still open. For some sub-classes, the complexity of the reachability problem is known. Structurally bounded vector addition systems, the class of vector addition systems with finite reachability sets from any initial configuration, is one of those classes. In fact, the reachability problem was shown to be polynomial-space complete for that class by Praveen and Lodaya in 2008. Surprisingly, extending this property to vector addition systems with states is open. In fact, there exist vector addition systems with states that are structurally bounded but with Ackermannian large sets of reachable configurations. It follows that the reachability problem for that class is between exponential space and Ackermannian. In this paper we introduce the class of polynomial vector addition systems with states, defined as the class of vector addition systems with states with size of reachable configurations bounded polynomially in the size of the initial ones. We prove that the reachability problem for polynomial vector addition systems is exponential-space complete. Additionally, we show that we can decide in polynomial time if a vector addition system with states is polynomial. This characterization introduces the notion of iteration scheme with potential applications to the reachability problem for general vector addition systems.
mardi 06 mars 2018Pierre Casteran (LaBRI) The hydra and the rooster
The Hydra game was introduced in 1982 by the mathematicians L. Kirby and J. Paris in their article: "Accessible Independence Results for Peano Arithmetic". This article contains two theorems: 1. Whichever the strategy of Hercules and the Hydra, any battle eventually terminates with Hercules' victory. 2. The previous result cannot be proved in Peano Arithmetic. We present a formal, self-contained (axiom-free) proof of a variant of both theorems, with the help of the Coq proof assistant. Since Coq's logic is higher-order intuitionnistic logic, the reference to Peano Arithmetic is replaced with a study of a class of proofs of termination indexed by ordinal numbers less or equal than epsilon_0. We present the main parts of this proof, as well as the main features of Coq that made its construction possible.
mardi 27 février 2018María Emilia Descotte (LaBRI) Resynchronizing Classes of Word Relations
A natural approach to defining binary word relations over a finite alphabet A is through two-tape finite state automata, which can be seen as regular languages L over the alphabet {1,2}xA, where (i,a) is interpreted as reading letter a from tape i. Thus, a word w of the language L denotes the pair (u_1,u_2) in A* x A* in which u_i is the projection of w onto i-labelled letters. While this formalism defines the well-studied class of Rational relations (a.k.a. non-deterministic finite state transducers), enforcing restrictions on the reading regime from the tapes, that we call synchronization, yields various sub-classes of relations. Such synchronization restrictions are imposed through regular properties on the projection of the language onto {1,2}. In this way, for each regular language C contained in {1,2}*, one obtains a class Rel(C) of relations, such as the classes of Regular, Recognizable, or length-preserving relations, as well as (infinitely) many other classes. We study the problem of containment for synchronized classes of relations: given C,D sub-languages of {1,2}*, is Rel(C) contained in Rel(D)? We show a characterization in terms of C and D which gives a decidability procedure to test for class inclusion. This also yields a procedure to re-synchronize languages from {1,2}xA preserving the denoted relation whenever the inclusion holds.
mardi 13 février 2018Michael Raskin (LaBRI) Complementing the languages of unambigous automata
Unambiguous non-deterministic finite automata have intermediate expressive power and succinctness between deterministic and non-deterministic automata. It has been conjectured that every unambiguous non-deterministic one-way finite automaton (1UFA) recognizing some language L can be converted into a 1UFA recognizing the complement of the original language L with polynomial increase in the number of states. A counterexample to this conjecture using only the 1-letter alphabet will be presented.
mardi 06 février 2018Lukas Fleischer (Stuttgart University) The Complexity of Decision Problems for Recognizing Morphisms
We discuss the complexity of decision problems on regular languages represented by morphisms to finite semigroups. There are two canonical ways of specifying the semigroup: giving its multiplication table or an implicit description as the subsemigroup of a transformation semigroup (generated by the images of the given morphism). For both representations, we will consider * the membership problem, * the emptiness/universality/inclusion/equivalence problems, * the intersection non-emptiness problem, and their restrictions to a certain classes of finite semigroups. Complexity results and open problems will be presented.
mardi 30 janvier 2018David Janin (LaBRI) Animation 3D et produit semi-direct
We define a simple and sound mathematical framework for describing temporal media programming language semantics based on the various concepts offered by semigroup theory. As a result a fairly general programming scheme can be defined in order to specify, compose and render both spatial media objects (e.g. 3D drawings) and timed media objects (e.g. Animation or Music). As an example, a simple monoid based semantics model of the turtle command language of Logo is detailed and extended throughout. Joint work with Simon Archipoff
mardi 23 janvier 2018Filip Mazowiecki (LaBRI) Pumping lemmas for weighted automata
We present three pumping lemmas for three classes of functions definable by fragments of weighted automata over the min-plus semiring and the semiring of natural numbers. As a corollary we show that the hierarchy of functions definable by unambiguous, finitely-ambiguous, polynomially-ambiguous weighted automata, and the full class of weighted automata is strict for the min-plus semiring. This is joint work with Cristian Riveros to be presented at stacs 2018.
mardi 09 janvier 2018Philippe Duchon (LaBRI) Simulabilité à mémoire finie de lois de probabilités continues
On s'intéresse à la question de la simulation exacte de lois de probabilités continues sur les réels, et plus précisément, à identifier quelles lois sont simulables exactement en n'utilisant qu'une mémoire finie - le modèle naturel étant une variante d'automates probabilistes, mais il est facile de voir que divers modèles sont équivalents (au moins au sens probabiliste de "presque sûrement"). Le premier résultat sur la question est une condition nécessaire dûe à Knuth et Yao, il y a plus de 40 ans: une loi à densité, et dont la densité est donnée par une fonction analytique, n'est pas simulable par automate si sa densité n'est pas en fait donnée par un polynôme. Je présenterai des résultats récents, qui permettent de caractériser les lois simulables parmi celles dont la densité est donnée par une fonction polynomiale par morceaux (de manière semi constructive dans le cas positif); et je discuterai de possibles extensions au cas multidimensionnel.
mardi 12 décembre 2017Cyril Gavoille (LaBRI) La coloration de graphe dans le modèle LOCAL - Partie II
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
mardi 05 décembre 2017Cyril Gavoille (LaBRI) La coloration de graphe dans le modèle LOCAL - Partie I
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
mardi 28 novembre 2017Ranko Lazic (Warwick University) Succinct progress measures and solving parity games in quasi-polynomial time
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.
mardi 21 novembre 2017Angelo Montanari (University of Udine) Model Checking: the Interval Way
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.
mardi 14 novembre 2017MF (LaBRI) Reunion d'equipe MF
mardi 07 novembre 2017Loïc Paulevé (LRI - Paris Sud) Formal methods for capturing dynamics of biological networks
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.
mardi 31 octobre 2017Vincent Penelle (LaBRI) Rewriting Higher-order Stack Trees
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.
mardi 24 octobre 2017Amina Doumane (LIP - ENS Lyon) Constructive completeness for the linear-time mu-calculus
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.
mardi 17 octobre 2017David Janin (LaBRI) Timed domains: an appetizer
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.
mardi 10 octobre 2017Miguel Romero (Oxford University) The complexity of graph query languages
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.
mardi 03 octobre 2017Joanna Ochremiak (IRIF) Proof complexity of constraint satisfaction problems
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.
mardi 26 septembre 2017Vincent Penelle (LaBRI) Which classes of origin graph are generated by transducers?
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.
mardi 04 juillet 2017Stefan GRUNER (University of Pretoria, South Africa) SAT-based Bounded Model Checking for 3-Valued Abstractions - Part II
Continuation of his precedent talk.
mardi 27 juin 2017Stefan GRUNER (University of Pretoria, South Africa) SAT-based Bounded Model Checking for 3-Valued Abstractions
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".
mardi 13 juin 2017Emilia Descotte (UBA, Argentine) Axiomatizations for downward XPath on Data Trees
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.
mardi 30 mai 2017Victor Marsault (University of Liège) An efficient algorithm to decide the periodicity of b-recognisable sets using MSDF convention
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.
mardi 23 mai 2017Michael Raskin (LaBRI) A linear lower bound for incrementing a space-optimal integer representation in the bit-probe model
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
mardi 16 mai 2017Igor Walukiewicz (LaBRI) Proving safety of concurrent programs
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.
mardi 09 mai 2017Alain Finkel (LSV, ENS Cachan) WBTS: the new class of WSTS without WQO.
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.
mardi 25 avril 2017Nathan Lhote (LaBRI) On Reversible Transducers
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.
mardi 04 avril 2017Andrzej Murawski (University of Warwick) Automata theory and game semantics of higher-order computation
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.
mardi 28 mars 2017David Janin (LaBRI) Time domain (for time denotational semantics)
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.
mardi 21 mars 2017Laurent Bienvenu (LIRMM Montpellier) Learning probability measures
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]
mardi 14 mars 2017Gabriele Puppis (LaBRI) On the decomposition of finite-valued streaming string transducers
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.
mardi 07 mars 2017Charles Grellois (University of Bologna) Verifying properties of functional programs: from the deterministic to the probabilistic case
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.
mardi 28 février 2017Emmanuel Fleury (LaBRI) Digital Currencies
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.
mardi 14 février 2017Hugo Gimbert (LaBRI) Emptiness of nonzero automata is decidable
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
mardi 24 janvier 2017Rasmus Ibsen-Jensen (IST Austria) Faster algorithms for program analysis
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.
mardi 10 janvier 2017B Srivathsan (CMI Chennai) Why liveness for timed automata is hard, and what we can do about it
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.



Archives des années précédentes




Responsables

Nathanaël Fijalkow, Filip Mazowiecki