--- title: "Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks" authors: - "Steven Carr" - "Nils Jansen" - "Ralf Wimmer" - "Alexandru Serban" - "Bernd Becker" - "Ufuk Topcu" doi: "10.24963/ijcai.2019/768" url: "https://ijcai.org/proceedings/2019/768" pdf: "https://ijcai.org/proceedings/2019/0768.pdf" venue: "Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence" year: 2019 pages: "5532-5539" track: "Main track" keywords: - "Planning and Scheduling: POMDPs" - "Planning and Scheduling: Markov Decisions Processes" - "Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis" --- # Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks Steven Carr, Nils Jansen, Ralf Wimmer, Alexandru Serban, Bernd Becker, Ufuk Topcu *Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence*, pages 5532-5539. DOI: [10.24963/ijcai.2019/768](https://doi.org/10.24963/ijcai.2019/768) ## Abstract We study strategy synthesis for partially observable Markov decision processes (POMDPs). The particular problem is to determine strategies that provably adhere to (probabilistic) temporal logic constraints. This problem is computationally intractable and theoretically hard. We propose a novel method that combines techniques from machine learning and formal verification. First, we train a recurrent neural network (RNN) to encode POMDP strategies. The RNN accounts for memory-based decisions without the need to expand the full belief space of a POMDP. Secondly, we restrict the RNN-based strategy to represent a finite-memory strategy and implement it on a specific POMDP. For the resulting finite Markov chain, efficient formal verification techniques provide provable guarantees against temporal logic specifications. If the specification is not satisfied, counterexamples supply diagnostic information. We use this information to improve the strategy by iteratively training the RNN. Numerical experiments show that the proposed method elevates the state of the art in POMDP solving by up to three orders of magnitude in terms of solving times and model sizes. ## Full text ## 1 Introduction Autonomous agents that make decisions under uncertainty and incomplete information can be mathematically represented as partially observable Markov decision processes (POMDPs). In this setting, while an agent makes decisions within an environment, it obtains observations and infers the likelihood of the system being in a certain state, known as the belief state. POMDPs are effective in modeling a number of real-world applications, see for instance [Kaelbling et al., 1998]. Traditional POMDP problems typically seek to compute a strategy that maximizes a cumulative reward over a finite horizon. However, the agent's behavior is often required to obey more complicated specifications. For example, reachability, liveness or, more generally, specifications expressed in temporal logic (e. g. LTL [Pnueli, 1977]) describe tasks that cannot be expressed using reward functions [Littman et al., 2017]. ∗Contact Authors Strategy synthesis for POMDPs is a difficult problem, both from the theoretical and the practical perspective. For infiniteor indefinite-horizon problems, computing an optimal strategy is undecidable [Madani et al., 1999]. Optimal action choices depend on the whole history of observations and actions, and thus require an infinite amount of memory. When restricting the specifications to maximizing accumulated rewards over a finite horizon and also limiting the available memory, computing an optimal strategy is PSPACE-complete [Papadimitriou and Tsitsiklis, 1987]. This problem is, practically, intractable even for small instances [Meuleau et al., 1999]. Moreover, even when strategies are restricted to be memoryless, finding an optimal strategy within this set is still NP-hard [Vlassis et al., 2012]. For more general specifications like LTL properties, synthesis of strategies with limited memory is even harder, namely EXPTIME-complete [Chatterjee et al., 2015]). The intractable nature of finding exact solutions in these problems gave rise to approximate [Hauskrecht, 2000], pointbased [Pineau et al., 2003], or Monte-Carlo-based [Silver and Veness, 2010] methods. However, none of these approaches provides guarantees for temporal logic specifications. [Chatterjee et al., 2015] studies such problems on a theoretical level. The tool PRISM-POMDP [Norman et al., 2017] actually provides guarantees by approximating the belief space into a fully observable belief MDP, but is restricted to small examples. Other techniques, such as those employing an incremental satisfiability modulo theory (SMT) solver over a bounded belief space [Wang et al., 2018] or a simulation over sets of belief models [Haesaert et al., 2018], are also restricted to small examples. Finally, [Junges et al., 2018] constructs finite-state controllers for POMDPs using parameter synthesis for Markov chains [Hahn et al., 2010; Junges et al., 2019] by applying convex optimization techniques [Cubuktepe et al., 2017; 2018]. Their procedure involves constructing a product of the POMDP and an automaton for temporal logic constraints, which can cause a substantial blow-up in the state space. Although strategy synthesis for POMDPs is hard, an available candidate strategy resolves the nondeterminism and partial observability for a POMDP and yields a so-called induced discrete-time Markov chain (MC). For this simpler model, verification methods are capable of efficiently certifying temporal logic constraints and reward specifications for billions of states [Baier and Katoen, 2008]. Tool support is available via probabilistic model checkers such as PRISM [Kwiatkowska et al., 2011] or Storm [Dehnert et al., 2017]. There remains a dichotomy between directly synthesizing an optimal strategy and the efficient verification of a candidate strategy. The key questions are (1) how to generate a "good" strategy in the first place and (2) how to improve a strategy if verification refutes the specification. Machine learning and formal verification techniques address these questions separately. In this paper, we combine methods from both fields in order to guarantee that a candidate strategy learned through machine learning provably satisfies temporal logic specifications. At first, we learn a randomized strategy* via recurrent neural networks (RNNs) [Hochreiter and Schmidhuber, 1997] and data stemming from knowledge of the underlying structure of POMDPs. We refer to the resulting trained RNN as the strategy network. RNNs are a good candidate for learning a strategy because they can successfully represent temporal dynamic behavior [Pascanu et al., 2013]. Secondly, we extract a concrete (memoryless randomized) candidate strategy from the RNN and use it directly on a given POMDP, resulting in the MC induced by the POMDP and the strategy. Formal verification reveals whether specifications are satisfied or not. In the latter case, we generate a so-called counterexample [Wimmer et al., 2014], which points to parts of the MC (and by extension of the POMDP) that are critical for the specification. For those critical parts, we use a linear programming (LP) approach that locally improves strategy choices (without any guarantees on the global behavior). From the improved strategy, we generate new data to retrain the RNN. We iterate that procedure until the strategy network yields satisfactory results. While the strategies are memoryless, allowing for randomization over possible choices - relaxing determinism - is often sufficient to capture necessary variability in decision-making. The intuition is that deterministic choices at a certain state may need to vary depending on previous decisions, thereby trading off memory. However, randomization in combination with finite memory may supersede infinite memory for many cases [Amato et al., 2010; Junges et al., 2018]. We encode finite memory directly into a POMDP by extending its state space. We can then directly apply our method to create finite-state controllers (FSCs) [Meuleau et al., 1999]. As previously discussed, the investigated problem is undecidable for POMDPs [Madani et al., 1999] and therefore the approach is naturally incomplete. Soundness is provided, as verification yields hard guarantees on the quality of a strategy. ## Related Work Besides the publications mentioned earlier, we list several results employing RNN architectures for POMDPs, all of them within the policy gradient class of algorithms specific to reinforcement learning [Sutton et al., 2000]. In this setting, the strategy is parameterized and updated by performing gradient ascent on the error function (typically chosen to maximize the discounted reward). *Also referred to as stochastic strategy or policy. In order to cope with arbitrary memory in POMDPs, policy gradient methods need some notion of memory. RNNs are suitable for this task because (1) they are differentiable endto-end and (2) they are designed to exhibit dynamic temporal behavior. [Wierstra et al., 2007] were the first to employ an RNN to learn (finite-memory) strategies for POMDPs, using an long short-term memory (LSTM) architecture which is able to leverage both long and short term events in the past. Recent progress in deep learning enabled scaling neural networks (NNs) to solve complex problems. For example, [Mnih et al., 2015] developed an NN - based Q-learning algorithm able to play video games straight from video frames, under partial observability. Instead of using RNNs, the memory problem is solved by replaying a series of frames at every step. Later, [Hausknecht and Stone, 2015] added an LSTM cell to enhance the algorithm's capacity with both long and short term memory. The field has rapidly moved to explore new ways of improving the memory representation [Parisotto and Salakhutdinov, 2018] [Pritzel et al., 2017] [Santoro et al., 2018]. However, even though they yield good performance on a variety of tasks, these methods do not provide any guarantees on the strategies learned. ## 2 Preliminaries A probability distribution over a finite or countably infinite set X is a function m : X → [0, 1] ⊆ R with �x∈X m(x) = m(X) = 1. The set of all distributions on X is Distr(X). The support of a distribution m is supp(m) = {x ∈ X | m(x) > 0}. (PO)MDPs. AMarkov decision process (MDP) M is a tuple M = (S,Act,P) with a finite (or countably infinite) set S of states, a finite set Act of actions, and a transition function P: S×Act →Distr(S). We use a reward function r : S×a→ R. A finite path p of an MDP M is a sequence of states and actions; last(p) is the last state of p. The set of finite paths of M is Paths M fin. A discrete-time Markov chain (MC) is an MDP with |Act(s)| = 1 for all s ∈ S. A strategy g for an MDP M is a function g : Paths M fin → Distr(Act) with supp(g(p)) ⊆ Act(last(p)) for all p ∈ Paths M fin. A strategy g is memoryless if last(p) = last(p ′ ) implies g(p) = g(p ′ ) for all p, p ′ ∈ Paths M fin. Definition 1 (InducedMarkov Chain) For an MDP M = (S,Act,P) and a strategy g ∈ G M , the MC induced by M and g is given by M g = (Paths M fin, P g ) where: Definition 2 (POMDP) A partially observable Markov decision process (POMDP) is a tuple M = (M,Z,O), with M = (S,Act,P) the underlying MDP of M, Z a finite set of observations and O: S→Z the observation function. The set of all finite observation-action sequences for a POMDP M is denoted by ObsSeq M fin . Definition 3 (POMDP Strategy) An observation-based strategy for a POMDP M is a function g : ObsSeq M fin → Distr(Act) such that supp(g(O(p))) ⊆ Act(last(p)) for all p ∈ Paths M fin. G M z is the set of observation-based strategies for M . A memoryless observation-based strategy g ∈ G M z is analogous to a memoryless MDP strategy, formally we simplify to g : Z →Distr(Act), i. e., we decide based on the current observation only. Similarly, a POMDP together with a strategy yields an induced MC as in Def. 1, resolving all nondeterminism and partial observability. A general POMDP strategy can be represented by infinite-state controllers. Strategies are often restricted to finite memory; this amounts to using finite-state controllers (FSCs) [Meuleau et al., 1999]. Definition 4 (FSC) A k-FSC for a POMDP is a tuple A = (N,nI,ga,d) where N is a finite set of k memory nodes, nI ∈ N is the initial memory node, g is the action mapping ga : N×Z →Distr(Act) and d is the memory update d : N×Z×Act →N. Let gA ∈ G M z denote the observationbased strategy represented by the FSC A . The product M ×A of a POMDP and a k-FSC yields a (larger) "flat" POMDP where the memory update is directly encoded into the state space [Junges et al., 2018]. The action mapping ga is left out of the product. Amemoryless strategy g ∈ G M×A z then determines the action mapping and can be projected to the finite-memory strategy gA ∈ G M z . ## Specifications We consider linear-time temporal logic (LTL) properties [Pnueli, 1977]. For a set of atomic propositions AP, which are either satisfied or violated by a state, and a ∈ AP, the set of LTL formulas is given by: Intuitively, a path p satisfies the proposition a if its first state does; (y1 ∧y2) is satisfied, if p satisfies both y1 and y2; ¬y is true on p if y is not satisfied. The formula ©y holds on p if the subpath starting at the second state of p satisfies y. The path p satisfies □y if all suffixes of p satisfy y. Finally, p satisfies (y1Uy2) if there is a suffix of p that satisfies y2 and all longer suffixes satisfy y1. ♦y abbreviates (trueUy). For POMDPs, one wants to synthesize a strategy such that the probability of satisfying an LTL-property respects a given bound, denoted j = P∼l (y) for ∼ ∈ {<,≤,≥,>} and l ∈ [0,1]. In addition, undiscounted expected reward properties j =E∼l (♦a) require that the expected accumulated cost until reaching a state satisfying a respects l ∈ R≥0. If j (either LTL or expected reward specification) is satisfied in a (PO)MDPM under g, we writeM g |=j, that is, the specification is satisfied in the induced MC, see Def. 1. While determining an appropriate strategy is still efficient for MDPs, this problem is in general undecidable for POMDPs [Chatterjee et al., 2016]. In particular, for MDPs, to check the satisfaction of a general LTL specification one needs memory. Typically, tools like PRISM [Kwiatkowska et al., 2011] compute the product of the MDP and a deterministic Rabin automaton. In this product, reachability of so-called accepting end-components ensures the satisfaction of the LTL property. This reachability probability can be determined in polynomial time. PRISM-POMDP [Norman et al., 2017] handles the problem similarly for POMDPs, but note that a strategy needs memory not only for the LTL specification but also for observation dependencies. Finally, given a (candidate) strategy g, checking whether M g |= j holds can be done both for MDPs and POMDPs in polynomial time. For more details we refer to [Baier and Katoen, 2008]. ## 3 Synthesis Procedure Formal problem statement. For a POMDP M and a specification j, where either j = P∼l (y) with y an LTL formula, or j = E∼l (♦a), the problem is to determine a (finite-memory) strategy g ∈ G M z such that M g |=j. If such a strategy does not exist, the problem is infeasible. ## Outline The workflow of the proposed approach is illustrated in Fig. 1: We train an RNN using observation-action sequences generated from an initial strategy as discussed in Sect. 3.1. The trained strategy network represents an observation-based strategy, taking as input an observation-action sequence and returning a distribution over actions, see Def 3. For a POMDP M, we use the output of the strategy network in order to resolve nondeterminism. The strategy network is thereby used to extract a memoryless strategy g ∈ G M and as a result we obtain the induced MCM g . Model checking of this induced MC evaluates whether the specification j is satisfied or not for the extracted strategy. In the former case, the synthesis procedure is finished. The extraction and evaluation is explained in Sect. 3.2. If the specification is not satisfied, we obtain a counterexample highlighting critical states of the POMDP. We employ a linear programming (LP) approach that locally improves action choices of the current strategy at these critical states, see Sect. 3.3. Afterwards, we retrain the RNN by generating new observation-action sequences obtained from the new strategy. We iterate this procedure until the specification is satisfied or a fixed iteration threshold is reached. For cases where we need to further improve, we use domain knowledge to create a specific memory-update function of a k-FSC A , see Def. 4. Then, we compute the product M ′ =M ×A . We iterate our method with M ′ as starting point and thereby determine a concrete k-FSC including the action mapping. Figure 1: Flowchart of the RNN-based refinement loop ![Image](https://ijcai.org/proceedings/2019/fulltext/768/image_000000_de2a7b4be173da95c2837cda65671142e9cc0da9befd17348bc6ee790b45ff9f.png) ## 3.1 Learning Strategies with RNNs As mentioned in Section 1, policy gradient algorithms are used to map observations to actions and are not well suited for POMDPs due to their inability to cope with arbitrary memory. To overcome this weakness, we design our method to make explicit use of memory using RNNs - a family of neural networks designed to exhibit dynamic temporal behavior. Constructing the strategy network. We use the long shortterm memory (LSTM) architecture [Hochreiter and Schmidhuber, 1997] in a similar fashion to policy gradient methods and model the output as a probability distribution on the action space (described formally by ˆ g : ObsSeq M fin →Distr(Act)). By having stochastic output units, we avoid computing gradients on the internal belief states, see [Meuleau et al., 1999] for a similar approach. Using back propagation through time, we can update the strategy during training. Thus, for a given observation-action sequence from ObsSeq M fin , the model learns a strategy ˆ g ∈ G M z . The output is a discrete probability distribution over the actions Act, represented using a final softmax layer. RNN training. We train the RNN using a slightly modified version of sampling re-usable trajectories [Kearns et al., 2000]. In particular, for a POMDP M = (M, Z,O) and a specification j, instead of randomly generating observation sequences, we first compute a strategy g ∈ G M of the underlying MDP M that satisfies j. Then we sample uniformly over all states of the MDP and generate finite paths (of a fixed maximal length) fromPaths M g fin of the inducedMCM g , thereby creating multiple trajectory trees. For each finite path p ∈ Paths M g fin , we generate one possible observation-action sequence pz ∈ ObsSeq M fin such that p = z0, a0, . . . , an-1, zn with zi = O(p[i]), where p[i] denotes the i-th state of p for all 1 ≤ i ≤ n. We form the training set D from a (problem specific) number of m observation-action sequences with observations as input and actions as output labels. Both input and output sets were processed using one-hot-encoding. To fit the RNN model, we use the Adam optimizer [Kingma and Ba, 2014] with a cross-entropy error function. Sampling large environments. In a POMDP M with a large state space (|S| > 10 5 ), computing the underlying MDP strategy g ∈ G M affects the performance of the procedure. In such cases, we restrict the sampling to a smaller environment that shares the observation Z and action spaces Act with M. For example, consider a gridworld scenario with a moving obstacle that has the same underlying probabilistic movement for different problem sizes; such a framework can provide a similar dataset regardless of the size of the grid. ## 3.2 Strategy Extraction and Evaluation We first describe how to extract a memoryless strategy from the strategy network for a specific POMDP, then we formalize the extension to FSCs to account for finite memory. Afterwards, we shortly explain how to evaluate the resulting strategies. Given a POMDP M, we use the trained strategy network ˆ g : ObsSeq M fin → Distr(Act) directly as observationbased strategy. Note that the RNN is inherently a predictor for the distribution over actions and will not always deliver the same output for one input. While we always use the first prediction we obtain, one may also sample several predictions and take the average of the output distributions. ## Extension to FSCs As mentioned before, LTL specifications as well as observation-dependencies in POMDPs require memory. Consider therefore a general FSC A = (N,nI,g,d) as in Def. 4. We first predefine the memory update function d in a problemspecific way, for instance, d changes the memory node when an observation is repeated. Consider observation sequence pz ∈ ObsSeq M fin with pz = z0,a0, . . . ,zn. Assume, the FSC is in memory node nk ∈ N at position i of pz. We define d(nk,zi,ai) = nk+1, if pz[i] = (zi,ai), and there exists a j < i such that pz[ j] = (z j , a j) with zi = z j . Similarly, we account for specific memory choices akin to the relevant LTL specification. Once d has been defined, we compute a product POMDP M ×A which creates a state space over S ×N. The training process is similar to the method outlined above but instead of generating observation-action sequences from ObsSeq M fin , we generate observation-node-action sequences (z0, n0), a0, . . . , an-1, (zn, nn) from ObsSeq M×A fin . In this case, the RNN is learning the mapping of observation and memory node to the distribution over actions as an FSC strategy network: ˆ g FSC : ObsSeq M×A fin ×N→Distr(Act) In order to extract the memoryless FSC A from the FSC strategy network ˆ gFSC, we collect the predicted distributions across the product set of all possible observations z ∈ Z and all possible memory nodes n ∈ N. From this prediction, the FSC A is constructed from the action mapping g(z,n) = ˆ gFSC(z, n) and the predefined memory update function d . Evaluation. We assume that for POMDP M = (M,Z,O) and specification j, we have a finite-memory observationbased strategy g ∈ G M as described above. We use the strategy g to resolve all nondeterminism inM, resulting in the induced MCM g , see Def. 1. For this MC, we apply model checking, which in polynomial time reveals whether M g |=j. For the fixed strategy g we extracted from the strategy network, this provides hard guarantees about the quality of g regarding j. As mentioned before, this strategy is only a prediction obtained from the RNN - so the guarantees necessarily do not directly carry over to the strategy network. ## 3.3 Improving the Represented Strategy We describe how we compute a local improvement for a strategy that does not satisfy the specification. In particular, we have POMDP M = (M,Z,O), specification j, and the strategy g ∈ G M with M g ̸|= j. We now create diagnostic information on why the specification is not satisfied. First, without loss of generality, we assume j = P≤l (y). Let g(z)(a) denote the probability of choosing action a ∈ Act upon observation z ∈ Z, under the strategy g. Let Pr∗ (s) denote the probability to satisfy y within the induced MC M g . For some threshold l ′ ∈ [0,1], a state s ∈ S is critical iff Pr∗ (s) > l ′ . We define l ′ as a function l ′ : S×l →Rwith respect to the threshold l from the original specification and the state s. We define the set of critical decision under the strategy g. Definition 5 (Critical Decision) A probability g(z)(a) > 0 according to an observation-based strategy g ∈ G is a critical decision iff there exist states s,s′ ∈ S with s ∈ O-1 (z), P(s,a,s′ ) >0, and s′ is critical. Intuitively, a decision is critical if it may lead to a critical state. The set of critical decisions serves as a counterexample, generated by the set of critical states and the strategy g. Note that even if a specification is satisfied for g, the sets of critical decisions and states may still be non-empty as they depend on the definition of the criticality-threshold l ′ . For each observation z ∈ O with a critical decision, we construct an optimization problem that minimizes the number of different (critical) actions the strategy chooses per observation class. In particular, the probabilities of action choices under g are redistributed such that the critical choices are minimized. subject to Basically, we maximize over the minimal possible worst case probability for critical states, using the original probability p∗ . From the resulting improved strategy, we generate a new set of paths starting from the critical states. After converting these new paths into observation-action sequences, we retrain the RNN. By gathering more data from these apparently critical situations, we locally improve the quality of the strategies at those locations and gradually introduce observation-dependencies. ## 3.4 Correctness and Termination Correctness of our approach is ensured by evaluating the extracted strategy on the POMDP using model checking. As the investigated problem is undecidable for POMDPs [Madani et al., 1999], our approach is naturally incomplete. In order to enforce termination after finite time, we abort the refinement loop after a specified number of iterations, or as soon as the progress from one iteration to the next (in terms of the model checking results) falls below a user-specified threshold. ## 4 Experimental Results We evaluate our RNN-based synthesis procedure on benchmark examples that are subject to either LTL specifications or expected cost specifications. For the former, we compare to the tool PRISM-POMDP, and for the latter we compare to PRISMPOMDP and the point-based solver SolvePOMDP [Walraven and Spaan, 2017]. Recall that, in general, a strategy over the continuous belief space induces an infinite memory strategy for POMDPs. PRISM-POMDP employs a discretization (we chose the default level of discretization) of that belief space which technically induces a finite-memory strategy. Therefore solutions from PRISM-POMDP are approximate; the tool computes an upper and lower bound on the optimum. We selected the two solvers from different research communities because they provide the possibility for a straightforward adaption to our benchmark setting. In particular, the tools support undiscounted rewards and have a simple and similar input interface. Extended experiments with, for instance, MonteCarlo-based methods [Silver and Veness, 2010] are interesting but beyond the scope of this paper. For a fair comparison, instead of terminating our synthesis procedure once a specification is satisfied, we always iterate 10 times, where one iteration encompasses the (re-)training of the RNN, the strategy extraction, the evaluations, and the strategy improvement as detailed in Sect. 3. For instance, for a specification j = P≤l (y), we leave the l open and seek to compute Pmin(y), that is, we compute the minimal probability of satisfying y to obtain a strategy that satisfies j. We cannot guarantee to reach that optimum, but we rather improve as far as possible within the predefined 10 iterations. The notions are similar for P≥l and Pmax as well as for expected cost measures E≤l (E≥l ) and Emin (Emax). We will now shortly describe our experimental setup and present detailed results for both types of examples. Implementation and setup. We employ the following Python toolchain to realize the full RNN-based synthesis procedure. First, we use the deep learning library Keras [Chollet and others, 2015] to train the strategy network. To evaluate strategies, we employ the probabilistic model checkers PRISM (LTL) and STORM (undiscounted expected rewards).We evaluated on a 2.3 GHz machine with a 12 GB memory limit and a specified maximum computation time of 10 5 seconds. ## 4.1 Temporal Logic Examples We examined three problem settings involving motion planning with LTL specifications. For each of the settings, we use a standard gridworld formulation of an agent with 4 action choices (cardinal directions of movement), see Fig. 2(a). Inside this environment there are a set of static ( ˆ x) and moving ( ˜ x) obstacles as well as possible target cells A and B. Each agent has a limited visibility region, indicated by the green area, and can infer its state from observations and knowledge of the environment. We define observations as Boolean functions that take as input the positions of the agent and moving obstacles. Intuitively, the functions describe the 8 possible relative positions of the obstacles with respect to the agent inside its viewing range. | Problem | |S| | |Act| | |Z| | |-----------------|-----------------|-------------------|-----------------| | Navigation (c) | c 4 | 4 | 256 | | Delivery (c) | c 2 | 4 | 256 | | Slippery (c) | c 2 | 4 | 256 | | Maze(c) | 3c+8 | 4 | 7 | | Grid(c) | c 2 | 4 | 2 | | RockSample[4,4] | 257 | 9 | 2 | | RockSample[5,5] | 801 | 10 | 2 | | RockSample[7,8] | 12545 (b) | 13 | 2 | Figure 2: (a) Example environment and (b) Benchmark metrics ![Image](https://ijcai.org/proceedings/2019/fulltext/768/image_000001_273e485e852eda4757389f7a940782669403f789a3fa8f43efcea3a1c833ef1f.png) 1. Navigation with moving obstacles - an agent and a single stochastically moving obstacle. The agent task is to maximize the probability to navigate to a goal state A while not colliding with obstacles (both static and moving): j1 = Pmax (¬X U A) with x = ˆ x∪ ˜ x, 2. Delivery without obstacles - an agent and static objects (landmarks). The task is to deliver an object from A to B in as few steps as possible: j2 = Emin(♦(A∧♦B)). 3. Slippery delivery with static obstacles - an agent where the probability of moving perpendicular to the desired direction is 0.1 in each orientation. The task is to maximize the probability to go back and forth from locations A and B without colliding with the static obstacles ˆ x: j3 = Pmax (□♦A∧□♦B∧¬♦X), with x = ˆ x, ## Evaluation Fig. 3 compares the size of counterexample in relation to the probability of satisfying an LTL formula in each iteration of the synthesis procedure. In particular, we depict the size of the set S′ ⊂ S of critical states regarding j1 = Pmax (¬X U A) for the Navigation example with grid-size 6. Note that even if the probability to satisfy the LTL specification is nearly one (for the initial state of the POMDP), there may still be critical intermediate states. As can be seen in the figure, while the probability to satisfy the LTL formula increases, the size of the counterexample decreases. In particular, the local improvement (Eq. 1, Sect. 3.3) is demonstrated to be effective. ![Image](https://ijcai.org/proceedings/2019/fulltext/768/image_000002_09e07952984a3bfae5ad3e768151ea55ac6f03dfb22cfdc3717efbea69d6dfdd.png) Iteration no. Figure 3: Progression of the number of critical states and the probability of satisfying an LTL specification as a result of local improvement steps. | Problem | States | Type, j | RNN-based Res. | Synthesis Time (s) | PRISM-POMDP - Res. | PRISM-POMDP - Time (s) | |-------------------------|----------|-------------|------------------|----------------------|----------------------|--------------------------| | Navigation (3) | 333 | PM max, j1 | 0.74 | 14.16 | 0.84 | 73.88 | | Navigation (4) | 1088 | PM max, j1 | 0.82 | 22.67 | 0.93 † | 1034.64 | | Navigation (4) [2-FSC] | 13373 | PM max, j1 | 0.91 | 47.26 | - | - | | Navigation (4) [4-FSC] | 26741 | PM max, j1 | 0.92 | 59.42 | - | - | | Navigation (4) [8-FSC] | 53477 | PM max, j1 | 0.92 | 85.26 | - | - | | Navigation (5) | 2725 | PM max, j1 | 0.91 | 34.34 | MO | MO | | Navigation (5) [2-FSC] | 33357 | PM max, j1 | 0.92 | 115.16 | - | - | | Navigation (5) [4-FSC] | 66709 | PM max, j1 | 0.92 | 159.61 | - | - | | Navigation (5) [8-FSC] | 133413 | PM max, j1 | 0.92 | 250.91 | - | - | | Navigation (10) | 49060 | PM max, j1 | 0.79 | 822.87 | MO | MO | | Navigation (10) [2-FSC] | 475053 | PM max, j1 | 0.83 | 1185.41 | - | - | | Navigation (10) [4-FSC] | 950101 | PM max, j1 | 0.85 | 1488.77 | - | - | | Navigation (10) [8-FSC] | 1900197 | PM max, j1 | 0.81 | 1805.22 | - | - | | Navigation (15) | 251965 | PM max, j1 | 0.91 | 1271.80* | MO | MO | | Navigation (20) | 798040 | PM max, j1 | 0.96 | 4712.25* | MO | MO | | Navigation (30) | 4045840 | PM max, j1 | 0.95 | 25191.05* | MO | MO | | Navigation (40) | - | PM max, j1 | TO | TO | MO | MO | | Delivery (4) [2-FSC] | 80 | EM min , j2 | 6.02 | 35.35 | 6.0 | 28.53 | | Delivery (5) [2-FSC] | 125 | EM min , j2 | 8.11 | 78.32 | 8.0 | 102.41 | | Delivery (10) [2-FSC] | 500 | EM min , j2 | 18.13 | 120.34 | MO | MO | | Slippery (4) [2-FSC] | 460 | PM max, j3 | 0.78 | 67.51 | 0.90 | 5.10 | | Slippery (5) [2-FSC] | 730 | PM max, j3 | 0.89 | 84.32 | 0.93 | 83.24 | | Slippery (10) [2-FSC] | 2980 | PM max, j3 | 0.98 | 119.14 | MO | MO | | Slippery (20) [2-FSC] | 11980 | PM max, j3 | 0.99 | 1580.42 | MO | MO | Table 1: Synthesizing strategies for examples with LTL specs. Table 1 contains the results for the above LTL examples. Note that the sizes of the FSCs were included to demonstrate the trade-off between computational tractability and expressivity: a larger FSC means that the strategy can store more information, which may lead to better choices. However, larger FSCs require more computational effort and may require more data for training the RNN. We convey this trade-off in the experiments, as the size of the FSC is often problem-specific. Naturally the strategies produced by the procedure will not have higher maximum probabilities (or lower minimum expected cost) than those generated by the PRISM-POMDP tool. However, they scale for significantly larger environments and settings. In the larger environments (Navigation(15) and upwards indicated by a star) we employ the sampling technique outlined at the end of Sect. 3.1 on a dataset with grid-size 10. The strategy still scales to these larger environments even when trained on data from a smaller state space. Also in Table 1, we compare the effect of increasing the value of k for several k-FSCs. In smaller instances with gridsizes of 4 and 5, memory-based strategies significantly outperform memoryless ones in terms of quality (the resulting probability or expected cost) while not consuming significantly more time. The increase in performance is due to additional expressiveness of an FSC-based strategy in these environments with a higher density of obstacles. Summarized, our method scales to significantly larger domains than PRISM-POMDP with competitive computation times. As mentioned before, there is an inherent level of randomness in extracting a strategy. While we always take the first shot result for our experiments, the quality of strategies may improved by sampling several RNN predictions. † †Output was a bound; we give the worst-case value from bound. Table 2: Comparison for standard POMDP examples. | Problem | Type | RNN-based Synthesis - States | RNN-based Synthesis - Res | RNN-based Synthesis - Time (s) | PRISM-POMDP - Res | PRISM-POMDP - Time (s) | pomdpSolve - Res | pomdpSolve - Time (s) | |-----------------|--------|--------------------------------|-----------------------------|----------------------------------|---------------------|--------------------------|--------------------|-------------------------| | Maze (1) | EM min | 68 | 4.31 | 31.70 | 4.30 | 0.09 | 4.30 | 0.30 | | Maze (2) | EM min | 83 | 5.31 | 46.65 | 5.23 | 2.176 | 5.23 | 0.67 | | Maze (3) | EM min | 98 | 8.10 | 58.75 | 7.13 | 38.82 | 7.13 | 2.39 | | Maze (4) | EM min | 113 | 11.53 | 58.09 | 8.58 | 543.06 | 8.58 | 7.15 | | Maze (5) | EM min | 128 | 14.40 | 68.09 | 13.00 † | 4110.50 | 12.04 | 132.12 | | Maze (6) | EM min | 143 | 22.34 | 71.89 | MO | MO | 18.52 | 1546.02 | | Maze (10) | EM min | 203 | 100.21 | 158.33 | MO | MO | MO | MO | | Grid (3) | EM min | 165 | 2.90 | 38.94 | 2.88 | 2.332 | 2.88 | 0.07 | | Grid (4) | EM min | 381 | 4.32 | 79.99 | 4.13 | 1032.53 | 4.13 | 0.77 | | Grid (5) | EM min | 727 | 6.62 | 91.42 | MO | MO | 5.42 | 1.94 | | Grid (10) | EM min | 5457 | 13.63 | 268.40 | MO | MO | MO | MO | | RockSample[4,4] | EM max | 2432 | 17.71 | 35.35 | N/A | N/A | 18.04 | 0.43 | | RockSample[5,5] | EM max | 8320 | 18.40 | 43.74 | N/A | N/A | 19.23 | 621.28 | | RockSample[7,8] | EM max | 166656 | 20.32 | 860.53 | N/A | N/A | 21.64 † | 20458.41 | ## 4.2 Comparison to Existing POMDP Examples For comparison to existing benchmarks, we extend two examples from PRISM-POMDP for an arbitrary-sized structure: Maze(c) with c+2 rows and Grid(c) - a square grid with length c. We also compare to RockSample [Silver and Veness, 2010] (see Table 2(b) for problem metrics). These problems are quite different to the LTL examples, in particular the significantly smaller observation spaces. As a result, a simple memoryless strategy is insufficient for a useful comparison. For each problem, the size of the k-FSC used is given by: Maze(c) has k = (c+1); Grid(c) has k = (c-1) and RockSample with b rocks has k = b. Our method compares favorably with PRISM-POMDP and pomdpSolve for Maze and Grid (Table 2). However, the proposed method performs poorly in comparison to pomdpSolve for RockSample: An observation is received after taking an action to check a particular rock. This action is never sampled in the modified trajectory-tree based sampling method (Sect. 3.1). Note that our main aim is to enable the efficient synthesis of strategies under linear temporal logic constraints. ## 5 Summary and FutureWork We introduced a new RNN-based strategy synthesis method for POMDPs and LTL specifications. While we cannot guarantee optimality, our approach shows results that are often close to the actual optimum with competitive computation times for large problem domains. For the future, we are interested in extending our method to continuous state spaces together with abstraction techniques that would enable to employ our model-based method. ## Acknowledgements This work was partially supported by the grants DARPA D19AP00004 and ONR N00014-18-1-2829. ## References 1. [Amato et al., 2010] Christopher Amato, Daniel S Bernstein, and Shlomo Zilberstein. Optimizing fixed-size stochas- tic controllers for POMDPs and decentralized POMDPs. AAMAS, 21(3):293-320, 2010. 2. [Baier and Katoen, 2008] Christel Baier and Joost-Pieter Ka- toen. Principles of Model Checking. MIT Press, 2008. 3. [Chatterjee et al., 2015] Krishnendu Chatterjee, Martin Chmelík, Raghav Gupta, and Ayush Kanodia. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. In ICRA, pages 325-330, 2015. 4. [Chatterjee et al., 2016] Krishnendu Chatterjee, Martin Chmelík, and Mathieu Tracol. What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences, 82(5):878-911, 2016. 5. [Chollet and others, 2015] Franc ¸ois Chollet et al. Keras. https://github.com/fchollet/keras, 2015. Accessed on 02.13.19. 6. [Cubuktepe et al., 2017] Murat Cubuktepe, Nils Jansen, Se- bastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, and Ufuk Topcu. Sequential convex program- ming for the efficient verification of parametric MDPs. In TACAS (2), volume 10206 of LNCS, pages 133-150, 2017. 7. [Cubuktepe et al., 2018] Murat Cubuktepe, Nils Jansen, Se- bastian Junges, Joost-Pieter Katoen, and Ufuk Topcu. Syn- thesis in pmdps: A tale of 1001 parameters. In ATVA, vol- ume 11138 of Lecture Notes in Computer Science, pages 160-176. Springer, 2018. 8. [Dehnert et al., 2017] Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker. In CAV (2), volume 10427 of LNCS, pages 592-600. Springer, 2017. 9. [Haesaert et al., 2018] Sofie Haesaert, Petter Nilsson, Cris- tian Ioan Vasile, Rohan Thakker, Ali-akbar Agha- mohammadi, Aaron D. Ames, and Richard M. Murray. Temporal logic control of POMDPs via label-based stochas- tic simulation relations. In ADHS, volume 51(16) of IFAC- PapersOnLine, pages 271-276. Elsevier, 2018. 10. [Hahn et al., 2010] Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric Markov models. Software Tools for Technology Transfer, 13(1):3-19, 2010. 11. [Hausknecht and Stone, 2015] Matthew Hausknecht and Pe- ter Stone. Deep recurrent q-learning for partially observable MDPs. CoRR, abs/1507.06527, 7(1), 2015. 12. [Hauskrecht, 2000] Milos Hauskrecht. Value-function ap- proximations for partially observable Markov decision pro- cesses. J. Artif. Intell. Res., 13:33-94, 2000. 13. [Hochreiter and Schmidhuber, 1997] Sepp Hochreiter and Jürgen Schmidhuber. Long short-term memory. Neural Computation, 9(8):1735-1780, 1997. 14. [Junges et al., 2018] Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, and Bernd Becker. Finite-state controllers of POMDPs via parameter synthesis. In UAI, 2018. 15. [Junges et al., 2019] Sebastian Junges, Erika Ábrahám, Chris- tian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quat- mann, and Matthias Volk. Parameter synthesis for markov models. CoRR, abs/1903.07993, 2019. 16. [Kaelbling et al., 1998] Leslie Pack Kaelbling, Michael L. Littman, and Anthony R. Cassandra. Planning and act- ing in partially observable stochastic domains. Artif. Intell., 101(1):99-134, 1998. 17. [Kearns et al., 2000] Michael J Kearns, Yishay Mansour, and Andrew Y Ng. Approximate planning in large POMDPs via reusable trajectories. In NIPS, pages 1001-1007, 2000. 18. [Kingma and Ba, 2014] Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint 1412.6980, 2014. 19. [Kwiatkowska et al., 2011] Marta Kwiatkowska, Gethin Nor- man, and David Parker. PRISM 4.0: Verification of proba- bilistic real-time systems. In CAV, volume 6806 of LNCS, pages 585-591. Springer, 2011. 20. [Littman et al., 2017] Michael L. Littman, Ufuk Topcu, Jie Fu, Charles Isbell, Min Wen, and James MacGlashan. Environment-independent task specifications via GLTL. arXiv preprint 1704.04341, 2017. 21. [Madani et al., 1999] Omid Madani, Steve Hanks, and Anne Condon. On the undecidability of probabilistic planning and infinite-horizon partially observable Markov decision problems. In AAAI, pages 541-548. AAAI Press, 1999. 22. [Meuleau et al., 1999] Nicolas Meuleau, Leonid Peshkin, Kee-Eung Kim, and Leslie Pack Kaelbling. Learning finite- state controllers for partially observable environments. In UAI, pages 427-436. 23. Morgan Kaufmann, 1999. 24. [Mnih et al., 2015] Volodymyr Mnih, Koray Kavukcuoglu, David Silver, et al. Human-level control through deep reinforcement learning. Nature, 518(7540):529, 2015. 25. [Norman et al., 2017] Gethin Norman, David Parker, and Xueyi Zou. Verification and control of partially observable probabilistic systems. Real-Time Systems, 53(3):354-402, 2017. 26. [Papadimitriou and Tsitsiklis, 1987] Christos H. Papadim- itriou and John N. Tsitsiklis. The complexity of Markov decision processes. Mathematics of Operations Research, 12(3):441-450, 1987. 27. [Parisotto and Salakhutdinov, 2018] Emilio Parisotto and Ruslan Salakhutdinov. Neural map: Structured memory for deep reinforcement learning. In ICLR. OpenReview.net, 2018. 28. [Pascanu et al., 2013] Razvan Pascanu, C ¸aglar Gülc ¸ehre, Kyunghyun Cho, and Yoshua Bengio. How to construct deep recurrent neural networks. CoRR, abs/1312.6026, 2013. 29. [Pineau et al., 2003] Joelle Pineau, Geoff Gordon, and Sebas- tian Thrun. Point-based value iteration: An anytime algo- rithm for POMDPs. In IJCAI, pages 1025-1032. 30. Morgan Kaufmann, 2003. 31. [Pnueli, 1977] Amir Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE Computer Society, 1977. 32. [Pritzel et al., 2017] Alexander Pritzel, Benigno Uria, Sri- ram Srinivasan, Adrià Puigdomènech Badia, Oriol Vinyals, Demis Hassabis, Daan Wierstra, and Charles Blundell. Neu- ral episodic control. In ICML, volume 70 of Proc. of Ma- chine Learning Research, pages 2827-2836. PMLR, 2017. 33. [Santoro et al., 2018] Adam Santoro, Ryan Faulkner, David Raposo, Jack W. Rae, Mike Chrzanowski, Theophane We- ber, Daan Wierstra, Oriol Vinyals, Razvan Pascanu, and Timothy P. Lillicrap. Relational recurrent neural networks. In NeurIPS, pages 7310-7321, 2018. 34. [Silver and Veness, 2010] David Silver and Joel Veness. Monte-carlo planning in large POMDPs. In NIPS, pages 2164-2172, 2010. 35. [Sutton et al., 2000] Richard S. Sutton, David A. McAllester, Satinder P. Singh, and Yishay Mansour. Policy gradient methods for reinforcement learning with function approxi- mation. In NIPS, pages 1057-1063, 2000. 36. [Vlassis et al., 2012] Nikos Vlassis, Michael L. Littman, and David Barber. On the computational complexity of stochas- tic controller optimization in POMDPs. ACM Trans. on Computation Theory, 4(4):12:1-12:8, 2012. 37. [Walraven and Spaan, 2017] Erwin Walraven and Matthijs Spaan. Accelerated vector pruning for optimal POMDP solvers. In AAAI, pages 3672-3678. AAAI Press, 2017. 38. [Wang et al., 2018] Yue Wang, Swarat Chaudhuri, and Ly- dia E. Kavraki. Bounded policy synthesis for pomdps with safe-reachability objectives. In AAMAS, pages 238-246. Int'l Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA / ACM, 2018. 39. [Wierstra et al., 2007] Daan Wierstra, Alexander Förster, Jan Peters, and Jürgen Schmidhuber. Solving deep memory POMDPs with recurrent policy gradients. In ICANN, pages 697-706. Springer, 2007. 40. [Wimmer et al., 2014] Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker. Minimal counterexamples for linear-time probabilistic verification. Theoretical Computer Science, 549:61-100, 2014.