9:30 - 10:15 Marc Zeitoun
Separation and concatenation hierarchies (part I)
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.
10:15 - 11:00 Thomas Place
Separation and concatenation hierarchies (part II)
As in part I.
11:30 - 12:15 Wojciech Czerwiński
Separability of Reachability Sets of Vector Addition Systems
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.
12:15 - 13:00 Sylvain Schmitz
An Order-Theoretic Framework for PTL Separability
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.
14:30 - 15:15 Christof Löding
Regular Separability for Well-Matched Complements of Visibly Pushdown Languages
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.
15:15 - 16:00 Georg Zetzsche
Parameterized WQOs, downward closures, and separability problems
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.
16:30 - 17:15 Thomas Colcombet
Separation of tropical automata
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
17:15 - 18:00 Moderated session of open problems and discussion