LTL Realizability via Safety and Reachability Games

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;

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<n�k E� syncF(q;m) = fposs(t)gt:orig=q [ foldCnt(q; m)g [ f:F(q)g [ � :newCnt(q; n)0�n�k � Action that reestablishes the dynamics of the problem: Precontinue = fsyncg [ f:F(q)gq2Q E� continue = oneof (e3; e4) e3 = fgoalg e4 = fturn(v0); :syncg

establishing a fixed order in the variables v 2 X [ Y. E.g. with the Moore semantics, the order must guarantee that the fluents turn(vi) first iterate over all variables in Y.

Safe2FOND(S) denotes the FOND problem constructed from specification S = hX;Y; (A;UkCW)is, where s 2 � Moore, Mealy � . The construction of Safe2FOND(S) is polynomial, and thus existence of a winning strategy for S can be determined in time that is exponential in the size of A. Recall that FOND planning is EXPTIME-complete in the size of succinct representations of the problem [Rintanen, 2004].

Theorem 7. The construction Safe2FOND(S) is a polynomial reduction of UkCW games S into FOND planning. If � is a strong cyclic solution to Safe2FOND(S) then a winning strategy for S can be constructed from �.

Proof sketch. The proof of correctness for UkCW-based automata compilations follows the intuition explained below. The dynamics of the automaton are captured by planning actions. Each planning state s simulates an automaton macrostate (as in the powerset construction), and has the property that F(q) 2 s i� there exists a run on the automaton in the simulated play that ends in q. In addition, planning states count the maximum number of times automaton runs hit accepting states. Given the properties above, and a fixed k, the UkCW game has a winning strategy i� there exists a policy that (1) only visits planning states with associated counter that is not greater than k, and (2) runs in perpetuity. Property (1) is achieved by forcing planning states with associated counter equal to k to be deadends - and this is actually done in the current compilation. Property (2) is achieved by strong-cyclic solutions, with the trick of introducing the artificial non-deterministic action continue and dummy goals (cf. [Patrizi et al., 2013]). The construction of Safe2FOND(S) is polynomial. A transducer that implements a winning strategy can be constructed by unfolding a strong cyclic solution, collapsing states that belong to the same simulated turn. �

5.2 NkBWGames via Planning

The construction Safe2FOND presented in Section 5.1 can be modified into an algorithm, Reach2FOND, that solves NkBW games via reduction to strong FOND planning. The main modifications follow.

In contrast to safety games, solutions to a reachability game have to yield good prefixes. Recall that the compiled FOND problem has fluents newCnt(q; m) that keep track of whether there exists a run of A on the play being simulated that hits m accepting states. In a NkBW reachability game, a good prefix is achieved when a state in which newCnt(q; k) holds is visited. As such, in Reach2FOND(S) the goal is no longer the dummy fluent goal, but to reach one of the fluents newCnt(q; k) for q 2 Q. The action continue is now deterministic, and its unique e�ect reestablishes the first stage. This time, not all runs of the automaton need to be carried over. To this end, action continue does not require all F(q) to be false, and instead falsifies all of them. Finally, strong solutions to Reach2FOND(S) yield winning strategies for S. The correctness and complexity results obtained in Section 5.1 extend to FOND compilations of NkBW games.

Theorem 8. The construction Reach2FOND(S) is a polynomial reduction of NkBW games S into FOND planning. If � is a strong solution to Reach2FOND(S) then a winning strategy for S can be constructed from �.

Proof sketch. Similar to the proof of correctness of Theorem 7, the dynamics of Reach2FOND(S) simulate plays of the game. This time, the dynamics simulate transitions in a NBW automaton. Planning states can do bookkeeping of some runs of the NBW (not necessarily all), and count the maximum number of times that these runs hit accepting states. In other words, a fixed play can be simulated by carrying over some runs of the NBW, or all, at the discretion of the planner. As such, strong solutions to Reach2FOND(S) yield winning strategies to S. A transducer that implements a winning strategy can be constructed by unfolding a strong solution, collapsing states that belong to the same simulated turn. In the other direction, winning strategies can be simulated with the dynamics of Reach2FOND(S). The construction of Reach2FOND(S) is polynomial. �

6 Multiple Automata Decompositions

Our automata-based approaches to LTL synthesis rely on worst-case exponential transformations of the LTL formula into NBW and UCW automata. In practice, this complexity can be reduced by systematically decomposing LTL formula ' into smaller subformulae and transforming them into multiple automata that together capture the models of '. Such transformations have been exploited in some previous approaches to LTL synthesis (e.g., [Camacho et al., 2017; Bohy et al., 2012; Camacho et al., 2018a]) and in approaches to planning with LTL goals and preferences (e.g. [Baier and McIlraith, 2006]).

In Acacia + , specification ' is systematically decomposed into the conjunction of a set of subformulae 'i, each of which is transformed into a UCW Ai. The resulting game is the composition of potentially smaller safety subgames, each one with associated UkCW Ai, which run in parallel. Winning strategies have to avoid bad prefixes in all of the subgames.

In [Camacho et al., 2018a], we presented a reduction of LTLf synthesis - that is, synthesis of LTL specifications interpreted over finite words - into FOND planning. The construction of a FOND problem is similar to the NkBW-based compilation presented in this paper, with the major exception that the target was non-deterministic finite-state automata (NFA). Automata decompositions take a specification ' in NNF, decompose it into a conjunction of subformulae 'i, and transform each 'i into an NFAAi. The resulting game is the composition of potentially smaller subgames, each one with associated NFA Ai, that run in parallel. The dynamics of all subgames are integrated within a single FOND problem, and the goal is achieved whenever all subgames are winning.

The FOND compilations that we presented in Section 5 are also amenable to automata decompositions. FOND compilations of UkCW games can use multiple automata decompositions following Acacia + , whereas NkBW games can use automata decompositions following Camacho et al. [2018a].

7 Evaluation

We implemented the algorithms for LTL realizability and synthesis via FOND in a tool we named SynKit [Camacho et al., 2018c]. SynKit implements the algorithms presented in this paper, and others (e.g., those in [Camacho et al., 2018a] for finite LTL synthesis). We use Spot to transform LTL formulae into NBW [Duret-Lutz et al., 2016]. Reductions to automata games listed in Table 1 are solved via FOND planning with Safe2FOND and Reach2FOND compilations. We use PRP to generate strong cyclic solutions [Muise et al., 2012], and MyND to generate strong solutions [Mattm¨uller et al., 2010]. Our experiments were run on an Intel Xeon E5-2430 2.2GHz processor, and each process was limited to 30 minute run times and 4GB memory usage. We configured SynKit to perform reductions to UkCW games with k � 2 and NkBW games with k � 3.

Synthesis via Planning One of the main objectives of our experiments was to evaluate whether automated planning is a viable technology to address LTL synthesis. We tested the performance of our planning-based methods over a collection of benchmarks used in the sequential realizability track of the SYNTCOMP 2017 competition. Table 2 summarizes the aggregated coverage results (i.e., number of problems solved) obtained by SynKit. For reference, we include coverage results of participants in SYNTCOMP 2017: Party, ltlsynt, Bosy, Bowser, and Acacia + . These results are reported on the competition website. They were run with an Intel XEON E3-1271 3.6GHz processor, 32GB of memory, and a processing time limit of 60 minutes. Rather than giving a precise comparison of run time, our objective was to evaluate whether planning technology, and the algorithms presented in this paper are competitive with more mature synthesis tools. In terms of run time, we observed that most problems can be solved with low time and memory usage. In terms of coverage, while SynKit does not outperform any of the tools we compared with, it is very competitive and able to determine realizability for several problems that eluded other solvers.

Advantage of NkBW-based Reductions The second objective of our experiments was to assess the advantage of our novel bounded realizability methods over existing bounded synthesis. Table 2 details the coverage results obtained with the tests for determining realizability and unrealizability listed in Table 1. The coverage obtained with reductions to NkBW and UkCW games is very similar. We observed that the run times di�er significantly in some problems, and no method clearly dominates the other. Thus, bounded realizability can be an alternative to bounded synthesis.

8 Summary and Discussion

LTL synthesis is central to the automated construction of controllers and certain classes of programs. While LTL synthesis is a well-established problem, it has only been in the last decade that e�cient tools have started to emerge. Common approaches to LTL synthesis reduce the problem to automata games and many modern tools make use of bounded synthesis techniques based on safety games played over UkCW.

In this paper we established the duality between so-called Mealy and Moore semantics of LTL specifications in the context of LTL synthesis. We exploited this duality to define novel reductions of LTL realizability to reachability games played over NkBW automata. We also introduced the first complete approach to LTL realizability and synthesis via automated planning. Our approach compiles automata games into instances of FOND planning. Preliminary experimental results show that reductions to NkBW games can be beneficial and complement other well-known reductions to UkCW games. Moreover, they show that planning technology can be a competitive technique to approach synthesis.

Acknowledgements

The authors gratefully acknowledge funding from the Natural Sciences and Engineering Research Council of Canada (NSERC) and Fondecyt grant numbers 1150328 and 1161526.