where *a* ∈ AP is an *atomic proposition*, inducing the *alphabet* Σ=2AP. These formulae are interpreted over infinite sequences *w* ∈ Σ*ω* called *ω*-words. A word *w* = *w*0*w*1 ··· ∈ Σ*ω* satisfies the *next* operator **X***φ* iff *φ* is satisfied in the next step. Similarly, the *until* operator *φ***U***ψ* is satisfied iff *φ* holds until *ψ* is eventually satisfied. Usual abbreviations are defined as *finally* **F***φ* ≡ tt **U** *φ* and *globally* **G***φ* ≡ ¬**F**¬*φ*, which require that *φ* holds at least once or always, respectively. Moreover, the construction underlying our work also considers *strong release φ* **M** *ψ* ≡ *ψ* **U** (*ψ* ∧ *φ*), *(weak) release φ* **R** *ψ* ≡ **G***ψ* ∨ (*φ* **M** *ψ*), and *weak until φ* **W** *ψ* ≡ **G***φ* ∨ (*φ* **U** *ψ*). Considering these additional operators allows formulas to be represented in *negation normal form*, i.e. the negation ¬ only appears in front of atomic propositions. In the interest of space, we refer to [12] for precise definition on the semantics and discussion of these subtleties. Understanding these issues is however not required for this work.

*LTL Synthesis* is an instance of the general synthesis problem, where the specification to be satisfied is given in form of an LTL formula [38]. Due to recent advances [11,12,16,20,21,25], the *automata-based approach* [43] to LTL synthesis received significant attention. In particular, the tool Strix [33], built on top of Owl [24], which in turn implements these ideas, won several iterations of the synthesis competition SYNTCOMP [18]. Essentially, the given LTL formula is translated into an *ω*-automaton, which in turn is transformed into a parity game. Solving the resulting game yields a solution to the original synthesis question.

This game is obtained by "splitting" the automaton, as follows. The set of atomic propositions is split into system- and environment-controlled propositions, i.e. AP = APS ∪ APE , and the players' actions correspond to choosing which of their propositions to enable. Once both players chose their propositions' values, the automaton moves to the next vertex according to the players' choices. Concretely, for an automaton state *p*, the environment can choose to move into (*p, v*) where *v* ⊆ 2APE , and from there, system can move to any automaton state *q* = *δ*(*p, v* ∪*v*) where *v* ⊆ 2APS and *δ* is the transition function of the automaton. In particular, this means that the obtained game is *alternating*, i.e. system and environment take turns in alternation. Moreover, by convention the environment moves first. See e.g. [33] for more details on this approach.

*Semantic Translations* from LTL to automata are the key ingredient to our approach. On top of providing a parity game, they also give a *semantic labelling*,

**Fig. 3.** Motivational example to provide guidance through semantic labelling.

i.e. interpretable meaning, to the game's vertices. In particular, the approach introduced in [8] (see also [10–12]) and implemented in Owl [25] intuitively yields for each vertex a list of LTL formulae, which roughly correspond to (sub-)goals which still have to be fulfilled, possibly repetitively.

#### **2.3 Our Goal**

In this work, we want to demonstrate that this semantic labelling can be efficiently exploited for reactive synthesis. For a motivational example to consider semantic labelling, we display a (vastly simplified) labelled game in Fig. 3. We are offered with the choice of choosing *a* or ¬*a*. While it is not completely clear that choosing *a* is indeed better, it certainly seems to be more promising, as the subsequent labelling seems much "easier" to handle. Thus, faced with a choice, we likely would first try to win with *a*. Observe that without the semantic labelling, our best option in this situation would be a random guess. In [22], the authors used a simple, manually designed mechanism trying to capture this notion, called *trueness*. Motivated by the (surprisingly good) results of this approach, we want to tackle this problem by more sophisticated means. Concretely, we want to make meaningful decisions based on the labelling. However, while the theory underpinning semantic translations is quite clean and pleasant [12], the actual labellings appearing in practice are quite complex. To further complicate things, the highly optimized implementation thereof [25] employs several subtle optimizations and special cases. We provide an example to showcase the complexity of this labelling in practice later in Sect. 5, kept brief in the interest of space, and a small real-world example in [23, Appendix A.1]. Since we have a simple intuition which however seems difficult to formalize, we opt to tackle this problem through means of machine learning.

#### **3 Previous Approaches and Their Limitations**

In this section, we briefly summarize the ideas of [22] and the inherent problems associated with them. The primary motivation of [22] is to exploit the semantic labelling provided by [25], which gives us an indication of the long term goals in the game. As an analogy, consider the game of chess. Here, the "semantic labelling" is given by the board state, i.e. the position of each piece. This labelling provides us with a reasonable indication of (i) our current situation and (ii) which moves might be better than others. In particular, understanding and evaluating the semantics of the game is what allows humans to have a good intuition about the quality of moves, without thinking through the intractably large game tree. Likewise, this understanding is what enabled algorithms to perform beyond human capabilities.

#### **3.1 Parity Game Solving by Trueness**

A central notion of [22] is *trueness*, an approximation of how close a formula is to being satisfied, i.e. tt. The intuition is that the semantic labelling of states effectively describes "goals" of the system player. If the formula is tt, the system has satisfied all goals and consequently won the game. Likewise, increasing the trueness is indicative for a good move. Remaining with the analogy of chess, trueness somewhat corresponds to counting the number of pieces on the board (or rather the difference between our and the opponent's pieces): If no enemy pieces remain, we certainly have won, and a change of this difference, i.e. capturing an enemy piece or avoiding capture of own pieces, is a good indicator for the quality of a move. In particular, this prohibits us from taking moves which immediately lead to a piece being taken.

In [22], the authors propose two ideas. First, they suggest to use a truenessmaximizing strategy as initial one for strategy iteration, i.e. in each state select the edge which maximizes (or minimizes, in the case of E) the obtained trueness. Second, they use *Q-Learning*, a popular reinforcement learning approach, as a solver for parity games, i.e. as competitor to strategy iteration, using three different reward signals. There, each edge is given a reward, which is mostly based on (the change of) trueness, and these values then are back-propagated until choosing optimal rewards in each step yields a winning strategy.

While they also show Q-Learning to be an interesting avenue, we primarily focus on the "initializing strategy iteration" approach, since our goal is to augment exiting strategy iteration solvers. Moreover, the experimental evaluation of [22] suggests that Q-Learning scales poorly to large real-world formulae.

#### **3.2 Problems**

We now outline two key issues of this approach.

We proceed to outline how we tackle these issues by a more sophisticated approach.

#### **4 A New Hope**

We want to improve reactive synthesis by applying machine learning. As already motivated by [22], we want to approach this problem by identifying "promising" edges, choosing those as initial strategy for SI. Naturally, as a first step, we need training data for our learning approach. In particular, we need to identify which actually are the actual good choices in games, i.e. the *ground truth*. As it turns out, this is more complicated than one might expect.

#### **4.1 Obtaining Training Data with SI**

As SI allows us to solve a game and determine winning edges, one might try to employ SI for obtaining a ground truth (as we did initially). However, SI actually provides us with potentially misleading or even conflicting information! As we already hinted in the introduction through Fig. 1, SI cannot give us a canonical ground truth. In the example, one edge is winning iff the other is not used, and vice versa. Thus, SI will yield a strategy which does not take both edges and we would consider one of them losing. Moreover, note that there is no fundamental reason to prefer one edge over the other, so SI might in one run classify the edge from *v*2 to *v*3 as good and in a second run (or on a similar game) do the opposite or even consider neither winning. The underlying problem is that parity games do not allow for a unique *maximally permissive* strategy (see e.g. [3]), thus we cannot derive the "suitability" of an edge from a single solution strategy.

#### **4.2 Solving the Game Tree**

Instead of using a particular strategy obtained from SI, we therefore propose to identify "all" solutions, i.e. all edges which are part of a winning strategy. More formally, for each vertex *v* we want to determine the value of each outgoing edge in the corresponding game tree rooted at *v*. To prefer "shorter" solutions over larger, we add a beta-decay to the value. Concretely, suppose we consider the game tree state *s* = (*v*1*,...,vi*) which ends in a system state *vi*. Then, the value of *s* is defined by val(*s*) = *β* · max*s*-∈successors(*s*) val(*s* ) for a fixed 0 *<β<* 1.

As we already mentioned, evaluating this tree is intractably large, namely exponential in the size of the game, which itself is already doubly-exponential in the input formula [27,38]. Thus, we employ a classical technique of game theory.

#### **4.3 Monte Carlo Tree Search (MCTS)**

Intuitively, we explicitly unfold the tree up to a specified depth, e.g. 7 plies, and then assign the results of (guided) random sampling to the occurring leaves, approximating the (beta-decayed) value of the game in these vertices.

We describe our method to approximate the value of a node *s* = (*v*1*,...,vi*) in the game tree. In essence, starting from *vi*, we randomly select successors, with the following restrictions for each player. The environment plays *optimally*, i.e. if a state is winning for the environment (which we can determine beforehand through classical approaches) we immediately stop sampling and return a value of 0. Otherwise, the environment heuristically tries to delay the play as long as possible (decreasing the value the system player obtains due to beta-decay). In contrast, the system player checks in a one-step lookahead if a choice is trivially winning, i.e. leading to a state labelled tt, always choosing such an edge if one exists. Otherwise, the system randomly chooses among edges which are not trivially losing, i.e. lead to a ff state. If either player closes a loop, i.e. selects a successor which already occurs along the path, we determine the value by checking if the loop is winning or losing. A loss yields a value of 0, while a win yields *β*length. In summary, we approximate the probability of winning by playing randomly (avoiding obvious mistakes) against an optimal opponent, under-approximating the true value. We deliberately opt for this random-choice approach to prefer regions where there is less potential for error.

#### **4.4 Optimizations**

While MCTS makes approximation of the game tree value feasible, we added several further technical improvements to arrive at a practically viable method.

*SCC Decomposition.* We exploit the structure of the game by decomposing it into its strongly connected components (SCCs) and put them in reverse topological order. Computing (or approximating) the value in that order allows for caching: Once a run in the game tree leaves an SCC, it can only reach SCCs further down in the topological order, and, since we compute values in this order, the value of the reached state is already known, allowing us to re-use it immediately.

*Pruning.* In addition to employing the MCTS values as game values in the tree expansion, we also use it to prune the game tree. In particular, once we computed the Monte Carlo values for each state, we restrict the choice of the environment to the successors which yield (close to) the lowest Monte Carlo value (recall that the environment prefers lower values). We empirically chose 0*.*02 as a threshold, i.e. we only keep those edges for the environment which are within 0*.*02 value of the lowest decision. While in theory this might remove crucial paths due to statistical fluctuations of MCTS, in practice it allows for a much deeper game tree, which in our experiments heavily outweighed the theoretical downside.

### **5 Handling the Truth**

We introduced a way how to obtain a well-founded notion of "value" (to be precise, an approximation thereof) for a choice, i.e. an indication how good this choice is. As such, we can rank edges by their value in each state. Intuitively, picking an edge which is ranked very highly should correspond to a good chance of winning. A high value means that even against an optimal player we can very likely close a winning loop, and, due to beta decay, do so quickly, thus minimizing the chance for an error.

Recall that our goal is to provide a good initial strategy. Thus, the exact values actually are irrelevant, since we only want to give the best edge as initial choice. Instead of trying to predict the exact value, we therefore want to learn this relative ranking. Formally, suppose we consider a system vertex *v* ∈ *V*S with edges *Ev* = {(*v, u*) | (*v, u*) ∈ *E*}. A ranking of edges effectively corresponds to a (total) order ≺*v* ⊆ *Ev* × *Ev*. The principle of *pairwise ranking* [30] suggests that we learn a function *f* : *Ev* × *Ev* → {−1*,* 1} that classifies pairs of edges depending on which one is the better choice, i.e. *f*(*e, e* ) = 1 if *e* ≺*v e* and −1 otherwise. However, such a function might not be perfect. For example, we could get *f*(*e*1*, e*2) = 1, *f*(*e*2*, e*3) = 1, and *f*(*e*3*, e*1) = 1, which is incompatible with any order. Thus, learning to rank suggests to determine an ordering ≺ that minimizes the *inversions* w.r.t. *f*, i.e. the number of cases where *f*(*e, e* ) = 1 but *e* ≺*v e* . This problem, called rank aggregation, is known to be **NP**-hard, and we employ a greedy approximation as suggested by [30].

Our concrete goal thus now is to learn such a function *f* based on the semantic labelling of the start and end vertices of the two edges. We want to employ machine learning for this purpose: While the high-level intuition of the semantic labelling is rather clear, the actual implementation used to obtain the games [24] employs numerous optimizations, separate cases, etc. To provide the reader with a sense of the complexity, we display a single edge in the automaton obtained for a simple formula in Fig. 4, and a real-world scenario in [23, Appendix A.1].

**Fig. 4.** A single transition in the automaton computed for the formula (*a*∧**G***b*)∨**GF***c*.

We proceed to describe (i) (some of) the features we use, i.e. which quantities we extract from the labelling, (ii) the model we employ, and (iii) the dataset and methodology used to train our model.

#### **5.1 Features**

In total, we have defined over 200 different features to convert the edges into a usable vector of reals. In the interest of space we only present the high-level ideas of a small subset which covers most interesting ideas.

Since most information is contained in the states rather than in the edges themselves, the majority of our features are defined for the former. An edge is then either associated with the feature value of its successor or with the change in a feature value between its predecessor and successor. As indicated in Fig. 4, the semantic labelling comprises several formulae, namely a "master" formula, which intuitively indicates the global state, and several "monitors" (which themselves comprise several formulae), monitoring repeating sub-goals. We define *base features*, which convert a single formula to a single number. These features can then be applied to both the master as well as monitor formulae, where further aggregation is necessary. Some notable base features are the following:

their trueness) and aggregate by weighted average (rather than maximum). Additionally, we introduce punishments for failing monitors. Intuitively, this encourages long-term progress for temporal goals.

**One Step** Here, the idea is to recommend an assignment that is to be played in the current state by traversing the syntax tree and propagating recommendations upwards, which is inspired by message passing in graph neural networks. For example, if we see *a* ∧ *b* we strongly recommend playing *a* and *b*, if we see **F**(*a* ∧ *b*) we take the previous recommendation and tune it down, since **F** is "less urgent". The feature value is obtained by measuring how well the valuation of an edge aligns with the recommended assignment.

#### **5.2 Pair Classification by Support Vector Machines**

To instantiate our pair classification function *f*, we opt for support vector machines. In principle, one could employ any binary classifier, which is why we also experimented with other models such as decision trees, random forests or gradient boosted trees. However, SVMs proved to perform best, which we attribute to their great ability to generalize due to their margin maximizing nature [30]. Additionally, SVMs are rather simple (compared to our other options) and provide us with extra information known as *confidence*. Given by the distance of the predicted sample to the decision hyperplane, its magnitude can be interpreted as how confident the SVM is in its prediction. We denote the confidence of a pair (*e*1*, e*2) by *c*(*e*1*, e*2) and use it to slightly alter the greedy ranking algorithm from literature. To rank the edges of a vertex *v*, each edge *e* ∈ *Ev* gets assigned a score *s*(*e*) = - *e*-∈*Ev,e*-=*e c*(*e, e* ). Recall that if we predict *e* ≺*v e* , the confidence is negative. Finally, we rank the edges according to their score, where a higher score corresponds to a better edge, and the recommended strategy is obtained by playing the highest ranked edge for each state.

#### **5.3 Further Notes on Implementation**

In addition to the feature extraction, there are several other engineering aspects, which are crucial for the final performance. In this section, we comment on the three most important ones.

*Statewise Feature Normalization.* Before passing the features to the model, we proceed to normalize them. Due to possible future applications in on-the-fly solvers, we only consider feature values of edges from the same state for this normalization. The crucial observation is that this already introduces comparative information in the features. A normalized trueness value of 1, for example, means this edge has the best trueness among all other edges from their state although it does not tell us anything about its absolute value. While the latter might also be important in theory, we observed that in practice the statewise normalized value is more important with only a few exceptions.

*State Classification.* We observed several significantly different behaviours required in different states. For example, in some states we need to exclusively focus on the master formula, while in others only the monitors play a role. This also relates to the underlying principles of the automaton construction. It is very difficult, especially for a simple model like an SVM, to switch between different behaviours. We divide states into three groups which approximate the different classes, and train separate models for each class. The three classes we suggest are (i) states without monitors, (ii) states where the master formula does not change in any successor, (iii) and states that fall into neither category. In addition to having the separate models learn separate behaviours, we can also provide them with separate feature sets that only include relevant information. For example, the first class only requires features of the master formula, whereas these can be neglected in the second one.

*Complement Construction.* The underlying automaton construction uses the fact that the system being able to enforce satisfaction of a formula *ϕ* is equivalent to the environment being able to enforce falsification of ¬*ϕ*. In other words, solving the game for the negated formula and swapped roles yields the same result. However, in the game obtained for ¬*ϕ* the role of "system", the player who choses second and for which we learnt the recommendation, i.e. for transitions from states (*p, v*) to *q*, now corresponds to the original environment. This drastically changes the meaning of features. For example, a trueness of 0 suddenly is very desirable. We tackle this by training separate models for both cases. Together with state classification, this yields a total of 6 different models that we assemble for our heuristic.

### **5.4 Training the Model**

With these ideas at hand, we conclude this section by discussing our dataset, in particular how we preprocess it, and how we train our model.

*Dataset and Preprocessing.* As one of our goals is to exploit human bias in writing LTL formulae, the foundation of our dataset is given by the LTL benchmarks of SYNTCOMP.2. To further augment the data, we mutate these formulae by randomly replacing temporal operators. This yields new (random) samples that syntactically resemble the original, human-written structure. For practical reasons, we only consider formulae which can be converted to a DPA within 10 min. Ultimately, this leaves us with 405 original and 514 mutated formulae, of which we use 60% each for training, 20% for validation, and 20% for evaluation.

Obtaining the edge pairs for training requires several further steps. First of all, we exclude trivial cases that can easily be detected by simple rules (see Sect. 4.3), allowing our model to focus on complicated cases. Further, we exclude pairs where the ground truth value happens to be equal, as it is unclear which edge the model should predict. In particular, we exclude all edges originating in losing

2 Available on GitHub https://github.com/SYNTCOMP/benchmarks.

states (since there is no sensible action to recommend). Finally, we only include a limited amount of pairs per game in the training set: Pairs of the same game tend to look similar, thus a few disproportionately large games would result in a very unbalanced dataset. All remaining edge pairs are added in both orders, i.e. ((*e*1*, e*2)*, y*) and ((*e*2*, e*1)*,* −*y*), where *y* ∈ {1*,* −1} determines which edge is better, in order to prioritize teaching symmetry to the model.

*Training.* For each of the 6 models, we first compute mean and standard deviation of the respective training set and use them to standardize the input to N (0*,* 1). Further, we perform recursive feature elimination for each state class individually, adapted to features appearing twice (once for each input edge). For each state class, we ended up with 30–40 features.

For the actual training process, we performed an extensive grid search for several model types (decision trees, random forests, etc., see Sect. 5.2) in order to determine suitable values for the hyper-parameters. As mentioned earlier, we ultimately opted for the SVMs due to their simplicity and generalization abilities.

#### **6 Experimental Evaluation**

In this section, we present experimental evaluation of our tool SemML. The model was learnt by communicating the relevant data to a Python process running scikit-learn [35]. We then extracted the learnt weights and, based on them, implemented the recommendation procedure in Java, on top of Owl [24]. The artifact can be found at [1], which references a slightly improved version from the one we submitted to the artifact evaluation [2].

#### **6.1 Evaluation Goals**

Our primary goal in this work is to show that our approach, enabled by our new ground truth, can be used to solve more complicated instances than the approach of [22], in particular formulae going beyond pure (co-)safety. Thus, our first evaluation goal is the following:

*Research Question 1:* How much does our model based on SVM and the game tree ground truth outperform the trueness-based initial strategy recommendation approach of [22]?

We refer to the trueness-based initial strategy of [22] as TrueSI.

Although not the focus of this work, we ultimately want to improve synthesis through meaningful exploration guidance, in particular, by suggesting likely winning edges. Thus, we are interested how our prototype performs in a real-world scenario.

*Research Question 2:* How do initial strategies recommended by our approach synergize with state-of-the-art synthesis tools?

We address both questions separately.

#### **6.2 RQ1: Quality of Initial Strategy**

*Datasets.* To fairly compare to [22], we consider the same dataset, i.e. randomly generated LTL formulae, split into three categories: "(Co-)Safety", "Near (Co- )Safety", and "Parity". See [22] for details on how these are obtained. In essence, the tool randltl [7] is used to generate random formulae with different biases. Then, we filter out formulae which need more than 10 min to be translated to a parity automaton. As a second dataset, we also use some (original and mutated) SYNTCOMP formulae (the test set described in Sect. 5.4). We only consider formulae where the corresponding game can be won by system. We do this simply because we can only recommend on games which are winning – otherwise there is no preference on edges since every action is losing by definition. In total, this leaves 262 randomly generated formulae and 123 from SYNTCOMP.

*Metrics.* We consider two metrics for our comparison. Firstly, similar to [22], we consider the fraction of *immediately solved* games, i.e. games where following actions recommended by SemML or TrueSI directly yields a winning strategy. In light of our motivation to augment SI solvers, we want to measure how "close" the recommended strategy is to being correct in case is not immediately winning. To this end, we feed it to (a modified version of) the parity game solver Oink [6] and compute the *(relative) distance* of the obtained strategy, as follows. We count the number of (reachable) states in which the winning strategy determined by Oink differs from the recommended one, i.e. how many "wrong" choices were recommended, and divide it by the total amount of (reachable) states. We note that this unfortunately induces a slight bias that we cannot measure: Oink may potentially change winning decisions because of internal details of the algorithm. Ideally, we would want to obtain the minimal distance over all winning strategies; however this quantity is intractable to compute due to the exponential size of the strategy space. Nevertheless, we believe that this measure strongly correlates with the quality of the strategy.

We argue that simply measuring the number of iterations required by strategy iteration to converge is a too crude metric: On the one hand, even a "very wrong" strategy can be changed to a winning strategy in a single iteration by changing the choice in every single state. On the other hand, even a nearly correct strategy, requiring only a hand full of changes, may need as many iterations. Moreover, this additionally induces the same bias as above.

**Table 1.** Summary of our comparison between TrueSI, the approach of [22], and our tool SemML. We first list the fraction of immediately winning strategies (larger is better), followed by the geometric mean of the relative distance, i.e. the fraction of states in which the decision was adapted by Oink to obtain a winning strategy (smaller is better). For the first comparison, we also consider random initialization as a baseline. For this second comparison to be fair, we only consider games where neither tool yielded an immediately winning strategy.

**Fig. 5.** A detailed comparison on SYNTCOMP formulae. The left plot compares how many games were immediately solved, grouped by size and considering the (arithmetic) mean in each group. SemML's values are displayed by crosses, TrueSI by circles. The right plot compares the relative distance of SemML's and TrueSI's solutions.

*Expectations.* Since our approach incorporates trueness as one of its many features, we expect that our approach should be at least on par with the previous one of [22]. As we also consider long-term temporal information beyond trueness, we particularly expect to outperform TrueSI on larger, more complicated instances.

*Results.* We ran this evaluation on consumer hardware (Intel Core i7-8565U with 16GB RAM). We summarize our findings in Table 1. Clearly, our approach vastly outperforms the previous one. In particular, while TrueSI perfectly handles (co-)safety formulae, its performance quickly drops when going to more complicated formulae. In comparison, the SemML solves the vast majority of formulae immediately, even on the quite complicated SYNTCOMP dataset. We note that these findings are not "absolute" (as to be expected from machine learning approaches). There are few instances where the previous approach does perform better. Our baseline comparison to a random initialization approach validates that both approaches indeed solve a non-trivial problem.

Since we are particularly interested in complex, "human written" formulae, we investigate the SYNTCOMP dataset more closely. In Fig. 5, we provide a more detailed view on our two metrics. First, we investigate how the "immediately solving" performance evolves in comparison to the size of the game, which intuitively correlates with the difficulty of the synthesis question. We observe that SemML solves practically all smaller games and still performs well on larger games, compared to TrueSI, which quickly falls off. The second plot displays the relative distances for each instance which neither recommendation solved immediately. We clearly see that the strategies recommended by SemML are better in almost all cases.

This positively answers our first question. Aside from the direct comparison to the previous approach, the significant percentage of immediately solved games gives us an interesting implication: If SemML solves many games immediately, we can use SemML as a best-effort guidance tool for reactive synthesis questions which are intractably large to solve. Moreover, SemML thus presents us with a constant size representation of a winning strategy for many games, effectively described by approximately a few hundred SVM weights compared to a decision table for thousands of states in *each* game.

#### **6.3 RQ2: On-the-fly SemML**

In our second experiment, we evaluate the suitability of SemML for real-world parity game solving by using it as guidance tool for the state-of-the-art reactive synthesis tool Strix [33].

*Strix' Anatomy.* We first briefly describe how Strix works and how it uses guidance heuristics. In essence, Strix builds the parity game on-the-fly, i.e. iteratively constructs parts of the game it deems important. Then, two strategy improvements are running in parallel, one for either player. Not yet explored states are treated as losing for both. In this way, if we find a winning strategy for either player on the constructed part of the game, it is winning for the complete game. Otherwise, we need to explore further. Here, a key ingredient for practical efficiency is a heuristic to decide which states should be explored first: If we explore states reachable under the "smallest" winning strategy, we naturally find this strategy as quickly as possible. In its current form, Strix employs trueness for this guidance and selects an *automaton* edge with the *globally* highest trueness for exploration. (Dually, edges with the lowest trueness are also followed, since these are "promising" for the environment.)

*Integration.* We integrate SemML with Strix as follows. Suppose we are asked to compute a global score for an automaton edge *e* = (*p, q*) (recall that SemML gives *local* advice on edges in the *game*). We explicitly build up the game between the automaton states *p* and *q*, i.e. all choices of the environment in *p* followed by the respective system choices. For each occurring system state *s*, we compute the SemML ranking score as explained in Sect. 5.2, i.e. the confidence based score. This only gives us local information: the magnitude of our score only reflects the preference relative to actions available in the system state *s* = (*p, v*). Since the previously used trueness proved to be a good indicator for global progress, we multiply our local score by this global value. Finally, to obtain a value for the automaton edge, we take the minimal value of all arising system states, since the environment chooses first. We additionally apply straightforward rules such as assigning values of 0 and 1 values to ff and tt states, respectively. Finally, Strix by default employs a decomposition approach, which does not build a single DPA. Therefore, SemML would not be applicable, and we disable it for the purpose of evaluation.

*Dataset.* We considered 188 randomly selected formulae of SYNTCOMP (which were not used in the training of the model), also including unrealizable ones.

*Metrics.* We evaluate the total required time to solve the game and compare to Strix in its normal configuration. Since we expect the unoptimized computation of SemML's advice to take considerable time, we separately measure the required time and additionally perform a comparison with this time subtracted. Since our scoring function is a straightforward SVM, we strongly believe that by tailoring the evaluation to Strix' requirements, it can be significantly sped up. In particular, our advice computation re-constructs information which is computed during the exploration of the automaton but difficult to access without significant changes to both Strix and Owl.

*Expectations.* We do not expect this approach to work to its full potential because Strix architecture does not exactly fit our approach (recall that our primary motivation was to compare to [22]). We discuss these differences and possible ways to address them later. Moreover, as we construct the intermediate game states for every recommendation and evaluate the recommender SVM several times, we expect that significant time is spent computing the advice of SemML.

*Results.* We conducted our experiments on a server with an Intel Xeon E5-2630 v4 processor with 256GiB of RAM and employed a 10 min timeout per execution. We summarize our findings in Fig. 6. Strikingly, our approach already performs favourably, despite the differences in architecture, hardly optimized advice computation, and no specific re-training for the task at hand. Excluding the time spent for advice computation, our approach performs significantly better in practically all instances. This answers our second question positively, too.

**Adapting SemML to Strix** In order to adapt our underlying approach, we require several non-trivial changes to SemML. We discuss the "mismatches" between the current approach and how they could be addressed. First, Strix selects a globally optimal edge to explore while SemML suggest actions locally. In particular,

**Fig. 6.** Scatter plot comparing Strix with guidance provided by SemML and the default Trueness. On the left, we depict the total runtime excluding time spent for computing the guidance, and on the right we show the total time. We plot all models for which at least one method produced a result and count timeouts as 20 min (twice the timeout of 10 min). Note that the plot is logarithmic. The dashed lines denote a 10x difference.

our scoring is not trained to compare edges of two different states. While trueness seems to be a good compromise for the time being, we believe that (through significant engineering effort) Strix can be modified to accommodate local recommendations, or, alternatively, a more sophisticated indicator of a state's global relevance can be learnt. Second, Strix performs two searches, one for the environment and one for the system player. However, the parity games we deal with are not entirely symmetric – environment always moves first. Thus, we cannot directly apply SemML's ranking to environment states, as they have a different structure. Here, we believe that the best solution is to train a separate model for the environment (or rather, six further models). Thirdly, Strix only constructs the automaton explicitly and computes the game implicitly. As such, Strix requests scoring information only for edges in the automaton and not in the game. This can be addressed by closely integrating the scoring computation with the exploration of the automaton – instead of rebuilding the game for each edge (*p, q*), we can compute all scores for all outgoing edges of *p* at once. Finally, as we mentioned, Strix by default applies a decomposition approach which builds several sub-automata. These also are equipped with semantic labelling, however with a different meaning – enough to create a significant hurdle for our learning approach. We note that Strix actually builds automata by communicating with Owl through a highly optimized interface between Java and C++, significantly complicating passing information back and forth between the processes.

### **7 Conclusion**

We demonstrated that semantic labelling can be exploited for practical gains in LTL synthesis. Our experimental evaluation shows that we vastly outperform the simple approach of [22], the first step in this direction. Moreover, despite several mismatches, our approach shows promising results for real world applications of this idea, i.e. when combined with the state-of-the-art tool Strix.

*Future Work.* As discussed above, the main point for future work is a tight, tailored integration with Strix. In particular, we want to modify our approach to be applicable to the decomposition methods of Strix, modify Strix to consider local guidance, and actually learn for the precise task required by Strix.

Aside from this, we believe that there might be further interesting features (hand-crafted or learnt) which could provide us with additional insights. In particular, we want to employ automated feature extraction, through more sophisticated model architectures such as *transformers* or *graph neural networks*.

### **References**

414 J. Křetínský et al.

43. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science (LICS 1986), Cambridge, Massachusetts, 16–18 June 1986, pp. 332–344. IEEE Computer Society (1986)

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Policy Synthesis and Reinforcement Learning for Discounted LTL

Rajeev Alur1 , Osbert Bastani1 , Kishor Jothimurugan1 , Mateo Perez2(B) , Fabio Somenzi2 , and Ashutosh Trivedi2

1 University of Pennsylvania, Philadelphia, PA, USA<EMAIL_ADDRESS>2 University of Colorado Boulder, Boulder, USA<EMAIL_ADDRESS>
Abstract. The difficulty of manually specifying reward functions has led to an interest in using linear temporal logic (LTL) to express objectives for reinforcement learning (RL). However, LTL has the downside that it is sensitive to small perturbations in the transition probabilities, which prevents probably approximately correct (PAC) learning without additional assumptions. Time discounting provides a way of removing this sensitivity, while retaining the high expressivity of the logic. We study the use of discounted LTL for policy synthesis in Markov decision processes with unknown transition probabilities, and show how to reduce discounted LTL to discounted-sum reward via a reward machine when all discount factors are identical.

### 1 Introduction

Reinforcement learning [39] (RL) is a sampling-based approach to synthesis in systems with unknown dynamics where an agent seeks to maximize its accumulated reward. This reward is typically a real-valued feedback that the agent receives on the quality of its behavior at each step. However, designing a reward function that captures the user's intent can be tedious and error prone, and misspecified rewards can lead to undesired behavior, called *reward hacking* [5].

Due to the aforementioned difficulty, recent research [8,17,23,31,35] has shown interest in utilizing high-level logical specifications, particularly linear temporal logic [7] (LTL), to express intent. However, a significant challenge arises due to the sensitivity of LTL, similar to other infinite-horizon objectives like average reward and safety, to small changes in transition probabilities. Even slight modifications in transition probabilities can lead to significant impacts on the value, such as enabling previously unreachable states to become reachable. Without additional information on the transition probabilities, such as the minimum nonzero transition probability, LTL is proven to be not probably approximately correct (PAC) [29] learnable [3,43]. Ideally, it is desirable to maintain PAC learnability while still keeping the benefits of a highly expressive temporal logic.

This research was partially supported by ONR award N00014-20-1-2115, NSF grant CCF-2009022, and NSF CAREER award CCF-2146563.

c The Author(s) 2023

C. Enea and A. Lal (Eds.): CAV 2023, LNCS 13964, pp. 415–435, 2023. https://doi.org/10.1007/978-3-031-37706-8\_21

Fig. 1. Example showing non-robustness of safety specifications.

Discounting can serve as a solution to this problem. Typically, discounting is used to encode time-sensitive rewards (i.e., a payoff is worth more today than tomorrow), but it has a useful secondary effect that payoffs received in the distant future have small impact on the accumulated reward today. This insensitivity enables PAC learning without requiring any prior knowledge of the transition probabilities. In RL, discounted reward is commonly used and has numerous associated PAC learning algorithms [29].

In this work, we examine the discounted LTL of [2] for policy synthesis in Markov decision processes (MDPs) with unknown transition probabilities. We refer to such MDPs as "unknown MDPs" throughout the paper. This logic maintains the syntax of LTL, but discounts the temporal operators. Discounted LTL gives a quantitative preference to traces that satisfy the objective sooner, and those that delay failure as long as possible. The authors of [2] examined discounted LTL in the model checking setting. Exploring policy synthesis and learnability for discounted LTL specifications is novel to this paper.

To illustrate how discounting affects learnability, consider the example [32] MDP shown in Fig. 1. It consists of a safe state s0, two sink states s1, s2, and two actions a1, a2. Taking action ai in s0 leads to a sink state with probability pi and stays in s0 with probability 1 − pi. Suppose we are interested in learning a policy to make sure that the system always stays in the state s0. Now consider two scenarios—one in which p1 = 0 and p2 = δ and another in which p2 = 0 and p1 = δ where δ > 0 is a small positive value. In the former case, the optimal policy is to always choose a1 in s0 and in the latter case, we need to choose a2 in s0. Furthermore, it can be shown that a near-optimal policy in one case is not near-optimal in another. However, we cannot select a finite number of samples needed to distinguish between the two cases (with high probability) without knowledge of δ. In contrast, the time-discounted semantics of the safety property evaluates to 1 − λk where k is the number of time steps spent in the state s0. Then, for sufficiently small δ, any policy achieves a high value w.r.t. the discounted safety property in both scenarios. In general, small changes to the transition probabilities do not have drastic effects on the nature of near-optimal policies for discounted interpretations of LTL properties.

*Contributions.* Table 1 summarizes results of this paper in the context of known results regarding policy synthesis for various classes of specifications. We consider three key properties of specifications, namely, (1) whether there is a finite-state optimal policy and whether there are known algorithms for (2) computing an optimal policy when the MDP is known, as well as for (3) learning a near-optimal

Table 1. Policy synthesis in MDPs for different classes of specifications.

policy when the transition probabilities are unknown (without additional assumptions). The classes of specifications include reward machines with discounted-sum rewards [24], linear temporal logic (LTL) [7], discounted LTL and a variant of discounted LTL in which all discount factors are identical, which we call *uniformly* discounted LTL. In this paper, we show the following.

*Related Work.* Linear temporal logic (LTL) is a popular and expressive formalism to unambiguously express qualitative safety and progress requirements of Kripke structures and MDPs [7]. The standard approach to model check LTL formulas against MDPs is the *automata-theoretic* approach where the LTL formulas are first translated to a class of good-for-MDP automata [20], such as limitdeterministic Büchi automata [18,36,37,40], and then, efficient graph-theoretic techniques (computing accepting end-component and then maximizing the probability to reach states in such components) [13,30,40] over the product of the automaton with the MDP can be used to compute optimal satisfaction probabilities and strategies. Since LTL formulas can be translated into (deterministic) automata in doubly exponential time, the probabilistic model checking problem is in 2EXPTIME with a matching lower bound [11].

Several variants of LTL have been proposed that provide discounted temporal modalities. De Alfaro et al. [15] proposed an extension of μ-calculus with discounting and showed [14] the decidability of model-checking over finite MDPs. Mandrali [33] introduced discounting in LTL by taking a discounted sum interpretation of logic over a trace. Littman et al. [32] proposed geometric LTL as a logic to express learning objectives in RL. However, this logic has unclear semantics for nesting operators. Discounted LTL was proposed by Almagor, Boker, and Kupferman [2], which considers discounting without accumulation. The decidability of the policy synthesis problem for discounted LTL against MDPs is an open problem.

An alternative approach to discounting that ensuring PAC learnability is to introduce a fixed time horizon, along with a temporal logic for finite traces. In this setting, the logic LTLf is the most popular [10,16]. Using LTLf with a finite horizon yields simple algorithms [41], finite automata suffice for checking properties, but at the expense of the expressivity of the logic, formulas like **GF**p and **FG**p both mean that p occurs at the end of the trace.

There has been a lot of recent work on reinforcement learning from temporal specifications [1,9,16,19,21,22,24–28,31,32,42,44]. Such approaches often lack strong convergence guarantees. Some methods have been developed to reduce LTL properties to discounted-sum rewards [8,19] while preserving optimal policies; however they rely on the knowledge of certain parameters that depend on the transition probabilities of the unknown MDP. Recent work [3,32,43] has shown that PAC algorithms that do not depend on the transition probabilities do not exist for the class of LTL specifications. There has also been work on learning algorithms for LTL specifications that provide guarantees when additional information about the MDP (e.g., the smallest nonzero transition probability) is available [6,12,17].

### 2 Problem Definition

An alphabet Σ is a finite set of letters. A finite word (resp. ω-word) over Σ is defined as a finite sequence (resp. ω-sequence) of letters from Σ. We write Σ∗ and Σω for the set of finite and ω-words over Σ.

A *probability distribution* over a finite set S is a function d: S→[0, 1] such that - s∈S d(s)=1. Let D(S) denote the set of all discrete distributions over S.

*Markov Decision Processes.* A Markov Decision Process (MDP) is a tuple M = (S, A, s0, P), where S is a finite set of states, s0 is the initial state, A is a finite set of actions, and P : S × A → D(S) is the transition probability function. An *infinite run* ψ ∈ (S×A)ω is a sequence ψ = s0a0s1a1 ..., where si ∈ S and ai ∈ A for all i ∈ Z≥0. For any run ψ and any i ≤ j, we let ψi:j denote the subsequence siaisi+1ai+1 ...aj−1sj . Similarly, a *finite run* h ∈ (S×A)∗×S is a finite sequence h = s0a0s1a1 ...at−1st. We use Z(S, A)=(S×A)ω and Zf (S, A)=(S×A)∗×S to denote the set of infinite and finite runs, respectively.

A policy π : Zf (S, A) → D(A) maps a finite run h ∈ Zf (S, A) to a distribution π(h) over actions. We denote by Π(S, A) the set of all such policies. A policy π is deterministic if, for all finite runs h ∈ Zf (S, A), there is an action a ∈ A with π(h)(a)=1.

Given a finite run h = s0a0 ...at−1st, the *cylinder* of h, denoted by Cyl(h), is the set of all infinite runs with prefix h. Given an MDP M and a policy π ∈ Π(S, A), we define the probability of the cylinder set by DMπ (Cyl(h)) = t−1 i=0 π(h0:i)(ai)P(si, ai, si+1). It is known that DMπ can be uniquely extended to a probability measure over the σ-algebra generated by all cylinder sets. Let P be a finite set of atomic propositions and Σ = 2P denote the set of all valuations of propositions in P. An infinite word ρ ∈ Σω is a map ρ : Z≥0 → Σ.

Definition 1 (Discounted LTL). *Given a set of atomic propositions* P*,* discounted LTL *formulas over* P *are given by the grammar*

$$\varphi := b \in \mathcal{P} \mid \neg \varphi \mid \varphi \vee \varphi \mid \mathbf{X} \lambda \varphi \mid \varphi \text{ U} \lambda \varphi \varphi$$

*where* λ ∈ [0, 1)*. Note that, in general, different temporal operators within the same formula may have different discount factors* λ*. For a formula* ϕ *and a word* ρ = σ0σ1 ... ∈ (2P )ω*, the semantics* ϕ, ρ ∈ [0, 1] *is given by*

$$\begin{aligned} \left[b,\rho\right] &= \mathbb{1}\left(b \in \sigma\_{0}\right) \\ \left[\neg\varphi,\rho\right] &= 1 - \left[\varphi,\rho\right] \\ \left[\varphi\_{1}\vee\varphi\_{2},\rho\right] &= \max\left\{\left[\varphi\_{1},\rho\right],\left[\varphi\_{2},\rho\right]\right\} \\ \left[\mathbf{X}\_{\lambda}\varphi,\rho\right] &= \lambda \cdot \left[\varphi,\rho\_{1:\infty}\right] \\ \left[\varphi\_{1}\mathbf{U}\_{\lambda}\varphi\_{2},\rho\right] &= \sup\_{i\geq 0}\left\{\min\left\{\lambda^{i}\left[\varphi\_{2},\rho\_{i:\infty}\right],\min\_{0\leq j$$

*where* ρi:∞ = σiσi+1 ... *denotes the infinite word starting at position* i*.*

Conjunction is defined using ϕ1 ∧ ϕ2 = ¬(¬ϕ1 ∨ ¬ϕ2). We use **F**λϕ = true**U**λϕ and **G**λϕ = ¬**F**λ¬ϕ to denote the discounted versions of *finally* and *globally* operators respectively. Note that when all discount factors equal 1, the semantics corresponds to the usual semantics of LTL.

For this paper, we consider the case of strict discounting, where λ < 1. We refer to the case where the discount factor is the same for all temporal operators as *uniform discounting*. Our definition differs from [2] in two ways: 1) we discount the next operator, and 2) we enforce strict, exponential discounting.

*Example Discounted LTL Specifications.* To develop an intuition of the semantics of discounted LTL, we now present a few example formulas and their meaning.

*Policy Synthesis Problem.* Given an MDP M = (S, A, s0, P), we assume that we have access to a *labelling function* L : S → Σ that maps each state to the set of propositions that hold true in that state. Given any run ψ = s0a0s1a1 ... we can define an infinite word L(ψ) = L(s0)L(s1)... that denotes the corresponding sequence of labels. Given a policy π for M, we define the value of π with respect to a discounted LTL formula ϕ as

$$\mathcal{J}^{\mathcal{M}}(\pi,\varphi) = \underset{\rho \sim \mathcal{D}\_{\pi}^{\mathcal{M}}}{\mathbb{E}}[\varphi,\rho] \tag{1}$$

and the optimal value for M with respect to ϕ as J ∗(M, ϕ) = supπ J M(π,ϕ). We say that a policy π is optimal for ϕ if J M(π,ϕ) = J ∗(M, ϕ). Let Πopt(M, ϕ) denote the set of optimal policies. Given an MDP M, a labelling function L and a discounted LTL formula ϕ, the policy synthesis problem is to compute an optimal policy π ∈ Πopt(M, ϕ) when one exists.

*Reinforcement Learning Problem.* In reinforcement learning, the transition probabilities P are unknown. Therefore, we need to interact with the environment to learn a policy for a given specification. In this case, it is sufficient to learn an εoptimal policy π that satisfies J M(π,ϕ) ≥ J ∗(M, ϕ)−ε. We use Πε opt(M, ϕ) to denote the set of ε-optimal policies. Formally, a learning algorithm A is an iterative process which, in every iteration n, (i) takes a step in M from the current state, (ii) outputs a policy πn and (iii) optionally resets the current state to s0. We are interested in probably-approximately correct (PAC) learning algorithms.

Definition 2 (PAC-MDP). *A learning algorithm* A *is said to be PAC-MDP for a class of specifications* C *if, there is a function* η *such that for any* p > 0*,* ε > 0*, MDP* M = (S, A, s0, P)*, labelling function* L*, and specification* ϕ ∈ C*, taking* N = η(|S|, |A|, |ϕ|, 1 p , 1 ε )*, with probability at least* 1 − p*, we have*

$$\left| \left\{ n \mid \pi\_n \notin H\_{opt}^\varepsilon(\mathcal{M}, \varphi) \right\} \right| \le N.$$

It has been shown that there does not exist PAC-MDP algorithms for LTL specifications. Therefore, we are interested in the class of discounted LTL specifications that are strictly discounted, i.e. λ < 1 for every temporal operator.

### 3 Properties of Discounted LTL

In this section, we discuss important properties of discounted LTL regarding the nature of optimal policies. We first show that, under uniform discounting, the amount of memory required for the optimal policy may increase with the discount factor. We then show that, in general, allowing multiple discount factors may result in optimal policies requiring infinite memory. This motivates our restriction to the uniform discounting case in Sect. 4. We end this section by introducing a PAC learning algorithm for discounted LTL.

#### 3.1 Nature of Optimal Policies

It is known that for any (undiscounted) LTL formula ϕ and any MDP M, there exists a *finite memory* policy that is optimal—i.e., the policy stores only a finite amount of information about the history. Formally, given an MDP M = (S, A, s0, P), a finite memory policy π = (M, δM, μ, m0) consists of a finite set of memory states M, a transition function δM : M × S × A → M and an action function μ : M × S → D(A). Given a finite run h = s0a0 ...st = h st, the policy's action is sampled from μ(δM(m0, h ), st) where δM is also used to represent the transition function extended to sequences of state-action pairs. We use Πf (S, A) to denote the set of finite memory policies. In this paper, we will show that uniformly discounted LTL admits finite memory optimal policies, but that infinite memory may be required for the general case.

Unlike (undiscounted) LTL, discounted LTL allows a notion of satisfaction quality. In discounted LTL, traces which satisfy a reachability objective sooner are given a higher value, and are thus preferred. If an LTL formula cannot be satisfied, the corresponding discounted LTL formula will assign higher values to traces which delay failure as long as possible. These properties of discounted LTL are desirable for enabling notions of promptness, but may yield more complex strategies which try to balance the values of multiple competing subformulas.

*Example 1.* Consider the discounted LTL formula ϕ = **G**λp∧**F**λ¬p. This formula contains two competing objectives that cannot both be completely satisfied. Increasing the value of **G**λp by increasing the number of p's at the beginning of the trace before the first ¬p decreases the value of **F**λ¬p. Under the semantics of conjunction, the value of ϕ is the minimum of the two subformulas. Specifically, the value of ϕ w.r.t. a word ρ is

$$\begin{aligned} \left[\mathbf{G}\boldsymbol{\lambda}p \wedge \mathbf{F}\boldsymbol{\lambda}\neg p, \rho\right] &= \left[\neg \mathbf{F}\boldsymbol{\lambda}\neg p \wedge \mathbf{F}\boldsymbol{\lambda}\neg p, \rho\right] \\ &= \left[\neg (\mathbf{F}\boldsymbol{\lambda}\neg p \lor \neg \mathbf{F}\boldsymbol{\lambda}\neg p), \rho\right] \\ &= 1 - \max\{\left[\mathbf{F}\boldsymbol{\lambda}\neg p, \rho\right], \left[\neg \mathbf{F}\boldsymbol{\lambda}\neg p, \rho\right]\} \\ &= 1 - \max\left\{\sup\_{i\geq 0} \{\boldsymbol{\lambda}^{i}\left[\neg p, \rho\_{i:\infty}\right]\}, 1 - \sup\_{i\geq 0} \{\boldsymbol{\lambda}^{i}\left[\neg p, \rho\_{i:\infty}\right]\}\right\}. \end{aligned}$$

where ρi:∞ is the trace starting from index i. Now consider a two state (deterministic) MDP with two states S = {s1, s2} and two actions A = {a1, a2} in which the agent can decide to either stay in s1 or move to s2 at any step and the system stays in s2 upon reaching s2. This MDP can be seen in Fig. 2. We have one proposition p which holds in state s1 and not in s2. Note that all runs produced by the example MDP are either of the form sω 1 or sk 1sω 2 . The discounted LTL value of runs of the form sω 1 is 0. The value of runs of the form ψ = sk 1sω 2 is

$$v(k) = \left[\varphi, L(\psi)\right] = 1 - \max\{\lambda^k, 1 - \lambda^k\}\ \dots$$

A finite memory policy stays in s1 for k steps will yield this value. Since λk is decreasing in k and 1−λk is increasing in k, the integer value of k that maximizes v(k) lies in the interval [γ − 1, γ + 1] where γ ∈ R satisfies λγ = 1 − λγ. Figure 2 shows this graphically. We have that γ = log(0.5) log(λ) which is increasing in λ. Hence, the amount of memory required increases with increase in λ.

Fig. 2. An example showing that memory requirements for optimal policies may depend on the discount factor. The red line is λk, the blue line is 1 *−* λk and the solid black line is v(k)=1 *−* max*{*λn, 1 *−* λn*}*, where k is the number of time steps one remains in s0. The dashed vertical line shows the value γ where v(k) is maximized. We have set λ = 0.99. Note that changing the value of λ corresponds to rescaling the x-axis. (Color figure online)

The optimal strategy in the example above tries to balance the value of two competing subformula. We will now show that extending this idea to the general case of multiple discount factors requires balancing quantities that are decaying at different speeds. This balancing may require remembering an arbitrarily long history of the trace—infinite memory is required.

Theorem 1. *There exists an MDP* M = (S, A, s0, P)*, a labelling function* L *and a discounted LTL formula* ϕ *such that for all* π ∈ Πf (S, A) *we have* JM(π,ϕ) < J ∗(M, ϕ).

*Proof.* Consider the MDP M depicted in Fig. 3. It consists of three states S = {s0, s1, s2} and two actions A = {a1, a2}. The edges are labelled with actions and the corresponding transition probabilities. There are two propositions P = {p1, p2} and p1 holds true in state s1 and p2 holds true in state s2. The specification is given by ϕ = **F**λ1**G**λ2 p1 ∧ **F**λ2 p2 where λ1 < λ2 < 1.

Fig. 3. The need for infinite memory for achieving optimality in discounted LTL.

For any run ψ that never visits s2, we have ϕ, L(ψ) = 0 since -**F**λ2 p2, L(ψ) = 0. Otherwise the run has the form ψ = sk0 0 sk1 1 sω 2 where k0 is stochastic and k1 is a strategic choice by the agent. To show that this requires an infinite amount of memory to play optimally, one just has to show that the optimal choice of k1 increases with k0. This means that the agent must remember k0, the number of steps spent in the initial state, via an unbounded counter. Note that every value of k0 has a non-zero probability in M and therefore choosing a suboptimal k1 for even a single value of k0 causes a decrease in value from the policy that always chooses optimal k1.

The value of the run ψ is ϕ, L(ψ) = min(λk0 1 (1 − λk1 2 ), λk0+k1 2 ). Note that λk0 1 (1 − λk1 2 ) increases with increase in k1 and λk0+k1 2 decreases with increase in k1. Therefore taking γ ∈ R to be such that λk0 1 (1 − λγ 2 ) = λk0+γ 2 , the optimal choice of k1 lies in the interval [γ−1, γ+1]. Now γ satisfies 1 = (λ2/λ1)k0+1 λγ 2 . Since λ1 < λ2 < 1 we must have that γ increases with increase in k0. Therefore, k1 also increases with increase in k0.

#### 3.2 PAC Learning

In the above discussion, we showed that one might need infinite memory to act optimally w.r.t a discounted LTL formula. However, it can be shown that for any MDP M, labelling function L, discounted LTL formula ϕ and any ε > 0, there is a finite-memory policy π that is ε-optimal for ϕ. In fact, we can show that this class of discounted LTL formulas admit a PAC-MDP learning algorithm.

Theorem 2 (Existence of PAC-MDP). *There exists a PAC-MDP learning algorithm for discounted LTL specifications.*

*Proof (sketch).* Our approach to compute ε-optimal policies for discounted LTL is to compute a policy which is optimal for T steps. The policy will depend on the entire history of atomic propositions that has occured so far.

Given discounted LTL specification ϕ, the first step of the algorithm is to determine T. We select T such that for any two infinite words α and β where the first T + 1 indices match, i.e. α0:T = β0:T , we have that  [[ϕ, α]]−[[ϕ, β]] ≤ ε. Say that the maximum discount factor appearing in all temporal operators is λmax . Due to the strict discounting of discounted LTL, selecting T ≥ log ε log λmax ensures that  [[ϕ, α]] − [[ϕ, β]] ≤ λn ≤ ε.

Now we unroll the MDP for T steps. We include the history of the atomic proposition sequence in the state. Given an MDP M = (S, A, s0, P) and a labeling L : S → Σ, the unrolled MDP MT = (S , A , s 0, P ) is such that

$$S' = \bigcup\_{t=0}^{T} S \times \underbrace{\Sigma \times \dots \times \Sigma}\_{t \text{ times}},$$

A = A, P ((s, σ0,...,σt−1), a,(s , σ0,...,σt−1, σt)) = P(s, a, s ) if 0 ≤ t ≤ T and σt = L(s ), and is 0 otherwise (the MDP goes to a sink state if t>T). The leaves of the unrolled MDP are the states where T timesteps have elapsed. In these states, there is an associated finite word of length T. For a finite word of length T, we define the value of any formula ϕ to be zero beyond the end of the trace, i.e. [[ϕ, ρj:∞]] = 0 for any j>T. We then compute the value of the finite words associated with the leaves which is then considered as the reward at the final step. We can use existing PAC algorithms to compute an ε-optimal policy w.r.t. this reward for the finite horizon MDP MT from which we can obtain a 2ε-optimal policy for M w.r.t the specification ϕ.

### 4 Uniformly Discounted LTL to Reward Machines

In general, optimal strategies for discounted LTL require infinite memory (Theorem 1). However, producing such an example required the use of multiple, varied discount factors. In this section, we will show that finite memory is sufficient for optimal policies under uniform discounting, where the discount factors for all temporal operators in the formula are the same. We will also provide an algorithm for computing these strategies.

Our approach is to reduce uniformly discounted LTL formulas to *reward machines*, which are finite state machines in which each transition is associated with a reward. We show that the value of a given discounted LTL formula ϕ for an infinite word ρ is the discounted-sum reward computed by a corresponding reward machine.

Formally, a reward machine is a tuple R = (Q, δ, r, q0, λ) where Q is a finite set of states, δ : Q × Σ → Q is the transition function, r : Q × Σ → R is the reward function, q0 ∈ Q is the initial state, and λ ∈ [0, 1) is the discount factor. With any infinite word ρ = σ0σ1 ... ∈ Σω, we can associate a sequence of rewards c0c1 ... where ct = r(qt, σt) with qt = δ(qt−1, σt−1) for t > 0. We use R(ρ) to denote the discounted reward achieved by ρ,

$$\mathcal{R}(\rho) = \sum\_{t=0}^{\infty} \lambda^t c\_t,$$

and R(w) to denotes the partial discounted reward achieved by the finite word w = σ0σ1 ...σT ∈ Σ∗—i.e., R(w) = -T t=0 λt ct where ct is the reward at time t.

Given a reward machine R and an MDP M, our objective is to maximize the expected value R(ρ) from the reward machine reading the word ρ produced by the MDP. Specifically, the value for a policy π for M is

$$\mathcal{J}^{\mathcal{M}}(\pi,\mathcal{R}) = \underset{\rho \sim \mathcal{D}\_{\pi}^{\mathcal{M}}}{\mathbb{E}}[\mathcal{R}(\rho)],$$

where π is optimal if J M(π, R) = supπ J M(π, R). Finding such an optimal policy is straightforward: we consider the product of the reward machine R with the MDP M to form a product MDP with a discounted reward objective. In the corresponding product MDP, we can compute optimal policies for maximizing the expected discounted-sum reward using standard techniques such as policy iteration and linear programming. If the transition function of the MDP is unknown, this product can be formed on-the-fly and any RL algorithm for discounted reward can be applied. Using the state space of the reward machine as memory, we can then obtain a finite-memory policy that is optimal for R.

We have the following theorem showing that we can construct a reward machine Rϕ for every uniformly discounted LTL formula ϕ.

Theorem 3. *For any uniformly discounted LTL formula* ϕ*, in which all temporal operators use a common discount factor* λ*, we can construct a reward machine* Rϕ = (Q, δ, r, q0, λ) *such that for any* ρ ∈ Σω*, we have* Rϕ(ρ) = ρ, ϕ*.*

We provide the reward machine construction for Theorem 3 in the next subsection. Using this theorem, one can use a reward machine Rϕ that matches the value of a particular uniformly discounted LTL formula ϕ, and then apply the procedure outlined above for computing optimal finite-memory policies for reward machines.

Corollary 1. *For any MDP* M*, labelling function* L *and a discounted LTL formula* ϕ *in which all temporal operators use a common discount factor* λ*, there exists a finite-memory optimal policy* π ∈ Π*opt*(M, ϕ)*. Furthermore, there is an algorithm to compute such a policy.*

#### 4.1 Reward Machine Construction

For our construction, we examine the case of uniformly discounted LTL formula with positive discount factors λ ∈ (0, 1). This allows us to divide by λ in our construction. We note that the case of uniformly discounted LTL formula with λ = 0 can be evaluated after reading the initial letter of the word, and thus have trivial reward machines.

The reward machine Rϕ constructed for the uniformly discounted LTL formula ϕ exhibits a special structure. Specifically, all edges within any given strongly-connected component (SCC) of Rϕ share the same reward, which is either 0 or 1 − λ, while all other rewards fall within the range of [0, 1 − λ]. We present an inductive construction of the reward machines over the syntax of discounted LTL that maintains these invariants.

Lemma 1. *For any uniformly discounted LTL formula* ϕ *there exists a reward machine* Rϕ = (Q, δ, r, q0, λ) *such that following hold:*

Fig. 4. Reward machines for ϕ = p (left) and ϕ = **X**λq (right). The transitions are labeled by the guard and reward.

I1*. For any* ρ ∈ Σω*, we have* Rϕ(ρ) = ρ, ϕ*.* I2*. There is a partition of the states* Q = L =1 Q *and a type mapping* χ : [L] → {0, 1 − λ} *such that for any* q ∈ Q *and* σ ∈ Σ*, (a)* δ(q, σ) ∈ L m= Qm*, and (b) if* δ(q, σ) ∈ Q *then* r(q, σ) = χ()*.* I3*. For any* q ∈ Q *and* σ ∈ Σ*, we have* 0 ≤ r(q, σ) ≤ 1 − λ*.*

Our construction proceeds inductively. We define the reward machine for the base case of a single atomic proposition, i.e. ϕ = p, and then the construction for negation, the next operator, disjunction, the eventually operator (for ease of presentation), and the until operator. The ideas used in the constructions for disjunction, the eventually operator, and the until operator build off of each other, as they all involve keeping track of the maximum/minimum value over a set of subformulas. We use properties I1 and I3 to show correctness, and properties I2 and I3 to show finiteness. A summary of the construction and detailed proofs can be found in the full version of this paper [4].

Atomic Propositions. Let ϕ = p for some p ∈ P. The reward machine Rϕ = (Q, δ, r, q0, λ) for ϕ is such that Q = {q0, q1, q2} and δ(q, σ) = q for all q ∈ {q1, q2} and σ ∈ Σ. The reward machine is shown in Fig. 4 where edges are labelled with propositions and rewards. If p ∈ σ, δ(q0, σ) = q1 and r(q0, σ)=1 − λ. If p /∈ σ, δ(q0, σ) = q2 and r(q0, σ)=0. Finally, r(q1, σ)=1 − λ and r(q2, σ)=0 for all σ ∈ Σ. It is clear to see that I1, I2, and I3 hold.

Negation. Let ϕ = ¬ϕ1 for some LTL formula ϕ1 and let Rϕ1 = (Q, δ, r, q0, λ) be the reward machine for ϕ1. Notice that the reward machine for ϕ can be constructed from Rϕ1 by simply replacing every reward c with (1 − λ) − c as -∞ i=0 λi (1 − λ)=1. Formally, Rϕ = (Q, δ, r , q0, λ) where r (q, σ) = (1 − λ) − r(q, σ) for all q ∈ Q and σ ∈ Σ. Again, assuming that invariants I1, I2, and I3 hold for Rϕ1 , it easily follows that they hold for Rϕ.

Next Operator. Let ϕ = **X**λϕ1 for some ϕ1 and let Rϕ1 = (Q, δ, r, q0, λ) be the reward machine for ϕ1. The reward machine for ϕ can be constructed from Rϕ1 by adding a new initial state q 0 and a transition in the first step from it to the initial state of Rϕ1 . From the next step Rϕ simulates Rϕ1 . This has the resulting effect of skipping the first letter, and decreasing the value by λ. Formally, Rϕ = ({q 0} Q, δ , r , q 0, λ) where δ (q 0, σ) = q0 and δ (q, σ) = δ(q, σ) for all q ∈ Q and σ ∈ Σ. Similarly, r (q 0, σ)=0 and r (q, σ) = r(q, σ) for all q ∈ Q and σ ∈ Σ. Assuming that invariants I1, I2, and I3 hold for Rϕ1 , it follows that they hold for Rϕ.

Disjunction. Let ϕ = ϕ1 ∨ ϕ2 for some ϕ1, ϕ2 and let Rϕ1 = (Q1, δ1, r1, q1 0, λ) and Rϕ2 = (Q2, δ2, r2, q2 0, λ) be the reward machines for ϕ1 and ϕ2, respectively. The reward machine Rϕ = (Q, δ, r, q0, λ) is constructed Rϕ1 and Rϕ2 such that for any finite word it maintains the invariant that the discounted reward is the maximum of the reward provided by Rϕ1 and Rϕ2 . Moreover, once it is ascertained that the reward provided by one machine cannot be overtaken by the other for any suffix, Rϕ begins simulating the reward machine with higher reward.

The construction involves a product construction along with a real-valued component that stores a scaled difference between the total accumulated reward for ϕ1 and ϕ2. In particular, Q = (Q1 × Q2 × R) Q1 Q2 and q0 = (q1 0, q2 0, 0). The reward deficit ζ of a state q = (q1, q2, ζ) denotes the difference between the total accumulated reward for ϕ1 and ϕ2 divided by λn where n is the total number of steps taken to reach q. The reward function is defined as follows.

– For q = (q1, q2, ζ), we let f(q, σ) = r1(q1, σ) − r2(q2, σ) + ζ denote the new (scaled) difference between the discounted-sum rewards accumulated by Rϕ1 and Rϕ2 . The current reward depends on whether f(q, σ) is positive (accumulated reward from Rϕ1 is higher) or negative and whether the sign is different from ζ. Formally,

$$r(q, \sigma) = \begin{cases} r\_1(q\_1, \sigma) + \min\{0, \zeta\} & \text{if } f(q, \sigma) \ge 0 \\ r\_2(q\_2, \sigma) - \max\{0, \zeta\} & \text{if } f(q, \sigma) < 0 \end{cases}$$

– For a state qi ∈ Qi we have r(qi, σ) = ri(qi, σ).

Now we need to make sure that ζ is updated correctly. We also want the transition function to be such that the (reachable) state space is finite and the reward machine satisfies I1, I2 and I3.

– First, we make sure that, when the difference ζ is too large, the machine transitions to the appropriate state in Q1 or Q2. For a state q = (q1, q2, ζ) with |ζ| ≥ 1, we have

$$\delta(q,\sigma) = \begin{cases} \delta\_1(q\_1,\sigma) & \text{if } \zeta \ge 1 \\ \delta\_2(q\_2,\sigma) & \text{if } \zeta \le -1. \end{cases}$$

– For states with |ζ| < 1, we simply advance both the states and update ζ accordingly. Letting f(q, σ) = r1(q1, σ) − r2(q2, σ) + ζ, we have that for a state q = (q1, q2, ζ) with |ζ| < 1,

$$\delta(q,\sigma) = (\delta\_1(q\_1,\sigma), \delta\_2(q\_2,\sigma), f(q,\sigma)/\lambda). \tag{2}$$

– Finally, for qi ∈ Qi, δ(qi, σ) = δi(qi, σ).

*Finiteness.* We argue that the (reachable) state space of Rϕ is finite. Let Qi = Li =1 Qi for i ∈ {1, 2} be the SCC decompositions of Q1 and Q2 that satisfy property I2 for Rϕ1 and Rϕ2 respectively. Intuitively, if Rϕ stays within Q1 × Q2 m × R for some ≤ L1 and m ≤ L2, then the rewards from Rϕ1 and Rϕ2 are constant; this enables us to infer the reward machine (Rϕ1 and Rϕ2 ) with the higher total accumulated reward in a finite amount of time after which we transition to Q1 or Q2. Hence the set of all possible values of ζ in a reachable state (q1, q2, ζ) ∈ Q1 × Q2 m × R is finite. This can be shown by induction.

*Property* I1*.* Intuitively, it suffices to show that Rϕ(w) = max{Rϕ1 (w), Rϕ2 (w)} for every finite word w ∈ Σ∗. We show this property along with the fact that for any w ∈ Σ∗ of length n, if the reward machine reaches a state (q1, q2, ζ), then ζ = (Rϕ1 (w) − Rϕ2 (w))/λn. This can be proved using induction on n.

*Property* I2*.* This property is true if and only if for every SCC C of Rϕ there is a type c ∈ {0, 1−λ} such that if δ(q, σ) = q for some q, q ∈ C and σ ∈ Σ, we have r(q, σ) = c. From the definition of the transition function δ, C cannot contain two states where one is of the form (q1, q2, ζ) ∈ Q1 × Q2 × R and the other is qi ∈ Qi for some i ∈ {1, 2}. Now if C is completely contained in Qi for some i, we can conclude from the inductive hypothesis that the rewards within C are constant (and they are all either 0 or 1 − λ). When all states of C are contained in Q1 × Q2 × R, they must be contained in Q¯1 × Q¯2 × R where Q¯i is some SCC of Rϕi . In such a case, we can show that |C| = 1 and in the presence of a self loop on a state within C, the reward must be either 0 or 1 − λ.

*Property* I3*.* We now show that all rewards are bounded between 0 and (1 − λ). Let q = (q1, q2, ζ) and f(q, σ) = r1(q1, σ) − r2(q2, σ) + ζ. We show the bound for the case when f(q, σ) ≥ 0 and the other case is similar. If ζ ≥ 0, then r(q, σ) = r1(q1, σ) ∈ [0, 1 − λ]. If ζ < 0, then r(q, σ) ≤ r1(q1, σ) ≤ 1 − λ and

$$r(q, \sigma) = r\_1(q\_1, \sigma) + \zeta = f(q, \sigma) + r\_2(q\_2, \sigma) \ge 0.$$

This concludes the construction for ϕ1 ∨ ϕ2.

Eventually Operator. For ease of presentation, we treat the until operator as a generalization of the *eventually* operator **F**λ and present it first. We have that ϕ = **F**ϕ1 for some ϕ1. Let Rϕ1 = (Q1, δ1, r1, q1 0, λ) be the reward machine for ϕ1. Let **X**i λ denote the operator **X**λ applied i times. We begin by noting that

$$\mathbf{F}\_{\lambda}\varphi\_1 \equiv \bigvee\_{i\geq 0} \mathbf{X}\_{\lambda}^{i}\varphi\_1 = \varphi\_1 \vee \mathbf{X}\_{\lambda}\varphi\_1 \vee \mathbf{X}\_{\lambda}^2\varphi\_1 \vee \dots \vee$$

The idea of the construction is to keep track of the unrolling of this formula up to the current timestep n,

$$\mathbf{F}^{n}\_{\lambda}\varphi\_{1} = \bigvee\_{n\geq i\geq 0} \mathbf{X}^{i}\_{\lambda}\varphi\_{1} = \varphi\_{1}\vee \mathbf{X}\_{\lambda}\varphi\_{1}\vee \mathbf{X}^{2}\_{\lambda}\varphi\_{1}\vee \dots \vee \mathbf{X}^{n}\_{\lambda}\varphi\_{1}\dots$$

For this, we will generalize the construction for disjunction. In the disjunction construction, there were states of the form (q1, q2, ζ) where ζ was a bookkeeping parameter that kept track of the difference between Rϕ1 (w) and Rϕ2 (w), namely, ζ = (Rϕ1 (w)−Rϕ2 (w))/λn where w ∈ Σ∗ is some finite word of length n. To generalize this notion to make a reward machine for max{R1,..., Rk}, we will have states of the form {(q1, ζ1),...,(qn, ζn)} where ζi = (Ri(w) − maxj Rj (w))/λn. When ζi ≤ −1 then Ri(w) +λn ≤ maxj Rj (w) and we know that the associated reward machine Ri cannot be the maximum, so we drop it from our set. We also note that the value of **X**i λϕ1 can be determined by simply waiting i steps before starting the reward machine Rϕ1 , i.e. λi Rϕ1 (ρi:∞) = R**X**i λϕ1 (ρ). This allows us to perform a subset construction for this operator.

For a finite word w = σ0σ1 ...σn ∈ Σ∗ and a nonnegative integer k, let wk:∞ denote the subword σk ...σn which equals the empty word if k>n. We use the notation -**X**k λϕ1, w = λkRϕ1 (wk:∞) and define -**F**k λϕ1, w = maxk≥i≥0 -**X**k λϕ1, w which represents the maximum value accumulated by the reward machine of some formula of the form **X**i λϕ1 with i ≤ k on a finite word w. The reward machine for **F**λϕ1 will consist of states of the form (v, S), containing a value v for bookkeeping and a set S that keeps track of the states of all R**X**i λϕ1 that may still obtain the maximum given a finite prefix w of length n, i.e. reward machine states of all subformulas **X**i λϕ1 for n ≥ i ≥ 0 that satisfy -**X**i λϕ1, w+λn > -**F**n λϕ1, w since λn is the maximum additional reward obtainable by any ρ ∈ Σω with prefix w. The subset S consists of elements of the form (qi, ζi) ∈ S where qi = δ1(q1 0, wi:∞) and ζi = (-**X**i λϕ1, w − -**F**n λϕ1, w)/λn corresponding to each subformula **X**i λϕ1. The value v = max{−1, −-**F**n λϕ1, w/λn} is a bookkeeping parameter used to initialize new elements in the set S and to stop adding elements to S when v ≤ −1. We now present the construction formally.

We form a reward machine Rϕ = (Q, δ, r, q0, λ) where Q = R × 2Q1×R and q0 = (0, {(q1 0, 0)}). We define a few functions that ease defining our transition function. Let f(ζ, q, σ) = r1(q, σ) + ζ and m(S, σ) = max (qi,ζi)∈S f(ζi, qi, σ). For the subset construction, we define

$$\Delta(S,\sigma) = \bigcup\_{(q,\zeta)\in S} \{ (\delta\_1(q,\sigma),\zeta'):\zeta' = \left( (f(\zeta,q,\sigma) - m(S,\sigma))/\lambda \right) > -1 \}$$

The transition function is

$$\delta((v, S), \sigma) = \begin{cases} \left( v'(S, v, \sigma), \ \Delta(S, \sigma) \perp \left( q\_0^1, v'(S, v, \sigma) \right) \right) & \text{if } v'(S, v, \sigma) > -1 \\ \left( -1, \ \Delta(S, \sigma) \right) & \text{if } v'(S, v, \sigma) \le -1 \end{cases}$$

where v (S, v, σ)=(v − m(S, σ))/λ. The reward function is r((v, S), σ) = m(S, σ).

We now argue that Rϕ satisfies properties I1, I2 and I3 and the set of reachable states in Rϕ is finite assuming Rϕ1 satisfies I1, I2 and I3.

*Finiteness.* Consider states of the form (v, S) ∈ Q. If v = 0, then it must be that ζi = 0 for all (qi, ζi) ∈ S since receiving a non-zero reward causes the value of v to become negative. There are only finitely many such states. If −1 <v< 0, then we will reach a state (v , S ) ∈ Q with v = −1 in at most n steps, where n is such that v/λn ≤ −1. Therefore, the number of reachable states (v, S) with −1 <v< 0 is also finite. Also, the number of states of the form (−1, S) that can be initially reached (via paths consisting only of states of the form (v, S ) with v > −1) is finite. Furthermore, upon reaching such a state (−1, S), the reward machine is similar to that of a disjunction (maximum) of |S| reward machines. From this we can conclude that the full reachable state space is finite.

*Property* I1*.* The transition function is designed so that the following holds true: for any finite word w ∈ Σ∗ of length n and letter σ ∈ Σ, if δ(q0, w)=(v, S), then m(S, σ)=(-**F**n+1 λ ϕ1, wσ − -**F**n λϕ1, w)/λn. Since r((v, S), σ) = m(S, σ), we get that Rϕ(w) = -**F**n λϕ1, w. Thus, Rϕ(ρ) = -**F**λϕ1, ρ for any infinite word ρ ∈ Σω. This property for m(S, σ) follows from the preservation of all the properties outlined in the above description of the construction.

*Property* I2*.* Consider an SCC C in Rϕ such that (v, S) = δ((v, S), w) for some (v, S) ∈ C and w ∈ Σ∗ of length n > 0. Note that if −1 <v< 0, then (v , S ) = δ((v, S), w) is such that v < v. Thus, it must be that v = 0 or v = −1. If v = 0, then all the reward must be zero, since any nonzero rewards result in v < 0. If v = −1, then it must be that for any (qi, ζi) ∈ S, qi is in an SCC Ci 1 in Rϕ1 with some reward type ci ∈ {0, 1 − λ}. For all ζi to remain fixed (which is necessary as otherwise some ζi strictly increases or decreases), it must be that all ci are the same, say c. Thus, the reward type in Rϕ1 for SCC C equals c.

*Property* I3*.* We can show that for any finite word w ∈ Σ∗ of length n and letter σ ∈ Σ, if δ(q0, w)=(v, S), then the reward is r((v, S), σ) = m(S, σ) = (-**F**n+1 λ ϕ1, wσ − -**F**n λϕ1, w)/λn using induction on n. Since property I3 holds for Rϕ1 , we have that 0 ≤ (-**F**n+1 λ ϕ1, wσ − -**F**n λϕ1, w) ≤ (1 − λ)λn.

Until Operator. We now present the until operator, generalizing the ideas presented for the eventually operator. We have that ϕ = ϕ1**U**λϕ2 for some ϕ1 and ϕ2. Let Rϕ1 = (Q1, δ1, r1, q1 0, λ) and Rϕ2 = (Q2, δ2, r2, q2 0, λ). Note that

$$\begin{aligned} \varphi\_1 \mathbf{U}\_{\lambda} \varphi\_2 &= \bigvee\_{i \ge 0} (\mathbf{X}\_{\lambda}^i \varphi\_2 \wedge \varphi\_1 \wedge \mathbf{X}\_{\lambda} \varphi\_1 \wedge \dots \wedge \mathbf{X}\_{\lambda}^{i-1} \varphi\_1) \\ &= \varphi\_2 \vee (\mathbf{X}\_{\lambda} \varphi\_2 \wedge \varphi\_1) \vee (\mathbf{X}\_{\lambda}^2 \varphi\_2 \wedge \varphi\_1 \wedge \mathbf{X}\_{\lambda} \varphi\_1) \vee \dots \end{aligned}$$

The goal of the construction is to keep track of the unrolling of this formula up to the current timestep n,

$$\varphi\_1 \mathbf{U}\_{\lambda}^n \varphi\_2 = \bigvee\_{n \ge i \ge 0} (\mathbf{X}\_{\lambda}^i \varphi\_2 \wedge \varphi\_1 \wedge \mathbf{X}\_{\lambda} \varphi\_1 \wedge \dots \wedge \mathbf{X}\_{\lambda}^{i-1} \varphi\_1) = \bigvee\_{n \ge i \ge 0} \psi\_i.$$

Each ψi requires a subset construction in the style of the eventually operator construction to maintain the minimum. We then nest another subset construction in the style of the eventually operator construction to maintain the maximum over ψi. For a finite word w ∈ Σ∗, we use the notation ψi, w and ϕ1**U**k λϕ2, w for the value accumulated by reward machine corresponding to these formula on the word w, i.e. ψi, w = min{-**X**i λϕ2, mini>j≥0{-**X**j λϕ1, w} and ϕ1**U**k λϕ2, w = maxk≥i≥0 ψi, w.

Let S = 2(Q1 Q2)×R be the set of subsets containing (q, ζ) pairs, where q may be from either Q1 or Q2. The reward machine consists of states of the form (v, I, X ) where the value v ∈ R and the subset I ∈ S are for bookkeeping, and X ∈ 2S is a subset of subsets for each ψi. Specifically, each element of X is a subset S corresponding to a particular ψi which may still obtain the maximum, i.e. ψi, w + λn > ϕ1**U**n λϕ2, w. Each element of S is of the form (q, ζ). We have that q ∈ Q2 for at most one element where q = δ2(q2 0, wk:∞) and ζ = (-**X**k λϕ2, w − ϕ1**U**n λϕ2, w)/λn. For the other elements of S, we have that q ∈ Q1 with q = δ1(q1 0, wk:∞) and ζ = (-**X**k λϕ1, w − ϕ1**U**n λϕ2, w)/λn. If for any of these elements, the value of its corresponding formula becomes too large to be the minimum for the conjunction forming ψi, i.e. ψi, w + λn ≤ ϕ1**U**n λϕ2, w+λn ≤ -**X**k λϕt, w which occurs when ζ ≥ 1, that element is dropped from S. In order to update X , we add a new S corresponding to ψn on the next timestep. The value v = max{−1, ϕ1**U**n λϕ2, w} is a bookkeeping parameter for initializing new elements in the subsets and for stopping the addition of new elements when v ≤ −1. The subset I is a bookkeeping parameter that keeps track of the subset construction for n>i≥0 **X**i λϕ1, which is used to initialize the addition of a subset corresponding to ψn = **X**n λϕ2 ∧ ( n>i≥0 **X**i λϕ1). We now define the reward machine formally.

We define a few functions that ease defining our transition function. We define δ∗(q, σ) = δi(q, σ) and f∗(ζ, q, σ) = ri(q, σ) + ζ if q ∈ Qi for i ∈ {1, 2}. We also define n(S, σ) = min(qi,ζi)∈S f∗(ζi, qi, σ) and m(X , σ) = maxS∈X n(S, σ). For the subset construction, we define

$$\Delta(S,\sigma,m) = \bigcup\_{(q,\zeta)\in S} \{ (\delta\_\*(q,\sigma),\zeta'):\zeta'<1 \}$$

where ζ = (f∗(ζ, q, σ) − m)/λ and

$$T(\mathcal{X}, \sigma, m) = \bigcup\_{S \in \mathcal{X}} \{ \Delta(S, \sigma, m) : n(S, \sigma) > -1 \}.$$

We form a reward machine Rϕ = (Q, δ, r, q0, λ) where Q = R ×S× 2S and q0 = (0, ∅, {{(q2 0, 0)}}). The transition function is

$$\delta((v, I, \mathcal{X}), \sigma) = \begin{cases} \left(v', \ I', \ T(\mathcal{X}, \sigma, m) \sqcup \left(I' \sqcup (q\_0^2, v')\right)\right) & \text{if } v' > -1\\ \left(-1, \ \emptyset, \ T(\mathcal{X}, \sigma, m)\right) & \text{if } v' \le -1 \end{cases}$$

where m = m(X , σ), v = (v − m)/λ, and I = Δ(I (q1 0, v ), σ, m). The reward function is r((v, I, X ), σ) = m(X , σ).

We now show a sketch of correctness, which mimics the proof for the eventually operator closely.

*Finiteness.* Consider states of the form (v, I, X ) ∈ Q. If v = 0, then for all S ∈ X and (qi, ζi) ∈ S it must be that ζi = 0 since receiving a non-zero reward causes the value of v to become negative. Similarly, all ζi = 0 for (qi, ζi) ∈ I when v = 0. There are only finitely many such states. If −1 <v< 0, then we will reach a state (v , I , X ) ∈ Q with v = −1 in at most n steps, where n is such that v/λn ≤ −1. Therefore, the number of reachable states −1 <v< 0 is also finite. Additionally, the number of states where v = −1 that can be initially reached is finite. Upon reaching such a state (−1, ∅, X ), the reward machine is similar to that of the finite disjunction of reward machines for finite conjunctions.

*Property* I1*.* The transition function is designed so that the following holds true: for any finite word w ∈ Σ∗ of length n and letter σ ∈ Σ, if δ(q0, w)=(v, I, X ), then m(X , σ)=(ϕ1**U**n+1 λ ϕ2, wσ − ϕ1**U**n λϕ2, w)/λn. Since r((v, I, X ), σ) = m(X , σ), we get that Rϕ(w) = ϕ1**U**n λϕ2, w. Thus, Rϕ(ρ) = ϕ1**U**λϕ2, ρ for any infinite word ρ ∈ Σω. This property for m(X , σ) follows from the properties outlined in the construction, which can be shown inductively.

*Property* I2*.* Consider an SCC C of Rϕ and a state (v, I, X ) ∈ C. If v = 0, then we must receive zero reward because non-zero reward causes the value of v to become negative. It cannot be that −1 <v< 0 since if v < 0, we reach a state (v , I , X ) ∈ Q with v = −1 in at most n steps, where n is such that v/λn ≤ −1. If v = −1, then we have a state of the form (−1, ∅, X ). For this to be an SCC, all elements of the form (qk, ζk) ∈ S for S ∈ X must be such that qk is in an SCC of its respective reward machine (either Rϕ1 or Rϕ2 ) with reward type tk ∈ {0, 1 − λ}. Additionally, there cannot be a t k = tk otherwise there would be a ζk that changes following a cycle in the SCC C. Thus, the reward for this SCC C is tk.

*Property* I3*.* This property can be shown by recalling the property above that r((v, I, X ), σ) = m(X , σ)=(ϕ1**U**n+1 λ ϕ2, wσ − ϕ1**U**n λϕ2, w)/λn.

### 5 Conclusion

This paper studied policy synthesis for discounted LTL in MDPs with unknown transition probabilities. Unlike LTL, discounted LTL provides an insensitivity to small perturbations of the transitions probabilities which enables PAC learning without additional assumptions. We outlined a PAC learning algorithm for discounted LTL that uses finite memory. We showed that optimal strategies for discounted LTL require infinite memory in general due to the need to balance the values of multiple competing objectives. To avoid this infinite memory, we examined the case of uniformly discounted LTL, where the discount factors for all temporal operators are identical. We showed how to translate uniformly discounted LTL formula to finite state reward machines. This construction shows that finite memory is sufficient, and provides an avenue to use discounted reward algorithms, such as reinforcement learning, for computing optimal policies for uniformly discounted LTL formulas.

### References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Synthesizing Permissive Winning Strategy Templates for Parity Games

Ashwani Anand, Satya Prakash Nayak(B) , and Anne-Kathrin Schmuck

Max Planck Institute for Software Systems, Kaiserslautern, Germany<EMAIL_ADDRESS>
Abstract. We present a novel method to compute *permissive winning strategies* in two-player games over finite graphs with ω-regular winning conditions. Given a game graph G and a parity winning condition Φ, we compute a *winning strategy template* Ψ that collects an infinite number of winning strategies for objective Φ in a concise data structure. We use this new representation of sets of winning strategies to tackle two problems arising from applications of two-player games in the context of cyber-physical system design – (i) *incremental synthesis*, i.e., adapting strategies to newly arriving, *additional* ω-regular objectives Φ- , and (ii) *fault-tolerant control*, i.e., adapting strategies to the occasional or persistent unavailability of actuators. The main features of our strategy templates – which we utilize for solving these challenges – are their easy computability, adaptability, and compositionality. For *incremental synthesis*, we empirically show on a large set of benchmarks that our technique vastly outperforms existing approaches if the number of added specifications increases. While our method is not complete, our prototype implementation returns the full winning region in all 1400 benchmark instances, i.e. handling a large problem class efficiently in practice.

### 1 Introduction

Two-player ω-regular games on finite graphs are an established modeling and solution formalism for many challenging problems in the context of correct-byconstruction cyber-physical system (CPS) design [2,7,39]. Here, control software actuating a technical system "plays" against the physical environment. The winning strategy of the system player in this two-player game results in software which ensures that the controlled technical system fulfills a given temporal specification for any (possible) event or input sequence generated by the environment. Examples include warehouse robot coordination [36], reconfigurable manufacturing systems [26], and adaptive cruise control [33]. In these applications, the

c The Author(s) 2023

S. P. Nayak and A.-K. Schmuck are supported by the DFG project 389792660 TRR 248–CPEC.

A. Anand and A.-K. Schmuck are supported by the DFG project SCHM 3541/1-1.

C. Enea and A. Lal (Eds.): CAV 2023, LNCS 13964, pp. 436–458, 2023. https://doi.org/10.1007/978-3-031-37706-8\_22

Fig. 1. Experimental results over 1400 generalized parity games comparing the performance of our tool PeSTel against the state-of-the-art generalized parity solver GenZiel [16]. Data points give the average execution time (in ms) over all instances with the same number of parity objectives. Left: all objectives are given *upfront*. Right: objectives are added *one-by-one*. See Sect. 6 for more details on those experiments.

technical system under control, as well as its requirements, are developing and changing during the design process. It is therefore desirable to allow for maintainable and adaptable control software. This, in turn, requires solution algorithms for two-player ω-regular games which allow for this adaptability.

This paper addresses this challenge by providing a new algorithm to efficiently compute *permissive winning strategy templates* in parity games which enable rich *strategy adaptations*. Given a game graph G = (V,E) and an objective Φ a winning strategy template Ψ characterizes the winning region W ⊆ V along with three types of local edge conditions – a *safety*, a *co-live*, and a *live-group* template. The conjunction of these basic templates allows us to capture infinitely many winning strategies over G w.r.t. Φ in a simple data structure that is both (i) easy to obtain during synthesis, and (ii) easy to adapt and compose.

We showcase the usefulness of *permissive winning strategy templates* in the context of CPS design by two application scenarios: (i) *incremental synthesis*, where strategies need to be adapted to newly arriving *additional* ω-regular objectives Φ , and (ii) *fault-tolerant control*, where strategies need to be adapted to the occasional or persistent unavailability of actuators, i.e., system player edges.

We have implemented our algorithms in a prototype tool PeSTel and run it on more than 1400 benchmarks adapted from the SYNTCOMP benchmark suite [21]. These experiments show that our class of templates effectively avoids recomputations for the required strategy adaptations. For*incremental synthesis*, our experimental results are previewed in Fig. 1, where we compare PeSTel against the state-of-the-art solver GenZiel [16] for generalized parity objectives, i.e., finite conjunction of parity objectives. We see that PeSTel is as efficient as GenZiel whenever all conjuncts of the objective are given *up-front* (Fig. 1(left)) - even outperforming it in more than 90% of the instances. Whenever conjuncts of the objective arrive *one at a time*, PeSTel outperforms the existing approaches significantly if the number of objectives increases (Fig. 1(right)). This shows the potential of PeSTel towards more adaptable and maintainable control software for CPS.

$$\begin{array}{c} \begin{array}{c} f \\ \hline \\ \emptyset \\ e \end{array} \end{array} \begin{array}{c} \Phi\_{1} = \Box \neg \{ f \} \quad \Rightarrow \Psi\_{1} = \Psi\_{\text{UNSA}\mathbb{R}}(e\_{dc})\\ \Phi\_{2} = \Box \Diamond \{ c, d \} \Rightarrow \Psi\_{2} = \Psi\_{\text{UN}\mathbb{R}}(\{ e\_{ac}, e\_{ad} \})\\ \Phi\_{3} = \Diamond \Box \neg \{ b \} \quad \Rightarrow \Psi\_{3} = \Psi\_{\text{Cottv}\mathbb{R}}(e\_{ab}, e\_{db}, e\_{dc}) \end{array}$$

Fig. 2. A two-player game graph with Player 1 (squares) and Player 0 (circles) vertices, different winning conditions Φi, and corresponding winning strategy templates Ψi.

Illustrative Example. To appreciate the simplicity and easy adaptability of our strategy templates, consider the game graph in Fig. 2(left). The first winning condition Φ1 requires vertex f to never be seen along a play. This can be enforced by Player 0 from vertices W0 = {a, b, c, d} called the *winning region*. The safety template Ψ1 ensures that the game always stays in W0 by forcing the edge ede to never be taken. It is easy to see that every Player 0 strategy that follows this rule results in plays which are winning if they start in W0. Now consider the second winning condition Φ2 which requires vertex c or d to be seen infinitely often. This induces the live-group template Ψ2 which requires that whenever vertex a is seen infinitely often, either edge eac or edge ead needs to be taken infinitely often. It is easy to see that any strategy that complies with this edge-condition is winning for Player 0 from every vertex and there are infinitely many such compliant winning strategies. Finally, we consider condition Φ3 requiring vertex b to be seen only finitely often. This induces the strategy template Ψ3 which is a co-liveness template requiring that all edges from Player 0 vertices which unavoidably lead to b (i.e., eab, ebd, and ede) are taken only finitely often. We can now combine all templates into a new template Ψ = Ψ1 ∧ Ψ2 ∧ Ψ3 and observe that all strategies compliant with Ψ are winning for Φ = Φ1 ∧ Φ2 ∧ Φ3.

In addition to their compositionality, strategy templates also allow for local strategy adaptations in case of edge unavailability faults. Consider again the game in Fig. 2 with the objective Φ2. Suppose that Player 0 follows the strategy π: a → d and d → a, which is compliant with Ψ2. If the edge ead becomes unavailable, we would need to re-solve the game for the modified game graph G = (V,E \ {ead}). However, given the strategy template Ψ2 we see that the strategy π : a → c and d → a is actually compliant with Ψ2 over G . This allows us to obtain a new strategy without re-solving the game.

While these examples demonstrate the potential of templates for strategy adaptation, there exist scenarios where conflicts between templates or graph modifications arise, which require re-computations. Our empirical results, however, show that such conflicts rarely appear in practical benchmarks. This suggests that our technique can handle a large problem class efficiently in practice.

Related Work. The class of templates we use was introduced in [4] and utilized to represent environment assumptions that enable a system to fulfill its specifications in a cooperative setting. Contrary to [4], this paper uses the same class of templates to represent the system's winning strategies in a zero-sum setting.

While the computation of *permissive strategies* for the control of CPS is an established concept in the field of supervisory control1 [14,42], it has also been addressed in reactive synthesis where the considered specification class is typically more expressive, e.g., Bernet et al. [8] introduce permissive strategies that encompass all the behaviors of positional strategies and Neider et al. [31] introduce permissiveness to subsume strategies that visit losing loops at most twice. Finally, Bouyer et al. [11] take a quantitative approach to measure the permissiveness of strategies, by minimizing the penalty of not being permissive. However, all these approaches are not optimized towards strategy adaptation and thereby typically fail to preserve enough behaviors to be able to effectively satisfy subsequent objectives. A notable exception is a work by Baier et al. [23]. While their strategy templates are more complicated and more costly to compute than ours, they are *maximally* permissive (i.e., capture *all* winning strategies in the game). However, when composing multiple objectives, they restrict templates substantially which eliminates many compositional solutions that our method retains. This results in higher computation times and lower result quality for incremental synthesis compared to our approach. As no implementation of their method is available, we could not compare both approaches empirically.

Even without the incremental aspect, synthesizing winning strategies for conjunctions of ω-regular objectives is known to be a hard problem – Chatterjee et al. [16] prove that the conjunction of even *two* parity objectives makes the problem NP-complete. They provide a generalization of Zielonka's algorithm, called GenZiel for generalized parity objectives (i.e., finite conjunction of parity objectives) which is compared to our tool PeSTel in Fig. 1. While PeSTel is (in contrast to GenZiel) not complete—i.e., there exist realizable synthesis problems for which PeSTel returns no solution—our prototype implementation returns the full winning region in all 1400 benchmark instances.

Fault-tolerant control is a well-established topic in control engineering [9], with recent emphasis on the logical control layer [19,30]. While most of this work is conducted in the context of supervisory control, there are also some approaches in reactive synthesis. While [29,32] considers the *addition* of "disturbance edges" and synthesizes a strategy that tolerates as many of them as possible, we look at the complementary problem, where edges, in particular system-player edges, disappear. To the best of our knowledge, the only algorithm that is able to tackle this problem without re-computation considers Büchi games [15]. In contrast, our method is applicable to the more expressive class of Parity games.

### 2 Preliminaries

Notation. We use N to denote the set of natural numbers including zero. Given two natural numbers a, b ∈ N with a<b, we use [a; b] to denote the set {n ∈ N | a ≤ n ≤ b}. For any given set [a; b], we write i ∈even [a; b] and i ∈odd [a; b] as shorthand for i ∈ [a; b] ∩ {0, 2, 4,...} and i ∈ [a; b] ∩ {1, 3, 5,...}

1 See [18,28,37] for connections between supervisory control and reactive synthesis.

respectively. Given two sets A and B, a relation R ⊆ A × B, and an element a ∈ A, we write R(a) to denote the set {b ∈ B | (a, b) ∈ R}.

Languages. Let Σ be a finite alphabet. The notation Σ∗ and Σω respectively denote the set of finite and infinite words over Σ, and Σ∞ is equal to Σ∗ ∪ Σω. For any word w ∈ Σ∞, wi denotes the i-th symbol in w.

Game Graphs. A *game graph* is a tuple G = - V = V 0 ∪· V 1, E where (V,E) is a finite directed graph with *vertices* V and *edges* E, and V 0, V 1 ⊆ V form a partition of V . Without loss of generality, we assume that for every v ∈ V there exists v ∈ V s.t. (v, v ) ∈ E. A *play* originating at a vertex v0 is a finite or infinite sequence of vertices ρ = v0v1 ... ∈ V ∞.

Winning Conditions/Objectives. Given a game graph G, we consider winning conditions/objectives specified using a formula Φ in *linear temporal logic* (LTL) over the vertex set V , that is, we consider LTL formulas whose atomic propositions are sets of vertices V . In this case the set of desired infinite plays is given by the semantics of Φ which is an ω-regular language L(Φ) ⊆ V ω. Every game graph with an arbitrary ω-regular set of desired infinite plays can be reduced to a game graph (possibly with a different set of vertices) with an LTL winning condition, as above. The standard definitions of ω-regular languages and LTL are omitted for brevity and can be found in standard textbooks [6]. To simplify notation we use e = (u, v) in LTL formulas as syntactic sugar for u ∧ v, with as the LTL *next* operator. We further use a set of edges E = {ei}i∈[0;k] as atomic proposition to denote i∈[0;k] ei.

Games and Strategies. A *two-player (turn-based) game* is a pair G = (G, Φ) where G is a game graph and Φ is a *winning condition* over G. A strategy of Player i, i ∈ {0, 1}, is a function πi : V ∗V i → V such that for every ρv ∈ V ∗V i holds that πi (ρv) ∈ E(v). Given a strategy πi , we say that the play ρ = v0v1 ... is *compliant* with πi if vk−1 ∈ V i implies vk = πi (v0 ...vk−1) for all k. We refer to a play compliant with πi and a play compliant with both π0 and π1 as a πi *-play* and a π0π1*-play*, respectively. We collect all plays originating in a set S and compliant with πi , (and compliant with both π0 and π1) in the sets L(S, πi ) (and L(S, π0π1), respectively). When S = V , we drop the mention of the set in the previous notation, and when S is singleton {v}, we simply write L(v, πi ) (and L(v, π0π1), respectively).

Winning. Given a game G = (G, Φ), a play ρ in G is *winning for* Player 0, if ρ ∈ L(Φ), and it is winning for Player 1, otherwise. A strategy πi for Player i is *winning from a vertex* v ∈ V if all plays compliant with πi and originating from v are winning for Player i. We say that a vertex v ∈ V is *winning for* Player i, if there exists a winning strategy πi from v. We collect all winning vertices of Player i in the Player i *winning region* Wi ⊆ V . We always interpret winning w.r.t. Player 0 if not stated otherwise.

Strategy Templates. Let π0 be a Player 0 strategy and Φ be an LTL formula. Then we say π0 *follows* Φ, denoted π0 -Φ, if for all π0-plays ρ, ρ belongs to L(Φ), i.e. L(π0) ⊆ L(Φ). We refer to a set Ψ = {Ψ1,...,Ψk} of LTL formulas as *strategy templates* representing the set of strategies that follows Ψ1 ∧ ... ∧ Ψk. We say a strategy template Ψ is *winning from a vertex* v for a game (G, Φ) if every Player 0 strategy following the template Ψ is winning from v. Moreover, we say a strategy template Ψ is *winning* if it is winning from every vertex in W0. In addition, we call Ψ *maximally permissive* for G, if every Player 0 strategy π which is winning in G also follows Ψ. With slight abuse of notation, we use Ψ for the set of formulas {Ψ1,...,Ψk}, and the formula Ψ1 ∧ ... ∧ Ψk, interchangeably.

Set Transformers. Let G = (V = V 0 ∪· V 1, E) be a game graph, U ⊆ V be a subset of vertices, and a ∈ {0, 1} be the player index.  In the following, we introduce two types of attractor operators: attra G(U) that computes the set of vertices from which Player a can force at least a single visit to U in *finitely many* steps, and the universal attractor uattrG(U) that computes the set of vertices from which both players are forced to visit U. For the following, let pre ∈ {upre, cprea}

$$\mathsf{pre}\_G^1(U) = \mathsf{pre}\_G(U) \cup U \qquad \mathsf{pre}\_G^i(U) = \mathsf{pre}\_G(\mathsf{pre}\_G^{i-1}(U)) \cup \mathsf{pre}\_G^{i-1}(U) \qquad (3)$$

$$\mathbf{attr}\_G^a(U) = \cup\_{i \ge 1} \mathbf{cpu}\_G^{a,i}(U) \quad \mathbf{uattr}\_G(U) = \cup\_{i \ge 1} \mathbf{upper}\_G^i(U) \tag{4}$$

### 3 Computation of Winning Strategy Templates

Given a 2-player game G with an objective Φ, the goal of this section is to compute a *strategy template* that characterizes a large class of winning strategies of Player 0 from a set of vertices U ⊆ V in a local, permissive, and computationally efficient way. These templates are then utilized in Sect. 5.1 for computational synthesis. In particular, this section introduces three distinct template classes—safety templates (Sect. 3.1), live-group-templates (Sect. 3.2), and colive-templates (Sect. 3.3) along with algorithms for their computation via safety, Büchi, and co-Büchi games, respectively. We then turn to general parity objectives which can be thought of as a sophisticated combination of Büchi and co-Büchi games. We show in Sect. 3.4 how the three introduced templates can be derived for a general parity objective by a suitable combination of the previously introduced algorithms for single templates. All presented algorithms have the same worst-case computation time as the standard algorithms solving the respective game. This shows that extracting strategy *templates* instead of 'normal' strategies does not incur an additional computational cost. We prove the soundness of the algorithms and discuss the complexities in the full version [5, Appendix A].

#### 3.1 Safety Templates

We start the construction of strategy templates by restricting ourselves to games with a safety objective—i.e., G = (G, Φ) with Φ := U for some U ⊆ V . A winning play in a safety game never leaves U ⊆ V . It is well known that such games allow capturing *all* winning strategies by a simple local template which essentially only allows Player 0 moves from winning vertices to other winning vertices. This is formalized in our notation as a safety template as follows,

Theorem 1 ([8, Fact 7]). *Let* G = (G, U) *be a safety game with winning region* W0 *and* S = {(u, v) ∈ E | - u ∈ V 0 ∩ W0 ∧ (v /∈ W0)}*. Then*

$$\Psi\_{\text{UNSAFE}}(S) := \Box \bigwedge\_{e \in S} \neg e,\tag{5}$$

*is a winning strategy template for the game* G *which is also maximally permissive.*

It is easy to see that the computation of the safety template Ψunsafe(S) reduces to computing the winning region W0 in the safety game (G, U) and extracting S. We refer to the edges in S as *unsafe edges* and we call this algorithm computing the set S as SafetyTemplate(G, U). Note that it runs in O(m) time, where m = |E|, as safety games are solvable in O(m) time.

#### 3.2 Live-Group Templates

As the next step, we now move to simple liveness objectives which require a particular vertex set I ⊆ V to be seen infinitely often. Here, winning strategies need to stay in the winning region (as before) but in addition always eventually need to make progress towards the vertex set I. We capture this required progress by *live-group templates*—given a group of edges H ⊆ E, we require that whenever a source vertex v of an edge in H is seen infinitely often, an edge e ∈ H (not necessarily starting at v) also needs to be taken infinitely often. This template ensures that compliant strategies always eventually make progress towards I, as illustrated by the following example.

*Example 1.* Consider the game graph in Fig. 2 where we require visiting {c, d} infinitely often. To satisfy this objective from vertex a, Player 0 needs to not get stuck at a, and should not visit b always (since Player 1 can force visiting a again, and stop Player 0 from satisfying the objective). Hence, Player 0 has to always eventually leave a and go to {c, d}. This can be captured by the livegroup {eac, ead}. Now if the play comes to a infinitely often, Player 0 will go to either c or d infinitely often, hence satisfying the objective.

Formally, such games are called *Büchi games*, denoted by G = (G = (V,E), Φ) with Φ := ♦I, for some I ⊆ V . In addition, a *live-group* H = {ej}j≥0 is a set of edges ej = (sj , tj ) with source vertices *src*(H) := {sj}j≥0. Given a set of live-groups H = {Hi}i≥0 we define a live-group template as

$$\Psi\_{\rm{LIVE}}(\mathcal{H}) \coloneqq \bigwedge\_{i \geq 0} \Box \Diamond src(H\_i) \implies \Box \Diamond H\_i. \tag{6}$$

# Algorithm 1. BüchiTemplate(G, I)

Input: A game graph G, and a subset of vertices I Output: A set of unsafe edges S and a set of live-groups H 1: W0 ← Büchi(G, I); S ← SafetyTemplate(G, W0); 2: G ← G|W0 ; I ← I ∩ W0; 3: H ← ReachTemplate(G, I); 4: return (S, H) 5: procedure ReachTemplate(G, I ⊆ V ) 6: H←∅; 7: while I = V do 8: A ← uattrG(I); B ← cpre0 G(A); H←H∪{Edges(B,A)}; I ← A ∪ B; 9: return H

The live-group template says that if some vertex from the source of a live-group is visited infinitely often, then some edge from this group should be taken infinitely often by the following strategy.

Intuitively, winning strategy templates for Büchi games consist of a safety template conjuncted with a live-group template. While the former enforces all strategies to stay within the winning region W, the latter enforces progress w.r.t. the goal set I within W. Therefore, the computation of a winning strategy template for Büchi games reduces to the computation of the unsafe set S to define Ψunsafe(S) in (5) and the live-group H to define Ψlive(H) in (6). We denote by BüchiTemplate(G, I) the algorithm computing the above as detailed in Algorithm 1. The algorithm uses some new notations that we define here. Here, the function Büchi solves a Büchi game and returns the winning region (e.g., using the standard algorithm from [17]), Edges(X, Y ) = {(u, v) ∈ E | u ∈ X, v ∈ Y }, is the set of edges between two subsets of vertices X and Y . G|U := - U = U0 ∪· U1, E s.t. U0 := V 0∩U, U1 := V 1∩U, and E := E∩(U×U) denotes the restriction of a game graph G := - V = V 0 ∪· V 1, E to a subset of its vertices U ⊆ V . We have the following formal result.

Theorem 2. *Given a Büchi game* G = (G, ♦I) *for some* I ⊆ V *, if* (S, H) = BüchiTemplate(G, I) *then* Ψ = {Ψunsafe(S), Ψlive(H)} *is a winning strategy template for the game* G*, computable in time* O(nm)*, where* n = |V | *and* m = |E|*.*

While live-group templates capture infinitely many winning strategies in Büchi games, they are *not* maximally permissive, as exemplified next.