--- title: "LTL Realizability via Safety and Reachability Games" authors: - "Alberto Camacho" - "Christian Muise" - "Jorge A. Baier" - "Sheila A. McIlraith" doi: "10.24963/ijcai.2018/651" url: "https://ijcai.org/proceedings/2018/651" pdf: "https://ijcai.org/proceedings/2018/0651.pdf" venue: "Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence" year: 2018 pages: "4683-4691" track: "Main track" keywords: - "Planning and Scheduling: Planning and Scheduling" - "Planning and Scheduling: Planning under Uncertainty" - "Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis" - "Planning and Scheduling: Applications of Planning" --- # LTL Realizability via Safety and Reachability Games Alberto Camacho, Christian Muise, Jorge A. Baier, Sheila A. McIlraith *Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence*, pages 4683-4691. DOI: [10.24963/ijcai.2018/651](https://doi.org/10.24963/ijcai.2018/651) ## Abstract In this paper, we address the problem of LTL realizability and synthesis. State of the art techniques rely on so-called bounded synthesis methods, which reduce the problem to a safety game. Realizability is determined by solving synthesis in a dual game. We provide a unified view of duality, and introduce novel bounded realizability methods via reductions to reachability games. Further, we introduce algorithms, based on AI automated planning, to solve these safety and reachability games. This is the the first complete approach to LTL realizability and synthesis via automated planning. Experiments illustrate that reductions to reachability games are an alternative to reductions to safety games, and show that planning can be a competitive approach to LTL realizability and synthesis. ## Full text ## 1 Introduction LTL synthesis aims to compute a strategy that satisfies a Linear Temporal Logic (LTL) specification. The problem was first proposed in the context of reactive synthesis, and is central to the automated construction of controllers and certain classes of programs [Pnueli and Rosner, 1989]. LTL realizability and synthesis are commonly addressed as a two-player game between an agent and the environment, played over automata transformations of the LTL specification (so-called automata games). Each player has a disjoint set of variables, and the objective is to synthesize a strategy for setting the agent's ("controllable") variables such that the LTL specification is guaranteed to be satisfied, no matter how the environment sets its ("uncontrollable") variables. Traditional approaches to LTL realizability and synthesis assume that the agent plays first. Interestingly, in recent years there has been a surge in the development of modern LTL synthesis tools based on automata games, and whereas LTL synthesis tool Lily [Jobstmann and Bloem, 2006] adopts an agent-first play protocol, many of the most successful LTL synthesis tools such as Unbeast [Ehlers, 2010], Acacia, and Acacia + [Filiot et al., 2009; Bohy et al., 2012] adopt an inverted turn protocol, where the environment plays first. Indeed, this inverted turn-taking has become the standard used in di�erent incarnations of SYNTCOMP, the annual reactive synthesis competition (e.g. [Jacobs et al., 2017]). SYNTCOMP has promoted standardization and facilitated tool comparison with the introduction of the high-level LTL input language TLSF [Jacobs et al., 2016]. Participating tools (including Acacia + ) are compliant with TLSF. � This work was conducted while the author was a�liated with CSAIL, Massachusetts Institute of Technology. To describe the di�erent semantics associated with turntaking protocols, the notions of Mealy- and Moore-type semantics has been introduced (e.g. [Ehlers, 2011; Khalimov et al., 2013]), where intuitively Mealy-type semantics correspond to settings where the environment plays first, and Moore-type semantics correspond to settings where the agent plays first. The names originate from Mealy and Moore machines. When a winning strategy exists for one of these semantics, the strategy has a finite representation and is typically conveyed in terms of Mealy (resp. Moore) machines. Inverting the order of agent-environment turn-taking corresponds to playing a dual game. We aim to provide a unified view of duality results for LTL realizability and synthesis, and automata games. To this end, we review the connection between LTL synthesis and automata games, and formalize a duality result for existence of winning strategies in automata games that replicates the duality results for synthesis. We further investigate di�erent reductions to automata games that exploit duality to determine realizability, and introduce novel techniques that exploit these correspondences. We exploit mappings from LTL synthesis to games, together with duality results, to chronicle di�erent techniques to solve LTL realizability and synthesis (Table 1). These techniques extend well-known approaches, and establish the connection between Mealy and Moore semantics for LTL realizability and synthesis, and games over Universal k-coB¨uchi Word (UkCW) automata and Non-deterministic k-B¨uchi Word (NkBW) automata. From an algorithmic perspective, our approaches to LTL realizability via reduction to NkBW games provide an alternative to existing techniques based on UkCW. Whereas the latter are safety games, the former are reachability games. Finally, we address the realizability problem in safe and co-safe specifications, and show how these can be solved more e�ciently. We further present the first complete approach to LTL synthesis via Fully Observable Non-Deterministic (FOND) planning. Our approach constructs a planning problem that simulates an automata game, and that can be solved using state-ofthe-art planners. While our contributions are intended to be largely theoretical, we conducted preliminary experiments to assess the practicality of the di�erent techniques for LTL realizability and synthesis that we present. Preliminary results show that techniques employing NkBW automata can complement existing techniques based on UkCW automata, addressing realizability and synthesis problems that otherwise cannot be solved by existing tools. Moreover, they show that automated planning technology (and, in particular, FOND) can be an e�cient approach to LTL realizability and synthesis. Finally, we believe that the NkBW game reductions presented here open the door to novel bounded realizability methods for LTL realizability and synthesis as reachability games, providing an alternative to bounded synthesis [Kupferman and Vardi, 2005; Schewe and Finkbeiner, 2007]. ## 2 Background ## 2.1 Automata on InfiniteWords A non-deterministic automaton is a tuple A = hQ; � ; q0; �; �i, where Q is a finite set of automaton states, � is a finite alphabet of input letters, q0 2 Q is the initial state of the automaton, � � Q � � � Q is a transition relation, and � � Q is an accepting condition. We sometimes write �(q; �) to denote the set Q 0 � Q such that (q; �; q 0 ) 2 � for every q 0 2 Q 0 . Intuitively, an automaton A in state q can transition into any state in �(q; �) when it reads an input letter �. When j�(q; �)j = 1 for every q 2 Q and � 2 �, the automaton is deterministic. � ! denotes the set of all infinite words over �. A run of A on word w = �1; �2; : : : 2 � ! is an infinite sequence of states � = q0; q1; : : : 2 Q ! where (qi�1; �i; qi) 2 � for every i > 0. It is useful to define operators occ� : Q ! N[ f0;1g, indexed by runs �, that return for each q 2 Q the number of occurrences of q in �. In what follows, we review three types of acceptance conditions. A run � is accepting with the B¨uchi condition if occ�(q) = 1 for some q 2 � - that is, when some state in � occurs infinitely often in �. Conversely, a run � is accepting with the coB¨uchi condition if occ�(q) < 1 for every q 2 �. Finally, � is accepting with the k-B¨uchi (resp. k-coB¨uchi) condition for k 2 N [ f0g if occ�(q) � k for some q 2 � (resp. occ�(q) � k for every q 2 �). The language of an automaton A, L(A), is the set of infinite words accepted by A. We say a non-deterministic automaton A accepts a word w when some run of A on w is accepting - that is, A has non-deterministic branching factor. In contrast, when A is a universal automaton all runs of A on w must be accepting - that is, A has universal branching factor. Following the naming conventions described above, Nondeterministic B¨uchi Word (NBW) automata and Nondeterministic k-B¨uchi Word (NkBW) automata have nondeterministic branching factor and B¨uchi and k-B¨uchi acceptance condition, respectively. Similarly, Universal CoB¨uchi Word (UCW) automata and Universal k-coB¨uchi Word (UkCW) automata have universal branching factor and coB¨uchi and k-coB¨uchi acceptance condition, respectively. For clarity, throughout the paper we use a pairwise notation to denote the acceptance condition of automata. For example, Uk = (A; UkCW) and Nk = (A; NkBW) denote automaton A with, respectively, UkCW and NkBW acceptance conditions. This notation makes it easy to write automata that di�er in their accepting conditions. In particular, it facilitates notation in complementation rules (cf. Proposition 1). The complementation of an automaton A is the task of constructing an automaton that accepts the words that are not in L(A). Proposition 1. The complementation of Uk is Nk+1. ## 2.2 Linear Temporal Logic Linear Temporal Logic (LTL) extends propositional logic with the unary temporal operator "next" and the binary temporal operator "until". As such, ' stands for "next '" and 'U stands for "' until ". LTL formulae over a set of propositions AP are evaluated over infinite sequences s0s1 � � � , where each si is a subset of AP. If � = s0s1 � � � , then, for every i � 0: - � �; i j= ' if ' is a propositional formula and si j= '. - � �; i j= ' i� �; i + 1 j= '. - � �; i j= 'U i� there exists a j � i such that s j j= and for every k 2 fi; : : : ; j � 1g, sk j= '. Finally we say that � is a model of ', denoted � j= ', i� �; 0 j= '. Three other common temporal operators, "eventually '" (� '), "always '" (� '), and " releases '" ( R'), can be defined as follows: � ' � >U', � ' � :�:', and R' � :(: U:'). ## 2.3 LTL and Automata It is well-known that for an LTL formula ' one can construct an automaton N' = (A';NBW) that accepts all and only the infinite words that satisfy '. The construction is worst-case exponential in the size of the formula. An UCW automaton U ' that accepts the models of ' can be obtained from the construction of an NBW automaton that accepts the models of :'. Formally, U' = (A; UCW) accepts the models of ' i� N:' = (A;NBW) accepts the models of :' (cf. [Kupferman and Vardi, 2005]). Lemma 1 summarizes these results. Lemma 1. Given an LTL formula ', it is possible to build an NBW automaton N', and a UCW automaton U', such that L(N') = L(U') = fw 2 � ! j w j= 'g. The constructions are worst-case exponential in the size of '. ## 2.4 Fully Observable Non-Deterministic Planning Here we briefly describe the Fully Observable NonDeterministic (FOND) setting, and refer the interested reader to Ge�ner and Bonet [2013] for a more thorough description. A FOND problem is a tuple hF;O; I;Gi, where F is a set of fluents (atomic propositions whose truth value can change over time); I � F are the fluents true in the initial state; G � F, are the fluents that must hold in a goal state; and O is the set of (possibly non-deterministic) operators or action schemas. Each o 2 O is made up of Preo (the fluents that must hold for o to be executable) and E�o (the set of possible e�ects for o, one of which will update the state). States are represented by a set of fluents (all those not in the set are presumed false) and partial states are represented by a set of literals (i.e., fluents or their negation). An action is a ground operator. The outcome of action a in state s is another state s 0 that results from updating s with one of the e�ects of the ground operator o corresponding to a. A distinguishing property of FOND planning is that the action outcome is not known until run time, and so all contingencies must be planned for. For this reason, solutions to a FOND problem take the form of a policy � that maps the state of the world to the action that should be executed. An execution of a policy � from state s0 is a sequence of states s0; s1; : : : such that each si+1 is an outcome of �(si) in si. Cimatti et al. [2003] defined di�erent classes of solutions to a FOND problem. Here, we examine two of them. A strong solution is a policy that is guaranteed to achieve the goal regardless of non-determinism. Strong cyclic solutions are less restrictive and guarantee goal reachability in the presence of fairness, which presumes that all the action outcomes in a given state would manifest infinitely often. As the name suggests, a strong cyclic solution may revisit states. Strong cyclic solutions have the property stated in Proposition 2. Proposition 2 (Strong Cyclic Solution). A policy � is a strong cyclic solution i� for every state s reachable by � there exists an execution that achieves the goal from s. Automated planning technology is highly optimized, and typically used for computation of plans or policies that achieve a prescribed goal after execution of a finite number of actions - that can be unbounded in strong cyclic plans. Patrizi et al. [2013] proposed a means of synthesizing infinite plans for planning domains with LTL goal formulae and fair non-deterministic actions. Their technique compiles the original domain into a new domain in a way that executions of a strong cyclic solution to the modified domain produce infinite plans in the original domain. The approach is limited to the class of LTL formulae that can be compiled into deterministic B¨uchi automata. ## 3 LTL Realizability and Synthesis The realizability and synthesis problems for an LTL specification were first posed by Pnueli and Rosner in 1989. Since then, the scholarly literature has explored two slightly different interpretations of an LTL specification in the context of synthesis. In this paper, we study both interpretations, which di�er in their semantics, distinguishing them via the subscript s 2 � Mealy;Moore � notation (cf. Definition 1). We adopt the terms Mealy and Moore semantics, which have been used previously in the synthesis literature (e.g. [Ehlers, 2011; Khalimov et al., 2013]). A strategy for an LTL specification hX;Y; 'is is a function f : (2 X ) � ! 2 Y that maps histories, or finite sequences of subsets of X, into subsets of Y. A strategy f is winning when, for every infinite sequence X1X2 � � � of subsets of X, either: (i) s = Mealy and f(Xi [ f (X1 � � � Xi))gi�1 satisfies '; or (ii) s = Moore and f(Xi [ f (X0 � � � Xi�1))gi�1 satisfies ' for some constant X0, typically set to the empty trace �. Winning strategies for an LTL specification hX;Y; 'iMoore are also winning strategies for hX; Y; 'iMealy, but the opposite does not hold in general (see example below). The realizability problem consists of determining existence of a winning strategy, and the synthesis problem consists of computing one (Definition 2). For unrealizable specifications, a certificate of unrealizablity is a strategy g : (2 Y ) � ! 2 X that prevents the agent from realizing '. Lemma 2 formulates a well-known duality between the two semantics in LTL realizability. Definition 1. An LTL specification is a tuple hX;Y; 'is, where X and Y are two finite and disjoint sets of variables, ' is an LTL formula over variables in X [ Y, and s 2 fMealy;Mooreg. Definition 2. The realizability problem for an LTL specification hX; Y; 'is is to determine whether there exists a winning strategy. The synthesis problem for a realizable LTL specification consists of computing a winning strategy. We say that an LTL specification is unrealizable when it is not realizable. Lemma 2 (Duality). An LTL specification hX;Y; 'iMealy is realizable i� hY; X; :'iMoore is unrealizable. Example LTL specification hfxg ; fyg ; �(x $ y)iMealy is realizable, and has a winning strategy f that maps each sequence X1 � � � Xn 2 (2 X ) � to fyg if Xn = fxg, and to ; otherwise. On the other hand, hfxg ; fyg ; �(x $ y)iMoore is unrealizable. An unrealizability certificate g : (2 Y ) � ! 2 X can be constructed by assigning g(fyg) = ; and g(;) = fxg. Clearly, plays that start with a prefix (g( f (X0))[ f (X0)) cannot satisfy �(x $ y). ## 3.1 Automata Games Following Thomas [1995], in this paper a two-player game is defined with respect to two finite sets of variables, X and Y, and an automaton A with alphabet � = 2 X[Y whose language describes which plays are winning in the game. In this paper we exploit the correspondence between LTL synthesis and games in various forms. To facilitate readability, in this paper we opt to represent games with a tuple hX; Y; Ais, where s 2 � Moore;Mealy � . In the following, we formalize automata games, and present duality results that are analogous to those for LTL synthesis. We first describe the dynamics of a game hX;Y;AiMoore, which corresponds to the definition of automata games commonly used in the literature. A game hX;Y;AiMoore has two players, P1 and P2. In each round of the game, P1 selects a subset of variables Yi � Y, followed by P2, which selects a subset of variables Xi � X. The game is played an infinite number of rounds, and so a play consists of an infinite word w = f(Xi [ Yi) j Xi � X; Yi � Ygi�1. The play is winning (for P1) if A accepts w, and the game is winning (for P1) if P1 has a strategy that only yields winning plays, regardless of the moves of P2. Formally, hX;Y;AiMoore is winning if there exists an strategy f : (2 X ) � ! 2 Y such that, for any sequence fXigi�1 of moves of P2, A accepts the infinite word w = f(Xi [ f (X0 � � � Xi�1))gi�1 for some constant X0. In this paper we are also interested in examining the conditions under which player P2 has a winning strategy. We write hX;Y;AiMealy to denote a game with inverted turns with respect to hX;Y;AiMoore. In each round, player P1 selects a subset of variables of X, followed by player P2, which selects a subset of variables of Y. The di�erence now is that the game is P2-centric. We say that the game is winning (for P2) if there exists an strategy g : (2 X ) � ! 2 Y such that, for any sequence fXigi�1 of moves of P1, the play w = f(Xi [ f (X1 � � � Xi))gi�1 is accepted by A. Proposition 3 below is analogous to Lemma 2, and formalizes the well-known zero-sum property of automata games. That is, player P1 has a strategy to win a game hX;Y;AiMoore i� player P2 has no strategy to win the dual game hY;X;AiMealy, where A is an automaton that accepts the complement language of A. Note that duality inverts the set of controllable variables. Throughout this paper we exploit a particular case of Proposition 3 with two classes of automata that recognize complement languages: UkCW and NkBW automata. We formalize the result in Lemma 3. Proposition 3 (Duality). A game hX;Y;AiMoore is winning (for P1) i� the game hY; X;AiMealy is not winning (for P2). Lemma 3 (Duality). Let Uk = (A;UkCW) and Nk = (A; NkBW). A game hX;Y;UkiMoore is winning i� hY;X;Nk+1iMealy is not winning. Likewise, hX;Y;UkiMealy is winning i� hY; X; Nk+1iMoore is not winning. ## 3.2 LTL Realizability and Automata Games The correspondence between LTL realizability and automata games has been commonly exploited to approach LTL realizability and synthesis (e.g. [Jobstmann and Bloem, 2006; Filiot et al., 2009; Ehlers, 2010]). Theorem 1 formalizes the mapping, which preserves winning strategies. Typically, automata-based approaches to LTL synthesis rely on deterministic automata. NBW automata can be determinized (into Rabin automata) with the Safra construction. This construction, unfortunately, is very involved and not amenable to symbolic methods. Reportedly, the best tools cannot even handle relatively simple automata with more than 6 states. Theorem 1. Let ' be an LTL formula over X [ Y, and let A' be an automaton that accepts the models of '. � is a winning strategy for hX; Y; 'iMoore (resp. hX; Y; 'iMealy) i� � is a winning strategy for hX;Y;A'iMoore (resp. hX;Y;A'iMealy). Safety Games As an alternative to avoid Safra's construction, so-called safraless methods reduce the synthesis problem to a series of safety games over UkCW automata [Kupferman and Vardi, 2005]. In a safety game, all plays that violate the LTL specification formula ' have a bad prefix. A bad prefix is a finite trace � from which it is no longer possible to satisfy '. That is, any infinite trace � 0 with prefix � is such that � 0 6 j= '. The challenge in a safety game is for the agent to avoid bad prefixes. The advantage of using UkCW automata is that these can be determinized e�ciently, using well-known methods derived from the powerset construction commonly used to determinize finite-state automata. Reachability Games In a reachability game, winning plays have a good prefix, that is, a finite trace � such that any infinite trace � 0 with prefix � satisfies the specification. In particular, games over NkBW automata are reachability games. ## 4 Reductions to Automata Games In this section we introduce a collection of techniques to reduce LTL realizability into a series of games defined over UkCW and NkBW automata. The reductions rely on Theorems 2, 3, 4, and 5, and are summarized in Table 1. Theorem 2. Let A = (A;UCW) be an automaton that accepts the models of :'. The following are equivalent: - � hX;Y; 'iMealy is unrealizable - � hY;X; (A;UkCW)iMoore is winning for some k in 2 O(jAj) - � hX;Y; (A; NkBW)iMealy not winning for some k in 2 O(jAj) Proof sketch. By Lemma 2, hX;Y; 'iMealy is unrealizable i� hY;X; :'iMoore is realizable. By well-known results on bounded synthesis (e.g. [Kupferman, 2006]), this occurs i� hY;X; (A;UkCW)iMoore is winning for some k in 2 O(jAj) . By Lemma 3, this occurs i� hX;Y; (A;NkBW)iMealy is not winning for some k worst-case exponential in the size of A. � Theorem 3. Let A = (A; NBW) be an automaton that accepts the models of :'. The following is equivalent: - � hX;Y; 'iMealy is realizable - � hY;X; (A; NkBW)iMoore is not winning for some k in 2 O(jAj) - � hX;Y; (A;UkCW)iMealy is winning for some k in 2 O(jAj) Proof sketch. By Lemma 2, hX;Y; 'iMealy is realizable i� hY;X; :'iMoore is unrealizable. This occurs i� hY;X; (A;NkBW)iMoore is not winning for some k < 1. By Lemma 3, this occurs i� hX;Y; (A;UkCW)iMealy is winning for some k < 1. The results for bounded synthesis (e.g. [Kupferman, 2006]) set the exponential bound on k. � Theorem 4. Let A = (A;UCW) be an automaton that accepts the models of ' The following is equivalent: - � hX;Y; 'iMoore is realizable - � hX;Y; (A;UkCW)iMoore is winning for some k in 2 O(jAj) - � hY;X; (A; NkBW)iMealy is not winning for some k in 2 O(jAj) Proof sketch. It follows from negating Theorem 2 and applying the duality results in Lemmas 2 and 3. � Theorem 5. Let A = (A; NBW) be an automaton that accepts the models of '. The following is equivalent: - � hX;Y; 'iMoore is unrealizable - � hX;Y; (A; NkBW)iMoore is not winning for some k in 2 O(jAj) - � hY;X; (A;UkCW)iMealy is winning for some k in 2 O(jAj) Proof sketch. It follows frin negating Theorem 3 and applying the duality results in Lemmas 2 and 3. � Bounded Realizability and Synthesis Table 1 summarizes the results of the theorems above into a series of tests to determine realizability and unrealizability of an LTL specification. The tests based on reductions to UkCW games (i.e. safety games) are well known, and commonly referred to as bounded synthesis methods [Schewe and Finkbeiner, 2007], which build upon safraless methods [Kupferman and Vardi, 2005]. These tests are constructive, meaning that a winning strategy for the reduced game is a winning strategy for the original specification - in case it is realizable -, or a certificate of unrealizability - in case it is unrealizable. Bounded synthesis has been a successful approach to synthesis, and nowadays many modern tools exploit reductions to UkCW games in some way (e.g. Lily [Jobstmann and Bloem, 2006], Unbeast [Ehlers, 2010], and Acacia/Acacia + [Filiot et al., 2009; Table 1: Strategies to determine realizability and unrealizability of an LTL specification via reduction to automata games. When ' is a safe (resp. co-safe) LTL formula, strategies that are good for safe (resp. good for co-safe) formulae only require tests with k = 0 in UkCW games; and k = 1 in NkBW games. Constructive tests yield a winning strategy or certificate, as appropriate. | Specification | Construction of A | Test | Good for | Constructive | Thm | |-----------------|---------------------|----------------------------------------------------------|------------|----------------|-------| | hX;Y; 'iMealy | L(A;NBW) = L(') | 9k:hY;X; (A;UkCW)iMoore winning for P1()unrealizable | co-safe | yes | 2 | | hX;Y; 'iMealy | L(A;NBW) = L(') | 9k:hX;Y; (A;NkBW)iMealy not winning for P2()unrealizable | co-safe | no | 2 | | hX;Y; 'iMealy | L(A;UCW) = L(') | 9k:hY;X; (A;NkBW)iMoore not winning for P1() realizable | safe | no | 3 | | hX;Y; 'iMealy | L(A;UCW) = L(') | 9k:hX;Y; (A;UkCW)iMealy winning for P2() realizable | safe | yes | 3 | | hX;Y; 'iMoore | L(A;UCW) = L(') | 9k:hX;Y; (A;UkCW)iMoore winning for P1() realizable | safe | yes | 4 | | hX;Y; 'iMoore | L(A;UCW) = L(') | 9k:hY;X; (A;NkBW)iMealy not winning for P2() realizable | safe | no | 4 | | hX;Y; 'iMoore | L(A;NBW) = L(') | 9k:hX;Y; (A;NkBW)iMoore not winning for P1()unrealizable | co-safe | no | 5 | | hX;Y; 'iMoore | L(A;NBW) = L(') | 9k:hY;X; (A;UkCW)iMealy winning for P2()unrealizable | co-safe | yes | 5 | Bohy et al., 2012]). The tests based on reductions to NkBW games (i.e. reachability games) are novel. These tests determine realizability and unrealizability. By way of analogy to bounded synthesis, we refer to them as bounded realizability methods. Note that a complete approach for LTL realizability and synthesis would combine at least two of these approaches in parallel or with interleaved search. Safe and Co-Safe LTL Specifications Di�erent syntactic characterizations of LTL formulas have been studied (e.g. [Sistla, 1994]). Here, we examine the safe and co-safe fragment of LTL [Kupferman and Vardi, 2001]. Safe properties assert that something bad never happens. Co-safe properties are dual, and assert that something good eventually happens. The following syntactic fragments of LTL express safe, and co-safe properties: Safe and co-safe LTL formulae can be transformed into automata with absorbing rejecting and accepting states, respectively [Kupferman and Vardi, 2001]. We observe that with these automata constructions, realizability of safe and co-safe formulae can be determined by performing only one test (Theorem 6). Theorem 6. LTL realizability for safe (resp. co-safe) specifications can be determined with strategies that are good for safe (resp. good for co-safe) formulae (cf. Table 1) by performing a single test with k = 0, in the case of reductions to UkCW games, and k = 1, in the case of reductions to NkBW games. Proof sketch. The proof follows from applying Lemma 3 in Theorems 2, 3, 4, and 5, with a construction of an NBW with absorbing accepting states. Here, we sketch the proof of one case. Let ' be a co-safe LTL formula, and let A = (A; NBW) be an automaton that accepts the models of '. hX;Y; 'iMoore is realizable i� hX;Y; (A;NkBW)iMoore is winning for all k, but this happens i� hX;Y; (A;NkBW)iMoore is winning for k = 1 (because A has absorbing accepting states). Lemma 3 derives that this only happens i� hY;X; (A;UkCW)iMealy is not winning for k = 0. � ## 5 Automata Games via Planning In recent years there has been increased interest in the development of algorithms that exploit automated planning techniques to synthesize programs of varying sorts including so-called generalized planning (e.g., [Aguas et al., 2016; Bonet et al., 2017]) and LTL synthesis. Camacho et al. [2018b] studied the correspondence between LTL synthesis and planning, and presented an algorithm to synthesize strategies, via planning, that is complete when the formula is transformed into deterministic B¨uchi automata, but not in general. Together with this work, it constitutes the first approach to LTL synthesis via planning. Also related to this work is [Camacho et al., 2018a], where planning technology is used to solve LTL synthesis for LTL interpreted over finite words [De Giacomo and Vardi, 2015]. Approaching LTL synthesis as planning enables the use of highly optimized search techniques and heuristics. Planning algorithms can reason about action costs, stochasticity, plan quality, and preferences. Our work opens the door to using planning technology for richer notions of LTL synthesis, including those that optimize for high-quality strategies [Almagor and Kupferman, 2016]. In this section we present reductions of UkCW and NkBW games to FOND planning. These reductions comprise the first complete approach to LTL realizability and synthesis via planning. For an LTL specification hX;Y; 'i, and a test strategy from Table 1, our approach consists of three steps: - (1) construct an automaton A - (2) solve a sequence of automata games via FONDplanning - (3) determine realizability or unrealizability In addition, and if the test is constructive, a fourth step can be performed to synthesize a winning strategy - if realizable - or a certificate of unrealizability - if unrealizable. Step 1: LTL to automata In the first step we construct an automaton (A; NBW) that accepts the models of ' or :', according to the strategy selected from Table 1. Our FOND compilation requires post-processing of the set of automaton transitions. Each transition t = (q; guard(t); q 0 ) in A with guard guard(t) = W i ci in DNF is decomposed into a set of transitions ti = (q; ci; q 0 ). Each ti has guard ci, that is a conjunctive formula over variables in X [ Y. For each ti, we denote by macro(ti) the set of transitions derived from t. It can be proved that the decomposition of the transitions does not a�ect the language accepted by the automaton. Step 2: Construction of a FOND Problem The second step takes as input the automaton generated in Step 1, and constructs a series of FOND problems Pk, for k � 0. Each Pk simulates a game over a UkCW or NkBW automaton in accordance with the strategy selected from Table 1. We detail the FOND compilations for UkCW and NkBW automata games in Sections 5.1 and 5.2. Step 3: Determine Realizability or Unrealizability The compiled FOND problems Pk have the following property: Pk has a solution i� the simulated automata game is winning. This property is exploited in the following manner: our technique searches for existence of solutions to the FOND problems Pk for k = 0; 1; : : : until the test in Table 1 is passed. Note that the tests are not guaranteed to terminate if, for instance, LTL realizability for an unrealizable specification is checked. However, termination can be achieved by combining two strategies in parallel: one that checks realizability, and another that checks unrealizability. Step 4: Construction of a strategy A finite state controller that implements a strategy that solves the synthesis p roblem for specification ' can be constructed from a policy for Pk. See [Patrizi et al., 2013; Camacho et al., 2017] for details. ## 5.1 UkCWGames via Planning Figure 1 describes the details of the compilation of a game with automaton A = hQ; � ; q0; �; �i into a FOND planning problem Pk. For illustration purposes, we assume the game is in the form hX;Y; (A;UkCW)iMealy, that is, we are searching for winning strategies for P2. At the end of the section we show how the dynamics of Pk can be modified to compile games in the form hX; Y; (A; UkCW)iMoore. The dynamics of Pk simulates an infinite sequence of rounds in the two-player game. Each round is divided into three sequential stages. The first stage simulates the move of the environment and agent players. The move of P1 is simulated with a cascade of actions that non-deterministically assign a value to the variables in X. In turn, the moves of P2 are simulated with a cascade of deterministic actions that assign a value to the variables in Y. As a consequence of the player moves, some automaton transitions are deemed unfeasible. The second stage performs all automaton transitions. Fluents F(q) are true in a planning state if there exists a run of A on the play being simulated that ends in q. The third stage sets the value of the counters associated to each automaton state q. A fluent newCnt(q; m) is true if there exists a run of A on the simulated play that ends in q and hits m accepting states. The fluent oldCnt(q; m) keeps track of the maximum number of hits for a fluent q. At the end of the third stage, the first stage is reestablished to simulate the next round. There are two important things to notice about the dynamics of Pk. First, when an input word being simulated is not accepted by (A;UkCW) (that is, a run visits more than k accepting states), a deadend in Pk is incurred. This is because a fluent newCnt(q; k + 1) prevents syncF actions to disable the fluent F(q), action continue is no longer applicable, and the first stage can no longer be reestablished. Second, the non-determinism of action continue ensures that execution of strong-cyclic solutions yield an infinite number of rounds in the game being simulated (cf. [Patrizi et al., 2013]). Finally, the turn-taking of player moves mandated by the semantics of the specification (Moore vs. Mealy) is forced by ## Components of the Safe2FOND compilation: ``` F B fturn(vi)g0�i�jX[Yj [ fsync; goalg [ fposs(t)gt2T [ foldCnt(q; m); newCnt(q; m)gq2Q;0�m�k I B fsync; oldCnt(q0; 0)g [ fsafe(t)gt2Safe(T ) [ fposs(t)gt:orig=q0 Safe(T) B f(q; �; q 0 ) 2 T j q 0 < �g O B fmoveX(v)gv2X [ fmovePosY(v); moveNegY(v)gv2Y [ ftransAcc(t; m); transRej(t; m)gt2T;0�m�k [ fstartSync; continueg [ fsyncF(q; m)gq2Q;0�m�k G B fgoalg Stage 1: Actions that simulate X and Y moves: PremoveX(vi) =fturn(vi)g E� moveX(vi) = fturn(vi+1); :turn(vi)g [ oneof (e1; e2) PremovePosY(vi) =fturn(vi)g E� movePosY(vi) = fturn(vi+1); :turn(vi)g [ e1 PremoveNegY(vi) =fturn(vi)g E� moveNegY(vi) = fturn(vi+1); :turn(vi)g [ e2 e1 = f:poss(t)gt2T;:vi2Lits(guard(t)) e2 = f:poss(t)gt2T;vi2Lits(guard(t)) Stage2: Actions that simulate transitions, t 2 T, 0 � m � k: PretransRej(t;m) = � turn(vjX[Yj); poss(t); safe(t); oldCnt(q; m) � E� transRej(t;m) = fF(q 0 ); newCnt(q 0 ; m)g [ f:poss(t 0 )gt02macro(t) PretransAcc(t;m) = � turn(vjX[Yj ); poss(t); :safe(t); oldCnt(q; m) � E� transAcc(t;m) = fF(q 0 ); newCnt(q 0 ; m + 1)g [ f:poss(t 0 )gt02macro(t) Stage 3: Actions that synchronize the automaton, q 2 Q, 0 � m � k: PrestartSync = � turn(vjX[Yj) � [ f:poss(t)gt2T E� startSync = � sync; :turn(vjX[Yj ) � f:oldCnt(q; m)gq2Q;0�m�k PresyncF(q;m) = fsync; F(q); newCnt(q; m)g [ f:newCnt(q; n)gm