Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints

1 Introduction

Research in the reinforcement and supervised learning communities has demonstrated the utility of recurrent neural networks (RNNs) in synthesizing control policies in domains that exhibit temporal behavior [Tsoi and Back, 1997; Bakker, 2001]. The internal memory states of RNNs, such as in long short-term memory (LSTM) architectures [Hochreiter and Schmidhuber, 1997], effectively account for temporal behavior by capturing the history from sequential information [Pascanu et al., 2014]. Furthermore, in applications that suffer from incomplete information, RNNs leverage history to act as either a state or value estimator [Wierstra et al., 2007] or as a control policy [Hausknecht and Stone, 2015].

In safety-critical systems such as autonomous vehicles, policies that are guaranteed to prevent unsafe behavior are necessary. We seek to provide formal guarantees for policies represented by RNNs with respect to temporal logic [Pnueli, 1977] or reward specifications. Such a verification task is, in general, hard due to the complex, often non-linear, structures of RNNs [Mulder et al., 2015]. Existing work directly employs satisfiability-modulo-theories (SMT) [ et al., 2018] or mixed-integer linear program (MILP) [Akintunde et al., 2019], however, such methods not only scale exponentially in the number of variables but also rely on constructions using only rectified linear units (ReLUs).

We take an iterative and model-based approach, see Fig. 1. We extract a policy from a given RNN in the form of a finitestate controller (FSC) [Poupart and Boutilier, 2003]. First, we employ a modification of a discretization technique called quantized bottleneck insertion, introduced in [Koul et al., 2019]. Basically, the discretization facilitates a mapping of the continuous memory structure of the RNN to a pre-defined number of discrete memory states and transitions of an FSC.

However, this standalone FSC without a formal model is often not sufficient to prove meaningful properties. The proposed approach relies on the exact behavior a policy induces on a specific application that can be modeled formally. We apply the extracted FSC directly to a formal model, and the resulting restricted model is amenable for efficient verification techniques that certify whether a specification is satisfied [Baier and Katoen, 2008].

If the specification does not hold, verification methods typically provide diagnostic information on critical parts of the model in the form of so-called counterexamples. We propose to utilize such counterexamples to identify improvements in the extracted FSC or in the underlying RNN. First, increasing the amount of memory states in the FSC may help to approximate the behavior of the RNN more precisely [Koul et al., 2019]. Second, the RNN may actually require further training data to induce higher-quality policies for the particular application. Existing approaches rely, for example, on loss visualization [Goodfellow and Vinyals, 2015], but we strive to exploit the information we can gain from the concrete behavior of the RNNs with respect to a formal model. Therefore, in order to decide whether more data are needed in the training of the RNN or whether first the number of memory states in the FSC should be increased, we identify those critical decisions of the current FSC that are "arbitrary". Basically, we measure the entropy [Cover and Thomas, 2012] of each stochastic choice over actions according to the current FSC-based policy at critical states. That is, if the entropy is high, the decision is deemed arbitrary despite its criticality and further training is required.

We showcase the applicability of the proposed method on partially observable Markov decision processes (POMDPs). With their ability to represent sequential decision-making problems under uncertainty and incomplete information, these models are of particular interest in planning and control [Cassandra, 1998]. Despite their utility as a modeling formalism and recent algorithmic advances, policy synthesis for POMDPs is hard both theoretically and practically [Meuleau et al., 1999]. For reasons outlined earlier, RNNs have recently emerged as efficient policy representations for POMDPs [Hausknecht and Stone, 2015]. We detail the proposed approach on POMDPs and combine the scalability and flexibility of an RNN representation with the rigor of formal verification to synthesize POMDP policies that adhere to temporal logic specifications.

We demonstrate the effectiveness of the proposed synthesis approach on a set of POMDP benchmarks. These benchmarks allows for a comparison to well-known POMDP solvers, both with and without temporal logic specifications. The numerical examples show that the proposed method (1) is more scalable, by up to 3 orders of magnitude, than wellknown POMDP solvers and (2) achieves higher-quality results in terms of the measure of interest than other synthesis methods that extract FSCs.

Related work. Closest to the proposed method is [Carr et al., 2019], which introduced a verification-guided method to train RNNs as POMDP policies. In contrast to the proposed method, while polices are extracted from the RNNs, these policies do not directly exhibit the memory structure of the RNNs and are instead handcrafted based on knowledge about the particular application.

There are three lines of related research. The first one concerns the formal verification of neural network-based control policies. Two prominent approaches [Huang et al., 2017; Katz et al., 2017] for the class of feed-forward deep neural networks rely on encoding neural networks as SMT problems through adversarial examples or ReLUs architectures respectively. [Akintunde et al., 2019] concerns the direct verification of RNNs with ReLU activation functions using SMT or MILP. However, the scalability of these solver-based methods suffer from the size of the input models. We circumvent this shortcoming by our model-based approach where verification is restricted to concrete applications followed by potential improvement of the RNNs.

The second relevant direction concerns the direct synthesis of FSCs for POMDPs without neural networks. For example, [Meuleau et al., 1999] uses a branch-and-bound method to compute optimal FSCs, and [Junges et al., 2018] constructs an FSC using parameter synthesis for Markov chains.

Third, existing work that concerns the extraction of FSCs from neural networks [Zeng et al., 1993; Weiss et al., 2018; Michalenko et al., 2019], does not integrate with formal verification to provide formal guarantees.

2 Preliminaries

A probability distribution over a set X is a function µ: X → [0, 1] ⊆ R with ∑x∈X µ(x) = µ(X) = 1. The set of all distributions on X is Distr (X). The support of a distribution µ is supp(µ) = {x ∈ X | µ(x) > 0}. The entropy of a distribution µ is H(µ) := - ∑x∈X µ(x) log|X| µ(x).

POMDPs. 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 probability function P : S × Act → Distr(S). The reward function for states and actions is given by r : S × Act → R. A finite path π of an MDP M is a sequence of states and actions; last(π) is the last state of π. The set of all finite paths is PathsMfin .

Definition 1 (POMDP). A POMDP is a tuple M = (M,Z,O), with M the underlying MDP of M, Z a finite set of observations, and O: S → Z the observation function.

For POMDPs, observation-action sequences are based on a finite path π ∈ PathsMfin of M and have the form: O(π) = O(s0) a0 -→ O(s1) a1 -→ · · ·O(sn). The set of all finite observation-action sequences for a POMDP M is ObsSeqMfin .

Definition 2 (POMDP Policy). An observation-based policy for a POMDP M is a function γ : ObsSeqMfin → Distr (Act ) such that supp(γ(O(π))) ⊆ Act (last(π)) for all π ∈ PathsMfin . ΓMz is the set of observation-based policies forM.

A policy for a POMDP resolves the nondeterministic choices in the POMDP, based on the history of previous observations, by assigning distributions over actions. A memoryless observation-based policy γ ∈ ΓMz is given by γ : Z → Distr(Act), i. e., decisions are based on the current observation only. A POMDP M together with a policy γ yields an induced discrete-time Markov chain (MC) Mγ . An MC does not contain any nondeterminism or partial observability. Our definition restricts POMDP policies to finite memory, which are typically represented as FSCs.

Definition 3 (Finite-state controller (FSC)). A k-FSC for a POMDP is a tuple A = (N, nI , α, δ) where N is a finite set of k memory nodes, nI ∈ N is the initial memory node, α is the action mapping α: N × Z → Distr(Act) and δ is the memory update δ : N × Z × Act → N.

An FSC has the observations Z as input and the actions Act as output. Upon an observation, depending on the current memory node the FSC is in, the action mapping α returns a distribution over Act followed by a change of memory nodes according to δ. FSCs are an extension of so-called Moore machines, where the action mapping is deterministic, that is, α : N × Z → Act , and the memory update δ : N × Z → N does not depend on the choice of action.

Definition 4 (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:

Intuitively, a path π satisfies the proposition a if its first state does; (ψ1∧ψ2) is satisfied, if π satisfies both ψ1 and ψ2; ¬ψ is true on π if ψ is not satisfied. The formula ©ψ holds on π if the subpath starting at the second state of π satisfies ψ; π satisfies □ψ if all suffixes of π satisfy ψ. Finally, π satisfies (ψ1 Uψ2) if there is a suffix of π that satisfies ψ2 and all longer suffixes satisfy ψ1. ♦ψ abbreviates (trueUψ).

For POMDPs, one wants to synthesize a policy such that the probability of satisfying an LTL-property respects a given bound, denoted ϕ = P∼λ(ψ) for ∼ ∈ {<, ≤, ≥, >} and λ ∈ [0, 1]. In addition, undiscounted expected reward properties ϕ = E∼λ(♦a) require that the expected accumulated cost until reaching a state satisfying a respects λ ∈ R≥0.

A specification ϕ is satisfied for POMDPMand γ if it is satisfied in the MCMγ (Mγ |= ϕ). We now define a general notion of an RNN that represents a POMDP policy.

Definition 5 (Policy network). A policy network for a POMDP is a function ˆ γ : ObsSeqMfin → Distr (Act ).

The underlying RNN which receives sequential input in the form of (finite) observation sequences from ObsSeqMfin , the output is a distribution over actions, see Fig. 4a. To be more precise, we identify the main components of such a network.

Definition 6 (Components of a policy network). A policy network ˆ γ is sufficiently described by a hidden-state update function ˆ δ : R × Z × Act → R and an action mapping γh : R → Distr (Act ).

Consider the following observation sequence:

The policy network receives an observation and returns an action choice. Throughout the execution of the sequence, the RNN holds a continuous hidden state h ∈ R, occasionally described as an internal memory state, which captures previous information. On each transition, this hidden state is updated to include the information of the current state and the last action taken under the hidden state transition function ˆ δ. From the prior observation sequence in (1), the corresponding hidden state sequence would be defined as:

Additionally, the output of the policy network is expressed by the action-distribution function γh, which maps the value of hidden state to a distribution over the actions. At internal memory states hi, we have ˆ δ(hi,O(si), ai) = hi+1 and γh(hi+1) = µ(Act) for state si on path π. Note that a policy network characterizes a well-defined POMDP policy.

3 Problem Statement

We attempt to solve two separate but related problems: (1) For a POMDP M, a policy network ˆ γ and a specification ϕ, the problem is to extract an FSC Aˆ γ ∈ ΓMz such that MAˆ γ |= ϕ. (2) If the extraction process fails to produce a suitable candidate, then we determine an improved policy network ˆ γ ∗ for which we can solve (1).

3.1 Outline

Fig. 2 illustrates the workflow of the proposed approach for a given POMDP M, policy network ˆ γ and specification ϕ. We summarize the individual steps below and provide the technical details in the subsequent sections.

FSC extraction. We first quantize the memory nodes of the policy network ˆ γ, that is, we discretize the memory update of the continuous memory state h. From this discrete representation of the memory update, we construct an FSC Aˆ γ ∈ ΓMz . The procedure has as input the number Bh of neurons which defines a bound on the number of memory nodes in the FSC.

Verification. We use the FSC Aˆ γ to resolve partial information and nondeterministic choices in the POMDPM, resulting in an induced MC MAˆ γ . We evaluate whether the given specification ϕ is satisfied for this induced MC using a formal verification technique called model checking [Baier and Katoen, 2008]. If the specification ϕ holds, then the synthesis is complete with output policy Aˆ γ. However, if ϕ does not hold, then we decide if we shall increase the bound Bh on the number of memory nodes or if the network needs retraining. In particular, we examine whether or not the entropy over the FSC's action distribution is above a prescribed threshold.

Policy improvement. In the high entropy case, we increase the discretization level, that is, we increase Bh, and construct the FSC Aˆ γ with additional memory states at its disposal. Whereas in the other case, additional memory nodes may cause the extracted FSC to be drawn from extrapolated information and we instead seek to improve the policy network. For that, we use diagnostic information in the form of counterexamples to generate new data [Carr et al., 2019].

Example 1. We consider the POMDP in Fig. 3 as a motivating example for the necessity of memory-based FSCs. The POMDP has three observations ("blue", s3 and s4) where observation "blue" is received upon visiting s0, s1, and s2. That is, the agent is unable to distinguish between these states. The specification is ϕ = Pr≥0.9(♦s3), so the agent is to reach state s3 with at least probability 0.9. In a 1-FSC (i.e. one memory node 0), we can describe an FSC A1 by:

A 2-FSC with two memory nodes (0 and 1), see Fig. 3c, allows for greater expressivity, i.e. the policy can base its decision on larger observation sequences. With this memory structure, we can create an FSC A2 that ensures the satisfaction of ϕ:

4 Policy Extraction

In this section we describe how we adapt the method called quantized bottleneck insertion [Koul et al., 2019] to extract an FSC from a given RNN. Let us first explain the relationship between the main components of a policy network ˆ γ (Definition 6) and an FSC A (Definition 3). In particular, the hidden-state update function ˆ δ : R×Z×Act → R takes as input a real-valued hidden state of the policy network, while the memory update function of an FSC takes a memory node from the finite set N. The key for linking the two is therefore a mechanism that encodes the continuous hidden state h into a set N of discrete memory nodes.

Policy networkmodification. To obtain the above linkage, we leverage an autoencoder [Goodfellow et al., 2016] in the form of a quantized bottleneck network (quantized bottleneck network (QBN)) [Koul et al., 2019]. This QBN, consisting of an encoder and a decoder, is inserted into the policy network directly before the softmax layer, see Fig. 4b. In the encoder, the continuous hidden state value h ∈ R is mapped to an intermediate real-valued vector RBh of pre-allocated size Bh. The decoder then maps this intermediate vector into a discrete vector space defined by {-1, 0, 1}Bh . This process, illustrated in Fig. 4b, provides a mapping of the continuous hidden state h into 3Bh possible discrete values. We denote the discrete state for h by ˆh and the set of all such discrete states by ˆH. Note, that | ˆH| ≤ 3Bh since not all values of the hidden state may be reached in an observation sequence. [Koul et al., 2019] has another QBN for a continuous observation space, however, we focus on discrete observations and can neglect the additional autoencoder.

FSC construction. After the QBN insertion we simulate a series of executions, querying the modified RNN for action choices, on the concrete application, e.g. using a POMDP model. We form a dataset of consecutive pairs (ˆht, ˆht+1) of discrete states, the action at and the observation zt+1 that led to the transition {ˆht, at, zt+1, ˆht+1} at each time t during the execution of the policy network. The number of accessed memory nodes N ⊆ ˆH corresponds to the number of different discrete states ˆh ∈ ˆH in this dataset. The deterministic memory update rule δ(nt, at, zt+1) = nt+1 is obtained by constructing a N × (|Z| × |Act |) transaction table, for a detailed description see [Koul et al., 2019]. We can additionally construct the action mapping α : N × Z → Distr (Act ) with α(nt, zt) = µ ∈ Distr (Act ) by querying the softmax-output layer (see Fig. 4a) for each memory state and observation.

5 Policy Evaluation and Improvement

Evaluation using formal verification. We assume that for POMDP M = (M,Z,O) and specification ϕ, we have an extracted FSC Aˆ γ ∈ ΓMz as inDefinition 3. We use the policy Aˆ γ to obtain the inducedMCMAˆ γ . For this MC, formal verification through model checking checks whether MAˆ γ |= ϕ and thereby provides hard guarantees about the quality of the extracted FSC Aˆ γ regarding ϕ. In particular, (probabilistic) model checking provides the probability (or the expected reward) to satisfy a specification for all states s ∈ S via solving linear equation systems [Baier and Katoen, 2008].

Example 1 (cont.). Consider the case in the 1-FSC A1 (Fig. 3b) where p = 1, the probability of reaching the state s3 in the induced MC is Pr(♦s3) = 13 . Clearly, the behavior induced by this 1-FSC violates the specification and we obtain two counterexamples of critical memory-state pairs for this policy Aˆ γ: (0, s0) and (0, s1).

If the specification does not hold, the policy may require refinement. As discussed before, on the one hand we can increase the upper bound Bh on the number of memory nodes to extract a new FSC. At each iteration of the inner loop in Fig. 2, we modify the QBN for the new, increased, level of discretization and obtain a new FSC using the process outlined in Sect 4. On the other hand, we may decide via a formal entropy check whether new data need to be generated to actually improve the policy.

Improving the policy network. Our goal is to determine whether a policy network requires more training data or not. Existing approaches in supervised learning methods leverage benchmark comparisons between a train-test set using a loss function [Baum and Wilczek, 1987]. Loss visualization, proposed by [Goodfellow and Vinyals, 2015] provides a set of analytical tools to show model convergence. However, such approaches aim at continuous functions instead of the discrete representations we seek. More importantly, we leverage the information gained from a model-based approach.

Counterexamples. We first determine a set of states that are critical for satisfaction of the specification under the current policy. Consider a sequence of memory nodes and observations (n0, z0) a0 -→ · · · at-1 ---→ (nt, zt) from the POMDP M under the FSC Aˆ γ. For each of these sequences, we collect the states s ∈ S underlying the observations, e.g., O(s) = zi for 0 ≤ i ≤ t. As we know the probability or expected reward for these states to satisfy the specification from previous model checking, we can now directly assess their criticality regarding the specification. We collect all pairs of memory nodes and states from N × S that contain critical states and build the set Crit M Aˆγ ⊆ N×S that serves us as a counterexample. These pairs carry the joint information of critical states and memory nodes from the policy applied to the MC and may be formalized using a so-called product construction.

Entropymeasure. The average entropy across the distributions over actions at the choices induced by the counterexample set Crit M Aˆγ is our measure of choice to determine the level of training for the policy network. Specifically, for each pair (n, s) ∈ Crit M Aˆγ , we collect the distribution µ ∈ Distr(Act) over actions that Aˆ γ returns for the observation O(s) when it is in memory node n. Then, we define the evaluation function H using the entropy H(µ) of the distribution µ:

For high values of H, the distribution is uniform across all actions and the associated policy network is likely extrapolating from unseen inputs.

In Fig. 5, we observe that when there are fewer samples and higher discretization, the extracted FSC tends to perform arbitrarily. We lift the function H to the full set Crit M Aˆγ :

We compare the average entropy over all components of the counterexample against a threshold η ∈ [0, 1], that is, if H(Crit M Aˆγ ) > η, we will provide more training data. Vice versa, if H(Crit M Aˆγ ) ≥ η, we will increase the upper bound on the number of memory states in the FSC.

Example 1 (cont.). Under the working example, the policy A1 was the 1-FSC with p = 1 (Fig. 3b), which produces two counterexample memory and state pairs: CritMA1 = {(0, s0), (0, s1)}. The procedure would then examine the policy's average entropy at these critical components (n, s) ∈ CritMA1 , which in this trivial example is given by H(CritMA1 ) = -p log2(p) - (1 - p) log2(1 - p) = 0 from (2). The average entropy is below a prescribed threshold, η = 0.5, and thus we increase the number of memory nodes, which results in the satisfying FSC A2 in Fig. 3c.

Collecting new training data. There are several ways to perform retraining of the policy network. One option is sampling using the QMDP value method [Littman et al., 1995]. Alternatively, one can generate data through bootstrapped random sampling as in [Hausknecht and Stone, 2015]. We follow the approach from [Carr et al., 2019] and start with a policy for the underlying MDP M that satisfies ϕ. This policy is gradually improved using a counterexample-guided technique employing the set CritMAˆ γ .

6 Numerical Examples

We evaluate the proposed verification and synthesis approach by via a series of benchmark examples that are subject to either LTL or expected cost specifications. For both sets we compare to two synthesis tools: PRISM-POMDP [Norman et al., 2017] and SolvePOMDP [Walraven and Spaan, 2017] from the respective formal methods and planning communities. We further compare to another RNN-based synthesis procedure with a handcrafted memory structure for FSCs [Carr et al., 2019]. For proper comparison with the synthesis tools we adopt the experiment setup of [Carr et al., 2019], whereby we always iterate for 10 instances of retraining the RNN from counterexample data. Similarly, the proposed approach is not guaranteed to reach the optimum, but shall rather improve as far as possible within 10 iterations.

Implementation and Setup. We provide a Python toolchain that employs the probabilistic model checker Storm [Dehnert et al., 2017]. We train and encode the RNN policy networks ˆ γ using the deep learning library Keras. All experiments are run on a 2.3 GHz machine with a 12 GB memory limit and a max computation time of 105 seconds.

Settings. We analyze themethod on three different settings: Maze(c), Grid(c) and Navigation(c), for detailed descriptions of these examples see [Norman et al., 2017] and [Carr et al., 2019], respectively. In each of these settings the policies have an action space of the cardinal directions navigating through a grid-based environment. For the former two examples, we attempt to synthesize a policy that minimizes an expected cost subject to reaching a goal state a: EMmin (♦a). In the latter example, we seek a policy that maximizes the probability of satisfying an LTL specification, in particular avoiding obstacles X, both static and randomly moving, until reaching a target area a: PMmax (¬XUa).

Discussion. The results are shown in Table 1. The proposed extraction approach scales to significantly larger examples than both state-of-the-art POMDP solvers which compute near-optimal policies. While the handcrafted approach scales equally well, the extraction method produces higherquality policies - within 2% of the optimum. That effect is due to our automatic extraction of suitable FSCs. Note that an optimal policy for Maze(1) can be expressed using 2 memory states. The FSC structure employed by the handcrafted method uses this structure and consequently, for the small Maze environments, the handcrafted method synthesizes higher values. Yet, with larger environments the fixed memory structure produces poor policies as more memory states are beneficial to account for the past behavior.

7 Conclusion

We introduced a novel synthesis procedure for extracting and verifying RNN-based policies. In comparison to other approaches to verify RNNs, we take a model-based approach and provide guarantees for concrete applications modeled by POMDPs. Based on the verification results, we propose a way to either improve the extracted policy or the RNN itself. Our results demonstrate the effectiveness of the approach and that we are competitive to state-of-the-art synthesis tools.

Acknowledgements

This work was supported by DARPA D19AP00004, ONR N00014-18-1-2829, and ARL ACC-APG-RTP W911NF.