These talks will review the current state of the art regarding some hierarchies of regular languages, built using two operations: polynomial closure and Boolean closure. The presentation will rely on a generic approach, which captures all known results about these hierarchies.

As in part I.

I will consider the separability problem of reachability sets of Vector Addition Systems by modular and unary sets. The focus will be on the technique, which allowed us to show decidability of these problems. Presentation is based on the joint work with Lorenzo Clemente, Sławomir Lasota and Charles Paperman, published on STACS 2017.

Czerwinski et al. have recently shown that, over finite words, PTL separability is decidable for a large class of languages, which turns out to even include higher-order languages. I will show how this result can be simplified and generalised in a framework based on well-quasi-orders and ideal decompositions, encompassing for instance finite tree languages. This talk is meant as a tutorial based on joint work with Jean Goubault-Larrecq, and the material will be re-used by Georg Zetzsche in his talk on parameterised wqos, downwards closures, and separability problems at 3:15pm.

We show that regular separability for a visibly pushdown language (VPL) and its complement relative to the set of well-matched words is decidable. These notions are explained below. A VPL is defined over an alphabet that is structured into three disjoint subsets of call, return, and local actions. A visibly pushdown automaton (VPA) acts like a standard pushdown automaton with the restriction that for call actions one symbol is pushed to the stack, for return actions one symbol is popped from the stack, and for internal actions the stack remains unchanged. A word is called well-matched if it is balanced with respect to calls and returns, that is, the stack is empty after reading the word and there are no pops on the empty stack. Given a VPL L consisting of well-matched words only, its well-matched complement consists of all well-matched words in the complement of L. We show that it is decidable whether there is a regular set R separating L and its well-matched complement (that is, R contains L and does not intersect the well-matched complement of L). A different formulation of the result is the following: For a visibly pushdown automaton it is decidable whether it is equivalent to a finite automaton on the set of well-matched words. The talk is based on the paper Vince Bárány, Christof Löding, and Olivier Serre. Regularity problems for visibly pushdown languages. In Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006, volume 3884 of Lecture Notes in Computer Science, pages 420-431. Springer, 2006.

We discuss a flexible class of well-quasi-orderings on words that generalizes the ordering of (not necessarily contiguous) subwords. Each of these orderings is specified by a finite automaton or a counter automaton and, like the subword ordering, guarantees regularity of all downward (or upward) closures. We then consider two problems. First, we study for which language classes one can effectively compute downward closures with respect to these orderings. Second, we are interested in which language classes permit a decision procedure to decide whether two given languages are separable by a PTL with respect to such an ordering. Here, a PTL is a finite Boolean combination of upward closed sets. The main result is that, under mild assumptions on closure properties, these two problems are solvable for the same language classes. Moreover, solvability is equivalent to that of a particular unboundedness problem that has recently been shown to be decidable for many powerful language classes.

Lombardy and Mairesse (2006) have shown that a partial function from words to reals that is definable both with a min-plus and a max-plus automaton can effectively be defined by an unambiguous automaton. I will show during this talk how this result can be strengthen to a separation result: whenevever there is a min-plus definable function which it pointwise larger or equal to a max-plus definable one, it is possible to separate them by an unambiguous definable function. This is joint work with Sylvain Lombrady