Separability Problems

an ICALP workshop

Venue:

The 14^{th} of July 2017, in Warsaw

Program:

9:30 - 10:15 Marc Zeitoun

Separation and concatenation hierarchies (part I), slides

+

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), slides

+

As in part I.

Coffee Break

11:30 - 12:15 Wojciech Czerwiński

Separability of Reachability Sets of Vector Addition Systems, slides

+

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.

Lunch

14:30 - 15:15 Christof Löding

Regular Separability for Well-Matched Complements of Visibly Pushdown Languages, slides

+

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, slides

+

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.

Coffee Break

16:30 - 17:15 Thomas Colcombet

Separation of tropical automata, slides

+

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