I've been working on Goodful Games automata for a couple of years now. These are automata that are in between deterministic and non-deterministic automata, in the sense

that they allow some non-determinism, but that is so restricted that these automata still have many of the desirable properties of deterministic automata. They can be used instead of deterministic automata in various applications, and at least in the

omega regular setting, they are a way of getting around the need to determinize non-deterministic automata, which, as we know, is hard and expensive and difficult. So last year, I gave a talk about this at the verification group in Liverpool.

This was followed shortly by the following email from Martin.

What we present in this paper is work triggered by this email about what happens if we apply this restriction of Goodful Gameness on the non-determinism in pushdown automata. In the pushdown setting, there's a much bigger gap between non-deterministic and deterministic

pushdown automata, since non-deterministic pushdown automata are much more expressive than deterministic ones, while deterministic ones have better decidability properties. And what Goodful Games pushdown automata give us is a completely new class of languages

that shares some of these nice decidability properties with deterministic pushdown automata while being more expressive. Let's start by going through what it means for an automaton to be good for games, and an example of what a Goodful Games automaton might look like.

So Goodful Gameness is also known as history determinism, which is perhaps a more enlightening name for this type of non-determinism, because we require non-deterministic choices to be resolvable without looking at the future

of the word. What that means is, for example, here we have an automaton that recognizes the language of words in which the pattern aab occurs, and it starts, the first state has a non-deterministic choice when it reads an a of either staying here and

waiting, or moving one state to the right and checking whether we see the pattern aab. So the automaton has to non-deterministically guess when this pattern aab occurs, and that choice requires the automaton to be able to look at the future of the word,

at least the following couple of letters, to decide whether to stay in the first state or go to the right. So this automaton is not good for games. So we formalize this notion of Goodful Gameness with the idea of a resolver. So a resolver is a function that takes the run seen so far in our automaton and the next

input letter, and it returns the transition that we should take. So this is a way of resolving non-determinism only by looking at the past without having any knowledge of the future of the word. And for an automaton to be good for games,

we ask that there should be a resolver that when it reads a word in the language of the automaton, it should be able to build an accepting run in the automaton incrementally while reading this word. So this automaton is not good for games

because our resolver would need to make a different choice depending on what the next couple of letters are, rather than the past of the word. However, we can make this automaton good for games by adding a couple of transitions. So in this new automaton,

we still have this non-deterministic choice, but now our resolver can tell us to always try to go to the right, always try to check that we see the pattern AAB. If it made a mistake, that's fine. The B will take us back to the initial state,

and if we do see AAB, we get to go to the accepting state, and if we see too many A's, then we have this third state in which we can wait for a B to occur. Now this good for games automaton is almost a deterministic automaton. It just has

this additional loop on an A in the first state, which as our resolver tells us, we don't actually need. So in this case, we can use the resolver to determinize the automaton by removing any transitions that our resolver doesn't actually use. So far, good for games

automata have been mostly studied in the setting of regular automaton. Here we can get around determinization. It is easier to turn an automaton into a good for games automaton

than it is to determinize it, and in some cases a good for games automaton can be exponentially more succinct than any equivalent deterministic automaton. So that's the situation in the context of omega regular automaton. So our first result in the context resetting,

where non-deterministic pushdown automata are more expressive than deterministic ones, is that good for games automata are indeed more expressive than deterministic ones. Our proof of this result is inspired by a result of Kupferberg and Skripjak showing an exponential

succinctness gap in the omega regular setting. We use the alphabet containing plus, minus, and zero, and can now assign an energy level to every word over this alphabet,

which is defined as follows. We start with zero, and whenever we see a plus, we increment the energy level by one. We see a minus, we decrement the energy level by one, and a zero doesn't change the energy level. Now this allows us to define the language safe of all infinite words

over the alphabet sigma whose energy level is always non-negative, so it never goes below zero. And it's not hard to see that the language safe is omega context-free. So down here you

have an automaton that essentially keeps track of the energy level. Whenever you see a plus, you push an x on the stack, no matter what is currently on top of the stack. If you see a minus and there is still an x on the stack, you pop it, and if you see a zero, you leave the stack

unchanged. You don't need more than one state. All the information is stored on your stack. Now consider the language finally safe of all those words that have a suffix in safe. So at the beginning you might have some prefix where you have more minuses than pluses,

but after some point you have an energy level which is always strictly non-negative. And now here is a pushdown automaton recognizing the language finally safe.

You essentially just have a loop at the initial state where you can ignore any prefix and then you non-deterministically decide to go to the second state and start keeping track of the energy level. Notice that this automaton is not good for games as it is,

because you need to make this choice from going to the initial state to this right state. And this can only be done when you have a position where a safe suffix starts and making

that decision requires knowledge about the future. But we can turn this automaton into a good for games automaton, essentially using the same trick we saw in the introductory example, we just add a transition for the error case, namely when we want to process a minus

when the stack is empty, which would mean we go to a negative energy level, and in that case we just leave the empty stack unchanged and go back to the initial state,

essentially allowing for restart. Now with the kobishi condition, which says eventually we have to stay in the rightmost state so we can only restart finally often, this means that at some point we did a last restart and then process a safe suffix in the right state. Now for the

product alphabet, so in both components we have a letter from sigma, and now we consider the

following language, call it safe component, of words over this product alphabet where at least one of the components, so either the word in the upper component or the word in the lower component, has a safe suffix. This is the language that can be recognized by a good for games automaton,

but not by a deterministic pushdown automaton. So what you can do to obtain a good for games automaton for the language is essentially use two copies of the automaton that we saw earlier,

one for the upper component on the left side and one for the lower component on the right side, and then you can switch between these copies. And a priori this is a non-deterministic switch, but the resolver can resolve the non-determinism by always keeping track of the oldest

safe suffix, so the one that is from the current position the longest that is still safe.

And one can show that this is indeed a resolver that works for the language of this automaton, which shows that the language is indeed recognizable by a good for games pushdown automaton. On the other hand, a pumping argument shows that there is no deterministic automaton

recognizing this language, because with one stack and determinism you cannot recognize in which of the two components you have a safe suffix. With non-determinism it's easy, but with

determinism you just have to keep track of both energy levels and this is impossible on one stack. What we have seen is that good for games pushdown automata are strictly more expressive than deterministic pushdown automata. The next obvious question is how

expressive are they? And it turns out that they are strictly less expressive than non-deterministic pushdown automata. And there are actually at least three ways to prove this result. So you can base your proof on the language of palindromes. This is a classical

example of a language that is not deterministic context-free, but context-free. And this proof can be also formulated for good for games pushdown automata because what you use here

is the fact that on a prefix you have a unique run. In a deterministic automaton, because you only have one run, in a good for games automaton, because you have this resolver which gives you a unique run. Similarly you can use the language a to the n, b to the n,

union a to the n, b to the 2n. Another classical example which is context-free but not deterministic context-free. And again the same property allows you to show that the language is not good for games context-free. And the final language

for which we were able to show that it's not good for games is the following one. It's a variant of what we saw earlier. You only have pluses and minuses and you ask for the existence of some energy level n such that you have infinitely many prefixes that have exactly that

energy level. And it turns out that this language is not good for games, but it is known that it is visibly pushed down. So this language can be recognized by a visibly pushed down automaton

which means we have a separation between the good for games languages and the visibly pushed down languages as well. And overall we have the following diagram. We have the languages

recognized by omega pushdown automata, by good for games pushdown automata, and by deterministic pushdown automata, and they form a hierarchy. And then we have the class of languages recognized by visibly pushed down automata. It's a subclass of the

languages recognized by pushdown automata, but it's incomparable to the good for games automata. So now we have a clear idea of the expressivity of good for games pushed down automata.

So let's talk about what these automata are actually good for. As the name suggests, these automata are useful for solving games. Here we talk about games where the winning condition is given by a pushdown automaton. So these can in theory be games with or without an arena.

In this example we have an arena of which the positions are partitioned between our two players and the edges are labeled with words from some input alphabet. So a play here is an infinite path throughout this arena, and one of the players will win if the labels along that path give us a

word that is in the language, and the other player wins if the word is not in the language. Now if this language is given to us by a deterministic pushdown automaton, then this is decidable. If the language is given by a non-deterministic pushdown automaton,

then this problem is undecidable. And here we show that for good for games pushed down automata, this is also decidable in X-time, as is the case for deterministic pushdown automata. The universality problem can also be reduced to solving games. So universality, which is

undecidable for non-deterministic pushdown automata, and X-time complete for deterministic pushdown automata is also decidable in X-time for good for games pushdown automaton. Here we have a table that summarizes both the expressivity results and the complexity results.

So we have a class of languages which is more expressive than deterministic context-free languages, but has the same nice decidability properties with respect to solving games and universality. This would be a good place to stop,

but I'm afraid Martin wants to mention some of the bad news. I guess I have to. So let's start with closure properties of this new class of languages. While the deterministic context-free languages and the context-free languages have some closure

properties, and the visibly pushdown languages actually have quite a lot of closure properties, it turns out that the good for games languages don't have any closure properties. So no union, no intersection, no complementation, and so on. The only thing that does hold is

closure under intersection with omega-regular languages and union with omega-regular languages. Secondly, coming to decision problems, the situation is also rather bleak.

Unfortunately, it is undecidable to determine whether a given non-deterministic pushdown is good for games. The problem being that good for gameness is a semantic

notion. So you ask for the existence of a resolver, and it turns out that this is undecidable. Similarly, deciding whether the language of the automaton is good for games,

so equivalently whether there exists an equivalent good for games pushdown automaton, is also undecidable. So to summarize, we can't decide whether a given pushdown automaton is good for games, nor whether it can be turned into one that is good for games, and if we

happen to get our hands on a good for games pushdown automaton, we have to be very careful with it since this is a class that doesn't have any nice closure properties. Not all bad, one can still manually show that an automaton or a class of automaton is indeed good for games, and there's some hope that we can find a syntactic subclass of good for games pushdown

automaton that we could then use to write specifications directly into good for games automaton. Other potential open problems include whether universality is x-time complete. In the paper we only show membership in x-time, but not hard and easy.

We also left as an open question what kind of resolvers pushdown automaton need. Is there a limit to their complexity, or can we always implement the resolver with say a

deterministic pushdown transducer? In the paper we only address pushdown automaton over infinite words, but the same questions are also valid over finite words. It seems from current work that in the case of finite words we will also get an expressivity gap between deterministic

and good for games pushdown automaton, but that's a story for another time. That's all we have to say about good for games automata for now. Thank you for watching this presentation. We look forward to discussing good for games automata with you at the Q&A next week. Meanwhile, if you have any pressing good for games questions,

here are our email addresses. We're very happy to receive any good for games distractions during this lockdown. See you next week.