Hello. In this video, I'd like to tell you about the Church's synthesis problem adapted to the setting of timed automata. The presentation is based on a paper titled Timed Games and

Deterministic Separability that I co-authored with Lorenzo Clemente and Swavo Milasota. We all work at the University of Warsaw, Poland.

I am Radosław Pierkowski and this is Timed Church's synthesis problem. In this video, I'd like to answer three questions about our work. First, what exactly did we do?

Next, how is it different from what has been done before? Finally, why we think it can be useful? Time is short, so let's just jump straight to the first question.

In a nutshell, the answer is as follows. We generalized the Church's synthesis problem to the setting of timed automata. And we also proved an analogue of the famous Bihiran-Webel theorem, the. As you can see, there are three things in both here.

And I owe you some explanation to each one. Let us start with the Church's problem. This problem was first stated by Alonso Church in 1957. Now, it is seen by many as a cornerstone of the program synthesis.

It is defined as follows. Given a specification of some sort, does there exist a controller such that for every possible input it will produce results matching the specification? I would like to present it visually the following way.

We are given a green machine, a specification. And it is fed with an infinite word of pairs of letters. It reads the word letter by letter. And finally, when it reads the whole infinite word,

it answers either accept or reject. But that is only a part of our pipeline. In fact, the input here consists only of a single string of letters.

So clearly, something is missing here at the middle. And the missing part is a controller. This is a very simple machine, a letter-to-letter transducer to be exact. It reads the input and based on its internal state and the input letter it just read,

it produces a new letter of this upper string here. As you can see, it operates on a letter-to-letter basis. That is, for each letter of the input, it produces exactly one letter of that upper string here.

Let me now repeat the formulation of the Church's problem. We are given a specification and we ask whether there exists a controller here such that for every possible input here, the results of the controller,

together with the input, will be accepted by the green specification. We may also look at this problem from the viewpoint of the game theory. Now, what we get is a winning condition here

and two players, controller and the input player. For the sake of this presentation, I will have to take the role of the input player. A single turn of this game looks as follows. First, I, as the input player, can produce a next letter of the input.

Then, the controller needs to produce its answer to my input. Observe that the question of the existence of a finite memory strategy for the controller is now exactly the same problem as the Church's synthesis as defined before.

Now, there's an important theorem by Behe and Landweber. It says that if the winning condition is specified by a omega-regular language, then it's actually decidable whether a winning strategy for the controller exists.

And if it does, we can also synthesize a finite memory one. As I mentioned earlier, we generalize the Church's synthesis problem to the setting of time to automata and we prove an analog of the Behe-Landweber theorem there.

So now, let me show you how we generalize our pipeline to the world of timed automata. For those of you who know timed automata, our derivation of timed synthesis game should be quite straightforward.

We just replace the models here with the timed counterparts. So, a finite omega automaton here is replaced with a timed automaton and also a finite transducer is replaced with a timed transducer.

If you don't know timed automata, don't worry, the change is actually very easy. We did that in three steps. First, we add the timeline to the input here. Now, every symbol is associated with a particular position on that timeline.

I, as the input player, can synthesize a new input at the bitrary non-negative offset from the previous symbol. For example, here. Now, the controller needs to wait a moment before it sees the next letter. I can also select some different offsets and put, for example, A here.

The only requirement is that I have to put the new input letter not before the previous one. An important remark here is that those two devices do not have a direct access to the timeline.

They don't see the exact time values of the input symbols. Therefore, they need some different way of measuring time. That's why they are given clocks. For the sake of simplicity, in this presentation I chose to give them only one clock each.

But in general, those machines can have arbitrary numbers of clocks. How does a clock look like? Well, it has a hand here, and when we let the time flow, the hand moves. The owner of the clock can measure time relative to the integer values written on the face of the clock.

For example, if the hand is between 3 and 4, then the owner knows the interval, but the exact time value is not known for him. Additionally, when the measured time exceeds the maximal constant written on the clock, in this case 6, the hand stops.

Now, all that the owner knows is that something above 6 was reached, and nothing more. How the readings from the clock can be used by the controller?

The controller has its strategy here. It is a simple graph of states with transitions between them. Now, the controller may use different types of transitions, that is, timed transitions.

A timed transition, for example, may say the following. If you are in the state p, and your clock shows something between 5 and 6, and additionally the input you have observed is a, then you can output x and go to the state q.

Additionally, a timed transition may also decide to reset a clock, that is, set its value back to 0. Take a look at this example. Assume that this clock has just been reset. Now, when we let the time flow, the clock begins to measure it.

The controller only stops when it sees the next input letter. Now, it can look at its clock, and the decision what letter to produce here can depend on the interval observed on this clock.

And that's basically all that changes when we move to the timed setting. So, to sum up, we have a player input that now plays timed symbols. Both of these machines are given clocks, and to use them they may use timed transitions that speak about the values of the clocks.

So, effectively, what we get here is a timed amiga-regular language here, and a timed letter-to-letter transducer as a strategy of the controller. So, this is how our timed synthesis games are defined.

But before I can tell you exactly what we proved about them, I need to be a bit more formal. Let me state the synthesis problem for our timed games. As before, we are given a specification, which is now a timed amiga-regular language. Our objective is to synthesize a timed letter-to-letter transducer, which is a winning strategy for the controller.

However, there are a few new design choices we need to make because of the addition of time. First of all, now we may wish to specify whether the winning condition describes desired or undesired behaviors of the controller.

In the original setting, we had the amiga-regular language here, and those are close under the complement, so this was not a problem earlier, but unfortunately it is not the case for timed automata. We may therefore want to use a condition that tells us either when the controller wins or when the controller loses.

The other choices are related to the clocks of the controller. We want to synthesize a timed transducer that uses those clocks. So, we may wish to fix the number of the clocks the transducer can use, or leave that unspecified.

Similarly, the clocks count up to some constant m, and we may want to specify that constant in advance or quantify it existentially. Before I can tell you what is the set of choices that we made here, it is best to first show what has been known here before.

So in fact, the answers for those two questions now intertwine. Let us construct a table summarizing some of the possible choices here. As columns, we'll have the type of the winning condition to be used, that is, with specifying desired or undesired behaviors of the controller.

The additional column here, deterministic, is a simpler case because the deterministic timed automata can be complemented.

The rows in turn correspond to the choices about clocks. We analyze the following three, when both constants are fixed, when only the number of clocks is fixed, and finally, when no constant is fixed. First of the known results is a decidability of the simple case here, where all parameters are fixed and the condition is deterministic.

Later, two other decidability results were shown, together with three undecidability results. As you can see, the second row wasn't considered before, but its first two cells can be easily filled up as follows.

There's only a question mark here. Our model is essentially a slight restriction of this setting, and our results concern the last column of this table.

First of our results, a kind of byproduct, resides here. Our games are a bit simpler, in fact, so actually the previously known result is stronger. However, our result has a simpler proof. For exactly the same reasons, our undecidability result here is stronger than the previous one, because we proved it for the simpler games.

Finally, our most important contribution is here. We are able to decide the winner and synthesize a controller when only the number of clocks is fixed, but the constant the clocks can count up to is arbitrary.

This is an important novelty, because earlier those two numbers were either both fixed or not. So this concludes the answer for the two questions here.

Let me now tell you why we think our results are interesting. Here the answer is because they allow us to solve another interesting problem about timed automata, the deterministic separability question. What is deterministic separability? Well, it's a very simple and natural problem.

We are given two automata, A and B, which are non-deterministic, and their languages do not intersect. We draw it like this, where those rectangles here are languages of A and B. And this black rectangle is just the set of all possible timed words.

So the question is now whether there exists a separator, a simpler deterministic automaton, that separates A from B. Now using our results from the table, we may solve this separability question as follows. So we use those two results to solve those two separability questions.

As you may have already figured it out, the separability problem is parentized by the same set of choices that we made in the case of synthesis. Note that here the open problem is this. The separability without fixing the resources.

Why is so? Our undecidability for games does not transfer to the separability question, and we don't know any techniques other than games that the separability reduces to. For me, the second decidability result here is more interesting because we don't need to specify the constant for clocks in advance.

For example, we don't need to specify the constant 6. You may wonder why we think the separability is interesting. One of the reasons is simply the fact that it is decidable. Many other problems for timed automata are not. In particular, a related problem of DTE membership is undecidable.

The other results include universality, complementability and language inclusion. In fact, we've been very lucky that the games that we solved separability with turned out to be using this variant of the winning condition.

If they used the other one here, we couldn't even decide them. Speaking of games, our game for separability is very simple. As before, there is a timed input here. The actions of controller are very limited though. It can only play accept or reject symbols.

Conceptually, he wants to prove that he knows a separator. To this end, he classifies the prefixes of the input word based on whether they belong to the red language or not. In turn, the specification describes the undesired behaviors of the controller.

For separability, there are two cases. Either something that should have been accepted is not accepted or something that shouldn't have been accepted was. It turns out that this simple game characterizes exactly the separability question. Then, using our result, we may solve that question when only the number of clocks is specified in advance.

I think this application shows well that our results are useful. We hope that more interesting applications will follow. Now, it's time to summarize what I have told you in this video. First, I showed you how we generalized the Church's synthesis problem to a timed setting.

Later, I showed you our results in the context of the previous knowledge. Finally, I explained how our result is used to solve an interesting question of separability. Should you wish to learn more about our work, please visit my webpage here.

Now, thank you for your attention and have an inspiring time at iCalp, especially in this year's unusual circumstances. Thank you.