Joint session talks:

1. C Aiswarya (Chennai Mathematical Institute, India) – Using tree-width for verifying infinite state systems Abstract

   Tree-width has been a popular parameter that gives tractable algorithms in parametrised algorithms. In this talk we explore its use in verification.

   Verification amounts to guaranteeing that a property holds on all runs of the system. We will consider systems with stacks, communicating channels, variables etc. As expected, these systems are Turing powerful and their verification is undecidable in general.

   Under-approximation is a technique that allows to still reason about such Turing powerful systems, and has been proven efficient in finding bugs. In under-approximate verification, only a subset of runs are explored, and the subset is often specified by a parameter. We will now impose a bound on tree-width as the parameter.

   Towards this, we will depart from the traditional view of treating runs as just words (sequences) to a richer understanding in terms of graphs. Thus the behaviours of a system is a (possibly infinite) set of unbounded graphs.

   With bounded tree-width under-approximation, we will explore only those behaviours whose tree-width is bounded by the given parameter. We will see that many verification problems become efficiently decidable when restricted to graphs of tree-width bounded by a parameter k, even though it allows to explore infinitely many runs (behaviours).

   We will see this in the particular case of multi-pushdown systems, communicating finite state machines, communicating pushdown machines, timed multi-pushdown systems and multi-pushdown systems handling numerical data.

   Slides
2. Mikołaj Bojańczyk (University of Warsaw, Poland) – Polyrational functions Abstract

   I will describe a class of string-to-string transducers, which goes beyond rational or regular functions, but still shares many of their good properties (e.g. the inverse image of a regular language is regular). Unlike many string-to-string transducer models (including sequential, rational and regular transducers), which have linear size increase, the the new class (called polyregular functions) has polynomial size increase.

   The main selling point of the polyregular functions is that they admit numerous equivalent descriptions: (a) automata with pebbles; (b) a fragment of lambda calculus; (c) a fragment of for-programs; and (d) compositions of certain atomic functions, such as reverse or a form of string squaring. Also, most likely (this is still ongoing work): (e) mso string-to-string interpretations.

   Slides
3. Cyril Gavoille (University of Bordeaux, France) – Distributed computing with quantum resources and beyond Abstract

   The goal of this talk is to show the impact of quantum ressources on the performances of distributed algorithms. We will present basic concepts on quantum information, and how to use non-local effects to extend the classical model distributed model.

   Slides
4. Seth Gilbert (National University of Singapore) – How To Plan Ahead Abstract

   Planning ahead has many benefits: it often leads to better results and less last minute stress. That is not what this talk will be about.

   Instead, let us think about scheduling. Imagine you are scheduling appointments at a doctor's office. Dr. Spaceman has a busy schedule, with patients all day. And then a VIP case arrives which has to be scheduled exactly at 10am. The result? All the other patients have to be rescheduled, which makes them exceedingly unhappy. Ideally, there would be some way to plan ahead and avoid this disruption.

   The same type of rescheduling problem occurs in many different contexts, ranging from delivery schedules to airline routes to assembly lines on a factory floors. In general, we want to maintain a nearly optimal schedule, while allowing jobs to be inserted and deleted. As the set of jobs in the system changes, we will reschedule existing jobs to maintain an efficient schedule. However, rescheduling jobs has a cost, and our goal is to minimize that cost. Specifically, I will talk about three examples: scheduling with arrival times and deadlines, scheduling to minimize the makespan, and scheduling to minimize the sum-of-completion-times.

   In general, we will see that by planning ahead, we can minimize the disruption caused by changes to the schedule.

   (Joint work with: Michael Bender, Martin Farach-Colton, Sandor Fekete, Jeremy Fineman, Shunhao Oh)

   Slides
5. Marcin Jurdzinski (University of Warwick, UK) – Universal Trees Abstract

   Universal trees are very basic combinatorial objects: an ordered tree is (n, h)-universal if every ordered tree of height at most h and with at most n leaves can be embedded into it. We give nearly-matching upper and lower bounds on the size of the smallest (n, h)-universal trees: if h is asymptotically logarithmic in n then it is polynomial in n, and if h is asymptotically super-logarithmic in n then it is quasi-polynomial.

   We then discuss several applications of universal trees:
   - to improve algorithms for solving games, such as parity games and mean-payoff parity games, to quasi-polynomial and pseudo-quasi-polynomial, respectively;
   - to show that separating automata---due to Bojanczyk and Czerwinski---unify all (but one) currently known quasi-polynomial algorithms for solving parity games: due to Calude, Jain, Khoussainov, Li, and Stephan, 2017; Jurdzinski and Lazic, 2017; Fearnley, Jain, Schewe, Stephan, and Wojtczak, 2017; and Lehtinen, 2018;
   - to prove a quasi-polynomial lower bound on the size of all (strongly) separating automata, hence pinpointing a quasi-polynomial barrier that most existing techniques for solving parity games efficiently are vulnerable to;
   - to improve and streamline translations from alternating parity automata on words to alternating weak automata.

   The talk is based on several joint works with various subsets of: Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow, Ranko LaziĆ, Karoliina Lehtinen, and Paweł Parys.

   Slides
6. Jerome Leroux (LaBRI, University of Bordeaux) – The Reachability Problem for Petri Nets is Not Elementary Abstract

   Petri nets, also known as vector addition systems, are a long established and widely used model of concurrent processes. The complexity of their reachability problem is one of the most prominent open questions in the theory of verification. That the reachability problem is decidable was established by Mayr in his seminal STOC 1981 work, and the currently best upper bound is non-primitive recursive cubic-Ackermannian of Leroux and Schmitz from LICS 2015. We show that the reachability problem is not elementary. Until this work, the best lower bound has been exponential space, due to Lipton in 1976.

   Joint work with Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki.

   Slides
7. Meena Mahajan (Institute of Mathematical Sciences, Chennai, India) – Lower bound techniques for QBF proof systems Abstract

   How do we prove that a false QBF is inded false? How big a proof is needed? The special case when all quantifiers are existential is the well-studied setting of propositional proof complexity. Expectedly, universal quantifiers change the game significantly. Several proof systems have been designed in the last couple of decades to handle QBFs. Lower bound paradigms from propositional proof complexity cannot always be extended - in most cases feasible interpolation and consequent transfer of circuit lower bounds works, but obtaining lower bounds on size by providing lower bounds on width fails dramatically. A new paradigm with no analogue in the propositional world has emerged in the form of strategy extraction, allowing for transfer of circuit lower bounds, as well as obtaining independent genuine QBF lower bounds based on a semantic cost measure.

   This talk will provide a broad overview of some of these developments.

   Slides
8. Jaikumar Radhakrishnan (Tata Institute of Fundamental Research, Mumbai, India) – Information theory in computer science Abstract

   Many combinatorial and computational problems can be analysed using the information-theoretic lens.
   We will present some examples where information-theoretic arguments yield interesting consequences in combinatorics and complexity theory.

   Slides
9. Marc Zeitoun (LaBRI, University of Bordeaux, France) – A survey on expressiveness problems for regular word languages Abstract

   In the theory of regular languages of finite words, the understanding of concatenation hierarchies is one of the most fundamental and challenging topic. In this talk, I will survey progress made on this problem since 1971. In particular, I will present a few recent generic statements implying all previously known results.

   Slides

Track A: Algorithms and Complexity

1. Umang Bhaskar (Tata Institute of Fundamental Research, Mumbai, India) – Partial Function Extension with Applications to Learning and Property Testing Abstract

   In partial function extension, we are given a partial function consisting of points from a domain and a function value at each point. Our objective is to determine if this partial function can be extended to a function defined on the domain, that additionally satisfies a given property, such as convexity. This basic problem underlies research questions in many areas, such as learning, property testing, and game theory. We present bounds on the complexity of partial function extension to subadditive, submodular, and convex functions, and present some applications to learning as well as property testing for these functions.

   Slides
2. Guillaume Blin (Labri, Bordeaux, France) – Algorithmic challenges in radiation therapy Abstract

   In this talk, we will present a wide range of algorithmic problems related to radiation therapy : from combinatorics to deep learning

   Slides
3. Andrej Bogdanov (The Chinese University of Hong Kong, Hong Kong) – Approximate degree and bounded indistinguishability Abstract

   A Boolean function has approximate degree d if it can be approximated pointwise by a degree-d polynomial. Two distributions over n bits are d-wise indistinguishable (for d ≤ n) if their marginals on any subset of d bits are identical. The duality between these two notions can be used to prove composition theorems in one direction and construct secret sharing schemes in the other direction. I plan to show this connection and describe some recent developments in both domains.

   Slides
4. Vincenzo Bonifaci (Institute for Systems Analysis and Computer Science, CNR, Rome, Italy) – Collective Dynamics for Electrical Flow Estimation Abstract

   The computation of electrical flows is a crucial primitive for many recently proposed optimization algorithms on weighted networks. While typically implemented as a centralized subroutine, the ability to perform this task in a fully decentralized way is desirable, and a natural question is whether it can provably be accomplished in an efficient way by a network of agents executing a simple protocol.

   We consider two distributed approaches to electrical flow computation on a weighted network: a deterministic process mimicking Jacobi's iterative method for solving linear systems, and a randomized token diffusion process, based on revisiting a classical random walk process on a graph with an absorbing node. We show that both processes converge to a solution of Kirchhoff's node potential equations, derive bounds on their convergence rates in terms of the weights of the network, and analyze their time and message complexity.

   Joint work with L. Becchetti and E. Natale.

   Slides
5. Yuval Filmus (Technion, Israel) – Discrete harmonic analysis: beyond the Boolean hypercube Abstract

   Analysis of Boolean functions is a topic at the intersection of computer science and combinatorics, which uses tools and techniques from probability theory and functional analysis.

   It has become part of the fundamental topic of theoreticians working in computational complexity theory. Tradionally, the functions being studied live on the Boolean hypercube {0,1}^n.

   Recently, attention has been drawn to other domains, with some spectacular applications, such as the recent proof of the 2-to-2 conjecture (a weaker variant of Khot's Unique Games Conjecture).

   In the talk, I will survey some elements of the classical theory, and then describe some recent progress.

   Slides
6. Naveen Garg (Indian Institute of Technology Delhi, India) – Integral flow in series parallel graphs Abstract

   This talk considers the problem of routing multicommodity flow in a series parallel graphs. It is conjectured that if the Supply+demand graph is Eulerian and the capacity of every cut is at least twice the demand across it then flow can be routed integrally. We show this is true when the graph is a parallel composition of paths. Our algorithm uses ideas from Edmonds algorithm for matching in general graphs to build an augmenting path like algorithm for routing flow.

   Slides
7. Arijit Ghosh (ACMU, ISI Kolkata, India) – Shallow Packing Lemma and its Applications in Combinatorial Geometry Abstract

   The packing lemma of Haussler states that given a set system with bounded VC dimension, if every pair of sets in the set system has large symmetric difference, then the set system cannot contain too many sets. This has turned out to be the technical foundation for many results in combinatorial geometry and discrepancy. Recently it was generalised to the shallow packing lemma, applying to set systems as a function of their shallow-cell complexity. We will present the idea behind the proof of this result and some of its applications.

   Slides
8. Nutan Limaye (Indian Institute of Technology Bombay, India) – A #SAT Algorithm for Small Constant-Depth Circuits with PTF gates Abstract

   We show that there is a randomized algorithm that, when given a small constant-depth Boolean circuit C made up of gates that compute constant-degree Polynomial Threshold functions or PTFs (i.e., Boolean functions that compute signs of constant-degree polynomials), counts the number of satisfying assignments to C in significantly better than brute-force time.

   Formally, for any constants d, k, there is an epsilon > 0 such that the algorithm counts the number of satisfying assignments to a given depth-d circuit C made up of k-PTF gates such that C has size at most n^(1+epsilon). The algorithm runs in time 2^(n − n^{Omega(epsilon)}) . Before our result, no algorithm for beating brute-force search was known even for a single degree-2 PTF (which is a depth-1 circuit of linear size).

   The main new tool is the use of a learning algorithm for learning degree-1 PTFs (or Linear Threshold Functions) using comparison queries due to Kane, Lovett, Moran and Zhang (FOCS 2017). We show that their ideas fit nicely into a memoization approach that yields the #SAT algorithms.

   This is a joint work with Swapnam Bajpai, Vaibhav Krishan, Deepanshu Kush, and Srikanth Srinivasan.

   Slides
9. Meghana Nasre (Indian Institute of Technology Madras, India) – Stability, Popularity and Lower Quotas Abstract

   We consider the problem of assigning a set of men to a set of women where each participant ranks members of the opposite side in an order of preference. This is called the stable marriage problem in literature. It is well known that every instance of the stable marriage problem admits a "stable matching" which can be computed efficiently by the Gale and Shapley algorithm.

   In this talk we consider three variants of the stable marriage problem where

   1. Preference lists can contain ties,
   2. Preference lists can be incomplete,
   3. Vertices can have lower quotas.

   For each of these variants a different notion of optimality is applicable; yet we show that, a simple extension of the Gale and Shapley algorithm computes an optimal matching in each of them. The talk is based on three papers -- Z. Kiraly (Algorithmica 2011), T. Kavitha (SICOMP 2014) and Nasre and Nimbhorkar (FSTTCS 2017).

   Slides
10. Christophe Paul (LIRMM, Montpellier, France) – Connected tree-width and connected cops and robber game. Abstract

    The node search game against a lazy/agile invisible robber has been introduced as a search-game analogue of the graph parameters of treewidth/pathwidth. In the "connected" variants of the above two games, we additionally demand that, at each moment of the search, the "clean" territories are connected.

    The connected search game against an agile and invisible robber has been extensively examined. The monotone variant (where we also demand that the clean territories are progressively increasing) of this game, corresponds to the graph parameter of connected path width. It has been shown that its value cannot be more than the double (plus some constant) of its non-connected counterpart. This implied that the "price of connectivity" is bounded by 2 for the case of an agile robber.

    In this talk, we consider the connected variant of this search game where the robber is lazy. We introduce two alternative graph-theoretical formulations of this game, one in terms of connected tree decompositions, and one in terms of (connected) layouts, leading to the graph parameter of connected tree width. We first show that in contrast to the "agile-robber" variant, the price of connectivity for the "lazy-robber" game is unbounded. To that aim, we observe that the connected treewidth parameter is closed under contraction and prove that the set of contraction obstruction is infinite for every integer k ≥ 2.

    Slides
11. Srikanth Srinivasan (Indian Institute of Technology Bombay, India) – A Hierarchy theorem for AC^0[2] circuits Abstract

    A Hierarchy theorem for a computational resource shows that access to more of that resource yields strictly more computational power. In this result, we study hierarchy theorems for Boolean circuits and show the first Fixed-Depth Size Hierarchy theorem for the well studied circuit class AC^0[2]. Such results were known for the smaller class AC^0 for more than 3 decades.

    The separating functions are obtained by constructing explicit AC^0[2] circuits for solving the coin problem, which is defined as follows. For a parameter delta, we have to decide whether a given coin has bias (1+delta)/2 or (1-delta)/2. Our upper bounds are proved by derandomizing a circuit construction of O'Donnell-Wimmer (2007) and Amano (2009) to reduce the number of samples. Our lower bounds follow from a modification of the Razborov-Smolensky polynomial method.

    This result is joint with Nutan Limaye (IITB CSE), Karteek Sreenivasaiah (IITH CSE), Utkarsh Tripathi (IITB Math) and S Venkitesh (IITB Math).

    Slides

Track B: Automata and Logic

1. Benedikt Bollig (LSV, ENS Paris-Saclay, France) – Communicating Finite-State Machines Capture First-Order Logic with "Happened Before" Abstract

   In the early 1960s, Büchi, Elgot, and Trakhtenbrot showed that finite automata over words have the same expressive power as monadic second-order (MSO) logic. Since then, this fundamental theorem has been generalized to various other computational devices such as tree automata, asynchronous automata, nested-word automata, and branching automata. Actually, all these devices are complementable, which allows for an inductive translation of formulas into automata. Here, we consider communicating finite-state machines (CFMs), introduced by Brand and Zafiropulo in 1983. CFMs are a basic model of finite-state processes that communicate via unbounded FIFO channels. Unfortunately, they are not complementable. In fact, they are strictly less expressive than MSO logic interpreted over message sequence charts (MSCs), which naturally arise as executions of CFMs.

   In this talk, we show that CFMs still capture first-order logic with "happened before" and are, therefore, expressively equivalent to existential MSO logic. The happened-before relation is a partial-order relation that reflects causality in an execution of a distributed system. The proof proceeds in two steps. We show that (i) every first-order sentence can be transformed into an equivalent formula from a star-free version of propositional dynamic logic (PDL) with loop and converse, and (ii) every star-free PDL sentence can be translated into an equivalent CFM. As a byproduct, we obtain that first-order logic over MSCs has the three-variable property.

   This is joint work with Marie Fortin and Paul Gastin, presented at CONCUR 2018: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2018.7

   Slides
2. Olivier Carton (IRIF, Université Paris Diderot, France) – Tight links between normality and automata Abstract

   Normality has been introduced by É. Borel more than one hundred years ago. A real number is normal to an integer base if, in its infinite expansion expressed in that base, all blocks of digits of the same length have the same limiting frequency. Normality formalizes the least requirements about a random sequence. In this talk, we explain several links between this notion and finite-state machines. This includes the characterization of normality by non-compressibility, preservation of normality by selection and computing frequencies with weighted automata.

   Slides
3. Nathanaël Fijalkow (LaBRI, University of Bordeaux, France) – The complexity of mean payoff games using universal graphs Abstract

   We study the computational complexity of solving mean payoff games. This class of games can be seen as an extension of parity games, and they have similar complexity status: in both cases solving them is in NP ∩ coNP and not known to be in P. In a breakthrough result Calude, Jain, Khoussainov, Li, and Stephan constructed in 2017 a quasipolynomial time algorithm for solving parity games, which was quickly followed by two other algorithms with the same complexity. Our objective is to investigate how these techniques can be extended to the study of mean payoff games.

   It has recently been shown that the notion of universal graphs (or equivalently: separating automata) captures the combinatorial structure behind all three quasipolynomial time algorithms for parity games and gives a unified presentation together with the best complexity to date.

   In this paper we give upper and lower bounds on the complexity of algorithms using universal graphs for solving mean payoff games. We construct two new algorithms. Our first algorithm depends on the largest weight N (in absolute value) appearing in the graph and runs in sublinear time in N , improving over the previously known linear dependence in N. Our second algorithm runs in polynomial time for a fixed number k of weights. We complement our upper bounds by providing in both cases almost matching lower bounds, showing the limitations of the approach. We show that using universal graphs we cannot hope to improve on the dependence in N nor break the linear dependence in the exponent in the number k of weights. In particular, universal graphs do not yield a quasipolynomial algorithm for solving mean payoff games.

   Slides
4. S Krishna (Indian Institute of Technology Bombay, Mumbai, India) – Building Blocks for Regular Functions Abstract

   Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this talk, we discuss how regular functions, either on finite or infinite words can be described using regular transducer expressions (RTE). The basic building blocks of these expressions are simple and natural functions. I will touch upon two such building blocks : one which uses the composition operation, and one which does not.

   This talk is based on two papers :
   Vrunda Dave, Paul Gastin, Shankara Narayanan Krishna. Regular Transducer Expressions for Regular Transformations, LICS 2018
   Mikolaj Bojanczyk, Laure Daviaud, Shankara Narayanan Krishna. Regular and First-Order List Functions, LICS 2018

   Slides
5. Andreas Maletti (University of Leipzig, Germany) – Characterizations of subregular tree languages– Abstract

   We first recall the well-known regular tree languages, their properties, and several of their characterizations. We then move on to classes of subregular tree languages that are relevant in natural language processing. Despite their rather bad closure properties, the local tree languages are particularly attractive in applications, since they are easy to infer from data. In addition, their expressive power is well understood. A more expressive formalism, called tree substitution grammars, is similarly popular despite its even worse closure properties, but their expressive power is not understood at all. We review the existing results and present the open problems.

   Slides
6. Kuldeep Meel (National University of Singapore) – Beyond NP Revolution– Abstract

   The paradigmatic NP-complete problem of Boolean satisfiability (SAT) solving is a central problem in Computer Science. While the mention of SAT can be traced to early 19th century, efforts to develop practically successful SAT solvers go back to 1950s. The past 20 years have witnessed a ``SAT revolution" with the development of conflict-driven clause-learning (CDCL) solvers. Such solvers combine a classical backtracking search with a rich set of effective heuristics. While 20 years ago SAT solvers were able to solve instances with at most a few hundred variables, modern SAT solvers solve instances with up to millions of variables in a reasonable time.

   The "NP-revolution" opens up opportunities to design practical algorithms with rigorous guarantees for problems in complexity classes beyond NP by replacing a NP oracle with a SAT Solver. In this talk, we will discuss how we use NP revolution to design practical algorithms for two fundamental problems in artificial intelligence and formal methods: Constrained Sampling and Counting.

   Slides
7. Daniel Neider (MPI Kaiserslautern, Germany) – Learning Linear Temporal Properties – Abstract

   Making sense of the observed behavior of complex systems is an important problem in practice. It arises, for instance, in debugging (especially in the context of distributed systems), reverse engineering (e.g., of malware and viruses), specification mining for formal verification, and the modernization of legacy systems to name but a few examples.

   To help engineers understand the dynamic (i.e., temporal) behavior of complex systems, we develop algorithms to learn linear temporal properties from data. More precisely, the problem we address in this talk is the following: given two disjoint, finite sets of (potentially infinite) words, representing positive and negative examples, construct a (minimal) formula in Linear Temporal Logic such that all positive examples satisfy the formula, while all negative example do not. In order to improve on the readability of the resulting formulas and to give a better "intuitive" explanation of the observed data, our learning algorithms are designed to learn minimal formulas, or at least formulas with a "simple" structure. We also discuss open problems in this area as well as interesting directions for future work.

   Slides
8. M Praveen (Chennai Mathematical Institute, India) – Playing with Repetitions in Data Words Using Energy Games – Abstract

   We introduce two-player games which build words over infinite alphabets, and we study the problem of checking the existence of winning strategies. These games are played by two players, who take turns in choosing valuations for variables ranging over an infinite data domain, thus generating multi-attributed data words. The winner of the game is specified by formulas in the Logic of Repeating Values, which can reason about repetitions of data values in infinite data words. We prove that it is undecidable to check if one of the players has a winning strategy, even in very restrictive settings. However, we prove that if one of the players is restricted to choose valuations ranging over the Boolean domain, the games are effectively equivalent to single-sided games on vector addition systems with states (in which one of the players can change control states but cannot change counter values), known to be decidable and effectively equivalent to energy games.

   Previous works have shown that the satisfiability problem for various variants of the logic of repeating values is equivalent to the reachability and coverability problems in vector addition systems. Our results raise this connection to the level of games, augmenting further the associations between logics on data words and counter systems.

   This is joint work with Diego Figueira.

   Slides
9. Sylvain Schmitz (LSV, ENS Paris-Saclay, France) – On the Complexity of VAS Reachability – Abstract

   The decidability of the reachability problem in vector addition systems is a landmark result in theoretical computer science, with applications in an array of fields ranging from program verification to data logics. I will present the main arguments of the first complexity upper bound for this problem, obtained together with Leroux by analysing the decomposition algorithm invented by Mayr and successively refined by Kosaraju and Lambert.

   Slides
10. Laurent Simon (LaBRI, University of Bordeaux, France) – SAT Solvers: a success story Abstract

    A presentation of the state-of-the-art of SAT solvers

11. Meenakshi d'Souza (International Institute of Information Technology, Bangalore, India) – Formal methods for embedded software systems: Two problems. – Abstract

    Many safety critical systems are embedded systems and critical control functionality is done by software in such systems. Formal methods play an important role in verifying safety and other functional requirements of these systems. This talk will present work done on two problems in this area:

    (1) Program analysis for detecting low level errors and safety violations in a programming language for industrial robots. Such a language has several complex data types, digital inputs originating from the underlying platform and robot arm movement instructions. (2) Modeling and verification of IoT protocols in Event-B. We describe refinement based modeling of IoT protocols MQTT, MQTT-SN and XMPP and verification of their QoS, persistent storage and other functional requirements.

    The talk will highlight challenges faced in modeling real-life systems using formal methods notations and verifying requirements about these systems.

    Slides
12. Jean-Marc Talbot (Aix-Marseille University, France) – Tree Transformations by means of visibly pushdown transducers Abstract

    In this talk, we consider tree transformations for which trees are represented as well-nested words and defined as transducers running on these well-nested words. Various classes of transformations are studied depending on the kind of machines defining them. We will be particularly interested into classes that define tree-to-tree transformations, that is when the output range contains only well-nested words.

    Slides
13. Georg Zetzsche (MPI-SWS, Kaiserslautern, Germany) Unboundedness Problems for Languages of Vector Addition Systems Abstract

    A vector addition system (VAS) with an initial and a final marking and transition labels induces a language. In part because the reachability problem in VAS remains far from being well-understood, it is difficult to devise decision procedures for such languages. This is especially true for checking properties that state the existence of infinitely many words of a particular shape. Informally, we call these unboundedness properties.

    We present a simple set of axioms for predicates that can express unboundedness properties. Our main result is that such a predicate is decidable for VAS languages as soon as it is decidable for regular languages. Among other results, this allows us to show decidability of (i) separability by bounded regular languages, (ii) unboundedness of occurring factors from a language K with mild conditions on K, and (iii) universality of the set of factors.