I will talk about an approach to regular separability problem in languages of vector addition systems.

And this is a joint work with Gergely Zeche, so first I will define regular separability notion and I will recall what are vector addition systems and their languages. Then I will tell you about our motivation and brief history of the problem and I will

state you our main result and then the rest of the talk I will devote to telling you about our techniques. So I will try to show you the intuition behind our proof because I think that maybe our

techniques are even a bigger contribution than the theorem itself. Okay, so what is a separability notion? Imagine we have two sets or languages K and L, let's say they are disjoint and then we say that set S separates them if it's like on the picture.

So K is included in S and S is disjoint from L. Okay, and we say that languages K and L are regular separable if there is some regular language S which separates them.

Sometimes we say a Schott tree rec-separable. Okay and now let's recall what are vector addition systems with states. So such a d-dimensional vector addition system with state, Schott tree, Schott-Lee, d-vas, it consists from a finite set of states Q and finite set of transitions, every such

a transition has a source state, target state and effect and effect is a d-dimensional integer vector and if we are talking about labeled vases, if we want to talk about

languages, then such a vas comes with a labeling of transitions by letters from some finite alphabet, let's say sigma, and how these transitions are applied if we are in configuration with state p and vector u, which is a vector with non-negative entries

necessarily, then we can fire such a transition which has source state p, target state q and some effect v, and then we go to a configuration with state q and with vector u plus v under the

condition that u plus v is non-negative on all the coordinates. Okay, so I hope it was just a reminder and so that's why I define it so briefly. If we want to define a language of a vas, then we need to specify source configuration and target configuration and then language of a vas

with such fixed configurations is defined naturally, so with just set of words which can be read on paths leading from source configuration to target configuration. What is important here is that we have an acceptance condition but by a single

configuration, not by a state. Okay, so what is a regular separability problem for vas languages? You are given two labeled vases with transitions labeled by letters from finite

alphabet. These vases are a and b and we ask whether their languages are regular separable. So what is a motivation for us to study this problem? I can say that this motivation is two fold. One comes from vases and another comes from separation. So first of all,

vases are a very fundamental model which is still not well understood and it needs deeper understanding. So for example, this very fundamental problem of reachability is still

complexity is not really understood but also many other problems lack understanding and and this is one motivation and one way to gain understanding is to study to study vases from a bit different perspective because maybe it gives you,

it gives us some new insights which we haven't thought before and one such possibility is to study separability problem which is a very natural problem which was maybe not so so much studied but recently it's studied more and we can observe that for example

separation generalizes reachability problem for vases because if we say about languages of vases specified by source and target configuration then reachability problem is just question whether

language is empty. So maybe we can generalize it and talk about more sophisticated problems which somehow use more structure and maybe this will give us some interesting insights. So this is let's say our motivation to study this problem.

Short history. So we conjecture that this problem is decidable in general but it's open, we don't know it but the problem is solved in a few subclasses. It's known to be decidable for example it's known that if our input are one-dimensional vases

then the problem so in other words one counter nets then the problem is decidable and also PSPACE complete. Similarly if our input are so-called integer vases or we can say

Z-vases. So what is a Z-vas? In a Z-vas we don't demand that our path should be necessarily all the time above zero in this positive quadrant. In a Z-vas the path can go below zero in any

dimension as much as it wants. So this is a Z-vas and the problem is also decidable for Z-vases. Similarly for commutative closure of vases which happen to be also a subclass of vast languages and also for languages of vases but with different acceptance conditions so with

acceptance not by target configuration but by set of target accepting states. So all these subclasses are solved and our main result kind of generalizes this. So our main result says the

following that the regular separability problem is decidable if we ask about regular separability of general vast language on one side and on the other side language of a vast coming from some subclass either one-dimensional vases or vases accepting by state or integer vases.

So you can see that this generalizes three of the four points from the previous slide and the fourth point can be also is also generalized because it can be reduced to the vast versus Z-vas case. And what is maybe more important is the technique we achieved this

by a uniform technique and we hope that maybe this technique can be used in the future to solve a general vast regular separability problem. And in the rest of the talk I will

present you this technique. Okay so what is our first observation? So let us fix an alphabet a n which consists of two n letters u1 d1 u2 d2 and so on and u1 corresponds to going up

in dimension one, d1 letter corresponds to going down in dimension one, u2 corresponds to going up in dimension two and so on. So if you have for example a word u1 d2 it corresponds

to first going up in dimension one and then going down in dimension two. So you can observe that words over the alphabet a n they correspond to such a walks in n-dimensional grid and we will use this connection and in that way we can define a language Zn like 0

and n-dimensional and this will be set of words which correspond to paths which let's say start in zero they do some walk and they finish back in the same place in the zero vector so their total effect is the zero vector and we write z paths because we

we don't demand that they stay in the positive quadrant they can travel also below zero in every coordinate. Okay so what is our lemma then? So the lemma says that for any

vass a and z was b one can compute a vass c over the alphabet a n such that languages of a and b

are regular separable even only if language of c and the our and our language Zn are regular separable. Observe that Zn is clearly a language of the z-vass. So what it gives us is is that we can actually reduce our vass versus z-vass separability problem to a similar vass versus

z-vass separability problem but when a z-vass is fixed and observe that now separators are regular languages which contain language L of c but are disjoint from language Zn.

So next step our next step will be looking what are the potential candidates on this separator Zn what regular languages are disjoint from our language Zn. Okay let's let's come back

for a moment to the other cases as I said I will focus mainly on this case of vass versus z-vass but let's briefly say how it works similarly for the other cases so when we have this alphabet a n Zn is is our language Dn is the set of a similar language set

of words corresponding to n paths of effect equals zero so paths which start in zero in zero vector but they all the time stay in the positive quadrant and they also come back

to zero at the end and Cn it will be set of words corresponding to n paths which start in zero but they don't have to finish in zero they they just have to stay in the positive quadrant all the time and then our result says a theorem in our paper that in the case of vass versus

z-vass we can we can reduce the case when the z-vass language is fixed and it's exactly Zn in the case of vass versus one vass we can fix the one vass language to be D1 and in the case of regular separability of vass versus vass accepting by state we can fix

the vass accepting by state language to be exactly Cn okay but let's come back to our vass versus z-vass case so our key lemma is like that so recall what was an and what was

Zn and as i said before our problem actually boils down to understanding what kind of which regular languages are disjoint with Zn and this lemma characterizes such languages

so lemma says that if r is over alphabet an is a regular language then r has empty intersection with Zn if and only if r is included in a finite union of basic languages and we have two kinds of basic languages modulo language and drift language and

of course i have to tell you what are these languages on the next page so what are basic languages first simpler kind of basic language is modulo language so n is a number and language

Mn is set of words corresponding to z paths with effect which is not equal zero vector modulo n so it's quite simple to see that Mn and Zn are actually disjoint because Zn contains these paths which have effect exactly zero and Mn does not contain such paths and may and also some other

ones and it's also easy to see that Mn is a regular language because its automaton just have to remember the current effect modulo n on every coordinate

and we have a second type of our basic languages which is called the drift language it's a bit more sophisticated so it's Duk, u is a vector n-dimensional one or d-dimensional one and k is a positive integer i will draw it to present it

easier so here we have a vector u here we have some perpendicular line to it and Duk contains words which correspond to z paths which somehow deviate into direction u

for example like that so this blue path it rather goes into direction u but sometimes it comes back so a path in order to be in Duk it has to never come back more than k so like on our picture here this path comes back a bit but not more than k

and additional condition is that this path has to be at the end not equal to zero so it's easy to see that Duk is definitely disjoint from that n because it doesn't finish at zero

and maybe it's not immediate to see that this is a regular language but it's also not hard but i will not prove it now because we don't have much time for it okay so these are our basic languages let us recall our main lemma it says that actually

we have characterized which regular languages don't touch language that n and i think this result can be of independent interests maybe i hope maybe it can be used in some research and not really considering not really concerning separability problem

okay let's go further i will try to show you intuition behind the lemma the proof of this lemma okay so let's recall the lemma and first we can assume without loss of generality

that if we look at the automaton of our regular language then directed acyclic graph Duk of strongly connected components of this automaton is a line so i mean strongly connected component transition then a component when a transition and so on so every automaton can be decomposed

in a finite union of such simple automata so therefore we can assume our automaton is of such a form and if we have such a automaton we can define a key notion cone of an automaton and let's look at simple cycles on our automaton so paths from some state q to the same state q

and such a such a cycle is labeled by some word and because this word is over alphabet an it corresponds to some vector so now let's look at these vectors effects of all the simple cycles

in our automaton and let's look at the non-linear combination of these vectors with non-negative real numbers so non-negative linear combinations of these effects and this is what we call a cone of automaton a so it's it can be shown

not not very hardly that such a cone always either equals the whole space d-dimensional or n-dimensional in the case of of yeah so maybe that's a typo it should be rn because our

alphabet is is n-dimensional so such a cone always equals n-dimensional space or is included in some half space and i will not go into details but in but we can show that if cone of some automaton actually equals the whole space then our language

is included in some modular language and in the other case if a cone is included in a half space then we can divide our language into a part which is included in i think one drift language

and another part which stays close to the to the border of this half space and in that case we can use induction assumption for smaller dimensions so actually here we we use an induction over over number of dimensions okay so this is roughly speaking how we have shown

um this lemma so recall one more time this lemma and now our question is we are given a vase and we actually have to tell whether this vase can be

separated by regular language from language that n but because of our lemma this is equivalent to a question whether language of this vase is included in a finite union of modulo and drift languages because only finite unions of modulo and drift languages are regular languages which

don't touch that n language okay so how do we answer this question this is actually quite sophisticated but i will give you a a few ideas how do we test this inclusion so first of all is actually quite similar to the to the proof of the lemma which i just have

mentioned we also look at the cone of a but now a is not an automaton but a is a vase so operating pasting and cutting cycles in advance is not so simple as in the automaton

we have to be much more careful so we use the known tools we use the cal m decomposition lumbered by the composition the kind of the composition which was used to decide reachability problem for vases and based on this column the composition we actually are

we are able to to design the regular language which over approximates our vast language but somehow behave similarly and and based on that we are we are able to

test this inclusion but i don't have time to go into details okay that's all i wanted to say thank you very much