SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes

TL;DR

This paper introduces methods to convert strategies for hybrid Markov decision processes into compact, understandable decision trees that preserve safety and near-optimality, facilitating deployment in embedded systems.

Contribution

It presents a novel approach to learn small, safe, and near-optimal decision-tree representations of strategies from UPPAAL Stratego, enabling practical deployment.

Findings

Decision trees are significantly smaller and more understandable.

Guarantees on safety and near-optimality are maintained.

Trade-offs between size and optimality can be controlled.

Abstract

For hybrid Markov decision processes, UPPAAL Stratego can compute strategies that are safe for a given safety property and (in the limit) optimal for a given cost function. Unfortunately, these strategies cannot be exported easily since they are computed as a very long list. In this paper, we demonstrate methods to learn compact representations of the strategies in the form of decision trees. These decision trees are much smaller, more understandable, and can easily be exported as code that can be loaded into embedded systems. Despite the size compression and actual differences to the original strategy, we provide guarantees on both safety and optimality of the decision-tree strategy. On the top, we show how to obtain yet smaller representations, which are still guaranteed safe, but achieve a desired trade-off between size and optimality.

Figures

Equations

$$\pi ={\gamma }_o::P::{\alpha }_1::{\beta }_1::{\gamma }_1::P::{\alpha }_2::{\beta }_2::{\gamma }_2::P::\cdots$$

$${\dot{x}}_i=f_i(c,u,\vec{x}),$$

$$F_{(c,u)}(\tau ,\vec{x})=\vec{x}+{\int }_0^{\tau }f(c,u,\vec{x})dt.$$

Full text

1 Introduction

Cyber-physical systems often are safety-critical and hence strong guarantees on their safety are paramount. Furthermore, resource efficiency and the quality of the delivered service are strong requirements; the behaviour needs to be optimized with respect to these objectives, while of course staying within the bounds of what is still safe. In order to achieve this, controllers of such systems can be either implemented manually or automatically synthesized. In the former case, due to the complexity of the system, coming up with a controller that is safe is difficult, even more so with the additional optimization requirement. In the latter case, the synthesis may succeed with significantly less effort, though the requirement on both safety and optimality is still a challenge for current synthesis methods. However, due to the size of the systems, the produced controllers may be very complex, hard to understand, implement, modify, or even just output. Indeed, even for moderately sized systems, we can easily end up with gigabytes-long descriptions of their controllers (in the algorithmic context called strategies).

In this paper, we show how to provide a more compact representation, which can yield acceptably short and simple code for resource-limited embedded devices, and consequently can be more easily understood, maintained, modified, debugged, and the requirements are better traceable in the final controller. To this end, as the formalism for the compact representation we choose decision trees [42]. This representation is typically several orders of magnitude smaller than the classical explicit description and also is known for its interpretability and understandability [42, 48, 8]. The resulting encoded strategy may differ from the original one, but despite that and despite being smaller, it is still guaranteed to be safe and as nearly-optimal as the original one. Moreover, we can trade off additional decrease in size for decrease in performance (getting farther from optimum) to a desired degree, while maintaining safety.

Example 1

As a running example and one of the case studies, we use the following example introduced in [36] and expanded with stronger safety guarantees in [35].

We consider two cars Ego and Front, depicted in Figure 1. We control Ego, whereas Front is controlled by the environment. Ego is driving behind Front, and both cars have a discrete input (the acceleration) and a continuous state (the velocity). The goal of the adaptive cruise control in Ego is, first, to stay safe (by keeping the distance between the cars greater than a given safe distance), and second, to drive as close to Front as possible, i.e. to optimize the aggregated distance between the cars.

We use Uppaal Tiga [1] to get a safe strategy for Ego as in [35], and then Uppaal Stratego [18] to learn a (near-)optimal strategy for a desired cost function, given the constraints from the safe strategy. The resulting strategy is output as a list with almost 6 million configurations. Using our new methods, we obtain a decision tree representing the strategy, that has only about 2713 nodes. Additionally, we can trade performance to reduce the size even further, e.g. by increasing the aggregated distance reasonably we can reduce the size to 1247 nodes.

Our contribution:

• •

We design and implement a framework Stratego+ to transform safe and (near-)optimal strategies into their decision-tree representation, preserving safety and the same level of optimality, while being much smaller.

• •

We provide several transformations and ways to yet further decrease the size while preserving safety, but relaxing the optimality to a desired extent.

• •

We test our methods on three case studies, where we show size reductions of up to three orders of magnitude, and quantify the additional size-performance trade-off.

Our techniques can be used to represent (finite-memory non-stochastic) strategies for arbitrary systems exhibiting non-determinism (e.g. Markov decision processes, timed/concurrent/stochastic games). This paper demonstrates the technique on hybrid Markov decision processes, as that is the formalism used in Uppaal Stratego.

Related Work:

The problem of computing strategies for hybrid systems has been extensively studied in the past years. Most approaches rely on abstraction techniques: the continuous and infinite state space of the system is represented with a finite number of symbols, e.g. discrete points [25, 51], sets of states [15], etc. However, it is still hard to deal with uncontrollable components, even though some approaches exist such as robust control [27], or contract-based design [52], but they usually consider the uncontrollable component as a bounded perturbation and do not tackle stochastic behaviour. The tool PESSOA [49, 39] can synthesize controllers for cyber-physical systems represented by a set of smooth differential equations with a specification in a fragment of Linear Temporal Logic (LTL). Abstraction techniques are used in [28] for synthesizing strategies for a class of hybrid systems that involve random phenomena together with discrete and continuous behaviours. Discrete, stochastic dynamical systems are considered in [55], where the synthesis of strategies with respect to LTL objectives is made possible with an abstraction-refinement method. In [23] a number of benchmarks for hybrid system verification has been proposed, including a room heating benchmark. In [16] Uppaal SMC was applied to the performance evaluation of several strategies proposed in the benchmark. However, there was no focus on safety in this approach. In our work, the safety strategy synthesis relies on a discretization of the continuous variables, leading to a decidable problem that can be handled by Uppaal Tiga, but we furthermore provide safety guarantees for the original system with the use of a Timed Game abstraction based on a guaranteed Euler scheme [37].

In artificial intelligence, compact (factored) representations of Markov decision processes (MDPs) have been developed using dynamic Bayesian networks [6, 32], probabilistic STRIPS [34], algebraic decision diagrams [31], and also decision trees [6]. For a detailed survey of compact representations see [4]. Formalisms used to represent MDPs can, in principle, be used to represent strategies as well. In particular, variants of decision trees are probably the most used [6, 13, 33]. Decision trees have been also used in connection with real-time dynamic programming and reinforcement learning [5, 45].

In the context of verification, MDPs are often represented using variants of (MT)BDDs [20, 29, 40], and strategies by BDDs [56]. Learning a compact decision-tree representation of a strategy has been investigated in [38] for the case of body sensor networks, in [8] for finite (discrete) MDPs, and in [9] for finite games, but only with Boolean variables. Moreover, these decision trees can only predict a single action for a state configuration whereas in this work, we allow the trees to predict more than one action for a single configuration. In control theory, [57] proves that the problem of computing size-optimal determinisiation of controllers is NP-complete and hence discuss various heuristic-based determinisation algorithms. None of these works consider the optimization aspect, which being a soft constraint enables the trade-offs.

Permissive strategies have been studied in e.g. [2, 7, 21].

2 Preliminaries

2.1 Hybrid Markov Decision Processes

We describe the mathematical modelling framework. The correspondence to the Uppaal models is straightforward.

Definition 1 (HMDP)

A hybrid Markov decision process (HMDP) $\mathcal{M}$ is a tuple $({C},{U},X,{F},\delta)$ where:

the controller ${C}$ is a finite set of (controllable) modes $C=\{c_{1},\ldots,c_{k}\}$, 2. 2.

the uncontrollable environment ${U}$ is a finite set of (uncontrollable) modes $U=\{u_{1},\dots,u_{l}\}$, 3. 3.

$X=(x_{1},\ldots,x_{n})$ is a finite tuple of continuous (real-valued) variables, 4. 4.

for each $c\in C$ and $u\in U$, ${F}_{c,u}:\mathbb{R}_{>0}\times\mathbb{R}^{X}\rightarrow\mathbb{R}^{X}$ is the flow-function that describes the evolution of the continuous variables over time in the combined mode $(c,u)$, and 5. 5.

$\delta$ is a family of probability functions $\delta_{\gamma}:U\rightarrow[0,1]$, where $\gamma=(c,u,\vec{x})$ is a global configuration. More precisely, $\delta_{\gamma}(u^{\prime})$ is the probability that $u$ in the global configuration $\gamma=(c,u,\vec{x})$ will change to the uncontrollable mode $u^{\prime}$.

In the following, we denote by $\mathbb{C}$ the set of global configurations $C\times U\times\mathbb{R}^{X}$ of the HMDP $\mathcal{M}$. The above notion of HMDP actually describes an infinite-state Markov Decision Process [44], where choices of mode for the controller is made periodically and choice of mode for the uncontrollable environment is made probabilistically according to $\delta$. Note that abstracting $\delta_{\gamma}$ to the support $\hat{\delta_{\gamma}}=\{u\,|\,\delta_{\gamma}(u)>0\}$, turns $\mathcal{M}$ into a (traditional) hybrid two-player game. The inclusion of $\delta$ allows for a probabilistic refinement of the uncontrolled environment in this game. Such a refinement is irrelevant for the purposes of guaranteeing safety; however, it will be useful for optimizing the cost of operating the system. Indeed, rather than optimizing only the worst-case performance, we wish to optimize the overall expected behaviour.

Strategies

A – memoryless and possibly non-deterministic – strategy $\sigma$ for the controller ${C}$ is a function $\sigma:\mathbb{C}\rightarrow 2^{C}$, i.e. given the current configuration $\gamma=(c,u,\vec{x})$, the expression $\sigma(\gamma)$ returns the set of allowed actions in that configuration; in our setting, the actions are the controllable modes to be used for the duration of the next period. Non-deterministic strategies are also called permissive since they permit many actions instead of prescribing one.

The evolution of system over time is defined as follows. Let $\gamma=(c,u,\vec{x})$ and $\gamma^{\prime}=(c^{\prime},u^{\prime},\vec{x}^{\prime})$. We write $\gamma\stackrel{{\scriptstyle\tau}}{{\rightarrow}}\gamma^{\prime}$ in case $c^{\prime}=c,u^{\prime}=u$ and $\vec{x}^{\prime}={F}_{(c,u)}(\tau,\vec{x})$.

A run is an interleaved sequence $\pi\in\mathbb{C}\times(\mathbb{R}\times\mathbb{C}\times\mathbb{C}\times\mathbb{C})^{*}$ of configurations and relative time-delays of some given period $P$:

[TABLE]

Then $\pi$ is a run according to the strategy $\sigma$ if after each period $P$ the following sequence of discrete (instantaneous) changes are made:

the value of the continuous variables are updated according to the flow of the current mode, i.e. $\gamma_{i-1}=(c_{i-1},u_{i-1},\vec{x}_{i-1})\stackrel{{\scriptstyle P}}{{\rightarrow}}(c_{i-1},u_{i-1},\vec{x}_{i})=:\alpha_{i}$; 2. 2.

the environment changes to any possible new mode, i.e. $\beta_{i}=(c_{i-1},u_{i},\vec{x}_{i})$ where $\delta_{\alpha_{i}}(u_{i})>0$; 3. 3.

the controller changes mode according to the strategy $\sigma$, i.e. $\gamma_{i}=(c_{i},u_{i},\vec{x}_{i})$ with $c_{i}\in\sigma(\beta_{i})$.

Safety

A strategy $\sigma$ is said to be safe with respect to a set of configuration $S\subseteq\mathbb{C}$, if for any run $\pi$ according to $\sigma$ all configurations encountered are within $S$, i.e. $\alpha_{i},\beta_{i},\gamma_{i}\in S$ for all $i$ and also $\gamma^{\prime}_{i}\in S$ whenever $\gamma_{i}\stackrel{{\scriptstyle\tau}}{{\rightarrow}}\gamma^{\prime}_{i}$ with $\tau\leq P$. Note that the notion of safety does not depend on the actual $\delta$, only on its supports. Recall that almost-sure safety, i.e. with probability 1, coincides with sure safety.

We use a guaranteed set-based Euler method introduced in [35] to ensure safety of a strategy not only at the configurations where we make decisions, but also in the continuum in between them. We refer the reader to Appendix 0.A.2 for a brief reminder of this method.

Optimality

Under a given deterministic (i.e. permitting one action in each configuration) strategy $\sigma$ the game $\mathcal{M}$ becomes a completely stochastic process $\mathcal{M}\upharpoonright\sigma$, inducing a probability measure on sets of runs. In case $\sigma$ is non-deterministic or permissive, the non-determinism in $\mathcal{M}\upharpoonright\sigma$ is resolved uniformly at random. On such a process, we can evaluate a given optimization function. Let $H\in\mathbb{N}$ be a given time-horizon, and $D$ a random variable on runs, then $\mathbb{E}^{\mathcal{M},\gamma}_{\sigma,H}(D)\in\mathbb{R}_{\geq 0}$ is the expected value of $D$ on the space of runs of $\mathcal{M}\upharpoonright\sigma$ of length111Note that there is a bijection between length of the run and time, as the time between each step, $P$, is constant. $H$ starting in the configuration $\gamma$. As an example of $D$, consider the integrated deviation of a continuous variable, e.g. distance between Ego and Front, with respect to a given target value.

Consequently, given a (memoryless non-deterministic) safety strategy $\sigma_{\mathit{safe}}$ with respect to a given safety set $S$, we want to find a deterministic sub-strategy222i.e. a strategy that for every configuration returns a (non-strict) subset of the actions allowed by the safe strategy $\sigma_{\mathit{opt}}$ that optimizes (minimizes or maximizes) $\mathbb{E}^{\mathcal{M},\gamma}_{\sigma_{\mathit{safe}},H}(D)$.

2.2 Decision Trees

From the perspective of machine learning, decision trees (DT) [42] are a classification tool assigning classes to data points. A data point is a $d$-dimensional vector $\vec{v}=(v_{1},v_{2},\dots,v_{d})$ of features with each $v_{i}$ drawing its value from some set $D_{i}$. If $D_{i}$ is an ordered set, then the feature corresponding to it is called ordered or numerical (e.g. $\mathit{velocity}\in\mathbb{R}$) and otherwise, it is called categorical (e.g. $\mathit{color}\in\{\mathit{red,green,blue}\}$). A (multi-class) DT can represent a function $f:\prod_{i=1}^{d}D_{i}\to A$ where $A$ is a finite set of classes.

A (single-label) DT over the domain $D=\prod_{i=1}^{d}D_{i}$ with labels $A$ is a tuple $\mathcal{T}=(T,\rho,\theta)$, where $T$ is a finite binary tree, $\rho$ assigns to every inner node predicates of the form $x_{i}\sim c$ where $\sim~{}\in\{\leq,=\}$, $c\in D_{i}$, and $\theta$ assigns to every leaf node a list of natural numbers $[m_{1},m_{2},\dots,m_{|A|}]$. For every $\vec{v}\in D$, there exists a decision path from the root node to some leaf $\ell_{\vec{v}}$. We say that $\vec{v}$ satisfies a predicate $\rho(t)$ if $\rho(t)$ evaluates to true when its variables are evaluated as given by $\vec{v}$. Given $\vec{v}$ and an inner node $t$ with a predicate $\rho(t)$, the decision path selects either the left or right child of $t$ based on whether $\vec{v}$ satisfies $\rho(t)$ or not. For $\vec{v}$ from the training set, we say that the leaf node $\ell_{\vec{v}}$ contains $\vec{v}$. Then $m_{a}$ of a leaf is the number of points contained in the leaf and classified $a$ in the training set. Further, the classes assigned by a DT to a data point $\vec{v}$ (from or outside of the training set) are given by $\arg\max\theta(\ell_{\vec{v}})=\{i\mid\forall i,j\leq\left\lvert A\right\rvert.~{}\theta(\ell_{\vec{v}})_{i}\geq\theta(\ell_{\vec{v}})_{j}\}$, i.e. the most frequent classes in the respective leaf.

Decision trees may also predict sets of classes instead of a single class. Such a generalization (representing functions of the type $\prod_{i=1}^{d}D_{i}\to 2^{A}$) is called a multi-label decision tree. In these trees, $\theta$ assigns to every leaf node a list of tuples $[(n_{1},y_{1})$, $(n_{2},y_{2})$, $\dots$, $(n_{|A|},y_{|A|})]$ where $n_{a},y_{a}\in\mathbb{N}$ are the number of data points in the leaf not labelled by class $a$ and labelled by class $a$, respectively. The (multi-label) classification of a data point is then typically given by the majority rule, i.e. it is classified as $a$ if $n_{a}<y_{a}$.

A DT may be constructed using decision-tree learning algorithms such as ID3 [46], C4.5 [47] or CART [10]. These algorithms take as input a training set, i.e. a set of vectors whose classes are already known, and output a DT classifier. The tree constructions start with a single root node containing all the data points of the training set. The learning algorithms explore all possible predicates $p=x_{i}\sim c$, which split the data points of this node into two sets, $X_{p}$ and $X_{\neg p}$. The predicate that minimizes the sum of entropies333Entropy of a set $X$ is $H(X)=\sum_{a\in A}p_{a}\log_{2}(p_{a})+(1-p_{a})\log_{2}(1-p_{a})$, where $p_{a}$ is the fraction of samples in $X$ belonging to class $a$. See [14] for more details. of the two sets is selected. These sets are added as child nodes to the node being split and the whole process is repeated, splitting each node further and further until the entropy of the node becomes 0, i.e. all data points belong to the same class. Such nodes are called pure nodes. This construction is extended to the multi-label setting by some of the algorithms. A multi-label node is called pure if there is at least one class that is endorsed by all data points in that node, i.e. $\exists a\in A:n_{a}=0$.

If the tree is grown until all leaves have zero entropy, then the classifier memorizes the training data exactly, leading to overfitting [42]. This might not be desirable if the classifier is trained on noisy data or if it needs to predict classes of unknown data. The learning algorithms hence provide some parameters, known as hyperparameters, which may be tuned to generalize the classifier and improve its accuracy. Overfitting is not an issue in our setup where we want to learn the strategy function (almost) precisely. However, we can use the hyperparameters to produce even smaller representations of the function, at the “expense” of not being entirely precise any more. One of the hyperparameters of interest in this paper is the minimum split size $k$. It can be used to stop splitting nodes once the number of data points in them become smaller than $k$. By setting larger $k$, the size of the tree decreases, usually at the expense of increasing the entropy of the leaves. There also exist several pruning techniques [41, 22], which remove either leaves or entire subtrees after the construction of the DT.

2.3 Standard Uppaal Stratego Workflow

The process of obtaining an optimized safe strategy $\sigma_{opt}$ using Uppaal Stratego is depicted as the grey boxes in Fig. 2. First, the HMDP $\mathcal{M}$ is abstracted into a 2-player (non-stochastic) timed game $\mathcal{TG}$, ignoring any stochasticity of the behaviour. Next, Uppaal Tiga is used to synthesize a safe strategy $\sigma_{\mathit{safe}}:\mathbb{C}\to 2^{C}$ for $\mathcal{TG}$ and the safety specification $\varphi$, which is specified using a simplified version of timed computation tree logic (TCTL)[1]. After that, the safe strategy is applied on $\mathcal{M}$ to obtain $\mathcal{M}\upharpoonright\sigma_{\mathit{safe}}$. It is now possible to perform reinforcement learning on $\mathcal{M}\upharpoonright\sigma_{\mathit{safe}}$ in order to learn a sub-strategy $\sigma_{\mathit{opt}}$ that will optimize a given quantitative cost, given as any run-based expression containing e.g. discrete variables, locations, clocks, hybrid variables. For more details, see [17, 19].

3 Stratego+

In this section, we discuss the new Uppaal Stratego+ framework following with each of its components are elucidated.

3.1 New Workflow

Uppaal Stratego+ extends the standard workflow in two ways: Firstly, in the top row, we generate the DT $\mathcal{T}_{opt}$ that exactly represents $\sigma_{\mathit{opt}}$, yielding a small representation of the strategy.

The DT learning algorithm can make use of two (hyper-)parameters $k$ and $p$ which may be used to prune the DT; this approach is described in Section 3.4. While pruning reduces the size of the DT, the resultant tree no longer represents the strategy exactly. Hence it is not possible to prune a DT representing deterministic strategies, like in the case of the $\sigma_{\mathit{opt}}$ described in the first row of the workflow, as safety would be violated.

However, for our second extension we apply the DT learning algorithm to the non-deterministic, permissive strategy $\sigma_{\mathit{safe}}$, resulting in $\mathcal{T}_{\sigma_{\mathit{safe}}}^{k,p}$. This DT is less permissive, thereby smaller, since the pruning disallows certain actions; yet it still represents a safe strategy (details in Section 3.4). Next, as in the standard workflow, this less permissive safe strategy is applied to the game and Stratego is used to get a near-optimal strategy $\sigma_{\mathit{opt}}^{k,p}$ for the modified game $\mathcal{M}\upharpoonright\mathcal{T}_{\sigma_{\mathit{safe}}}^{k,p}$. In the end, we again construct a DT exactly representing the optimal strategy, namely $\mathcal{T}_{opt}^{k,p}$. Note that in the game restricted to $T_{\sigma_{\mathit{safe}}}^{k,p}$ fewer actions are allowed than when it is restricted only to $\sigma_{\mathit{safe}}$, and hence the resulting strategy could perform worse. For example, let $\sigma_{\mathit{safe}}$ allow decelerating or remaining neutral for some configuration, while $T_{\sigma_{\mathit{safe}}}^{k,p}$ pruned the possibility to remain neutral and only allows decelerating. Thus, $\sigma_{\mathit{opt}}$ remains neutral, whereas $\sigma_{\mathit{opt}}^{k,p}$ has to decelerate and thereby increase the distance that we try to minimize.

In both cases, the resulting DT is safe by construction since we allow the DT to predict only pure actions (actions allowed by all configurations in a leaf, see next section for the formal definition). We convert these trees into a nested if-statements code, which can easily be loaded onto embedded systems.

3.2 Representing strategies using DT

A DT with domain $\mathbb{C}$ and labels $C$ can learn a (non-deterministic) strategy $\sigma:\mathbb{C}\to 2^{C}$. The strategy is provided as a list of tuples of the form $(\gamma,\{a_{1},\dots,a_{k}\})$, where $\gamma$ is a global configuration and $\{a_{1},\dots,a_{k}\}$ is the set of actions permitted by $\sigma$. The training data points are given by the integer configurations $\gamma\in\mathbb{C}$ (safety for non-integer points is guaranteed by the Euler method; see Section 2.1) and the set of classes for each $\gamma$ is given by $\sigma(\gamma)$. Consequently, a multi-label decision tree learning algorithm as described in Section 2.2 can be run on this dataset to obtain a tree $\mathcal{T}_{\sigma}$ representing the strategy $\sigma$.

Each node of the tree contains the set of configurations that satisfy the decision path traced from the root of the tree to the node. The leaf attribute $\theta$ gives, for each action $a$, the number of configurations in the leaf where the strategy disallows and allows $a$, respectively. For example, consider a node with 10 configurations with $\theta=[(0,10),(2,8),(9,1)]$. This means that the first action is allowed by all 10 configurations in the node, the second action is disallowed by 2 configurations and allowed by 8, and the third action is disallowed by 9 configurations and allowed only by 1.

Since we want the DT to exactly represent the strategy, we need to run the learning algorithm until the entropy of all the leaves becomes 0, i.e. all configurations of the leaf agree on every action. More formally, given a leaf $\ell$ with $n$ configurations we require $\theta(\ell)=(0,n)$ or $\theta(\ell)=(n,0)$ for every action. We call an action that all configurations allow a pure action.

The table on the left of Fig. 3 shows a toy strategy. Based on values of distance $d$ and velocity $v$, it permits a subset of the action set $\{\mathit{dec},\mathit{neu},\mathit{acc}\}$. A corresponding DT encoding is displayed on the right of Fig. 3.

3.3 Interpreting DT as strategy

To extract a strategy from a DT, we proceed as follows: Given a configuration $C$, we pick the leaf $\ell_{C}$ associated with it by evaluating the predicates and following a path through the DT. Then we compute $\theta(\ell_{C})$ = $[(n_{1},y_{1}),$ $(n_{2},y_{2}),\dots,$ $(n_{|A|},y_{|A|})]$ where $n_{a},y_{a}\in\mathbb{N}$ are the number of data points in the leaf not labelled by class $a$ and labelled by class $a$, respectively. The classes assigned to $\ell_{C}$ are exactly its pure actions, i.e. $\{a\mid(0,y_{a})\in\theta(\ell_{C})\}$.

Note that allowing only pure actions is necessary in order to preserve safety. We do not follow the common (machine learning) way of assigning classes to the nodes based on the majority criterion, i.e. the majority of the data points in that node allow the action; because then the decision tree might prescribe unsafe actions just because they were allowed in most of the configurations in the node. This is also the reason why the DT-learning algorithm described in the previous section needs to run until the entropy of all leaves becomes 0.

3.4 Learning smaller, yet safe DT

We now describe how to learn a DT for a safe strategy that is smaller than the exact representation, but still preserves safety. A tree obtained using off-the-shelf DT learning algorithms is unlikely to exactly represent the original strategy.444This is because DT learning algorithms are usually configured to avoid overfitting on the dataset We use two different methods to achieve the goal: firstly, we use the standard hyperparameter named minimum split size, and secondly, we introduce a new post-processing algorithm called safe pruning. Both methods rely on the given strategy being non-deterministic/permissive, i.e. permitting several actions in a leaf.

(1) Using minimum split size

The splitting process can be stopped before the entropy becomes 0. We do this by introducing a parameter $k$, which determines the minimum number of data points required in a node to consider splitting it further. During the construction of the tree, a node is usually split if its entropy is greater than 0. When $k$ is set to an integer greater than 2, a node is split only if both the entropy is greater than 0 and the number of data points (configurations) in the node is at least $k$. The strategy given by such a tree is safe as long as it predicts only pure actions, i.e. $a$ with $n_{a}=0$. In order to obtain a fully expanded tree, $k$ may be set to 2 (in nodes with $<2$ configurations, there is nothing to split). For larger $k$, the number of pure actions in the leaves decreases. Ultimately, for too large $k$, we would obtain a tree that has some leaf nodes not containing any pure actions. In such a case, the strategy represented by the DT would not be well-defined, as for some data point no action could be picked. However, this can be detected immediately during the construction.

(2) Using safe pruning

Another way of obtaining a smaller tree is by using a procedure to prune the leaves of the produced tree by merging them while preserving safety. For example, consider the decision node on the left of Figure 4 with two children that are leaves A and B. For A, only the action $\mathit{dec}$ is pure (i.e. allowed by all configurations in the leaf), while for B both $\mathit{dec}$ and $\mathit{neu}$ are pure. Since the sets of pure actions of the two leaf nodes intersect, we can safely remove both A and B and replace the decision node with a new leaf node C that contains only those actions that are in the intersection, in this case only $\mathit{dec}$.

Algorithm 1 describes the pruning process formally. If $\theta$ returns only safe actions, then the tree obtained after pruning is guaranteed to represent a safe strategy, although a less-permissive one. The algorithm may be run for multiple (possibly 0) rounds, denoted by $p$, at most until we get a “fully pruned” tree representing a safe but deterministic strategy. We denote by $\mathcal{T}_{\sigma_{\mathit{safe}}}^{k,p}$ the decision tree for $\sigma_{\mathit{safe}}$ constructed by only splitting nodes with $k$ or more data points, followed by $p$ rounds of safe pruning. Clearly, the more permissive the original strategy is, the more we can prune using safe pruning.

When generating $T_{\sigma_{\mathit{safe}}}^{k,p}$, we use a modified implementation of the CART decision tree learning algorithm implemented in the DecisionTreeClassifier class of the Python-based machine learning library Scikit-learn [43]. Since we construct the DT from a safe strategy and as long as we let the DT-encoded strategy have at least one pure action in each leaf, the strategy will remain safe. With this in mind, we can freely change the parameters of the DecisionTreeClassifier class. However, in our experiments, we picked only the minimum split size $k$ from the Scikit-parameters as a demonstrative example, as well as our newly introduced $p$. The methods described in this paper would work with other parameters as well.

3.5 Comparing DTs to Binary Decision Diagrams

A Binary Decision Diagram (BDD, e.g. [11]) is a popular data structure that can be used to represent boolean functions $f:\mathbb{B}^{n}\to\mathbb{B}$. It may also be used to represent strategies by encoding configurations and actions into a suitable form via bit-blasting, i.e. converting them into propositional formulae. For example, the configuration-action pair $((x=6,y=2),a_{0})$ can be represented as $(x_{2}\land x_{1}\land\neg x_{0}\land\neg y_{2}\land y_{1}\land\neg y_{0}\land a_{0})$, if it is known that the maximum value that $x$ and $y$ can take is less than 8 (3 bits). A strategy can be seen as a disjunction $\bigvee_{\gamma,a\in\sigma(\gamma)}(\gamma,a)$ of all configuration-action pairs $(\gamma,a)$ permitted by the strategy $\sigma$. Such an encoding allows for an easy conversion into a BDD. Though theoretically straightforward, there are some practical concerns involved when constructing the BDD. Mainly, the ordering of the variables in the BDD can drastically change its size. While computing the optimal ordering so as to have the smallest BDD is an NP-complete problem [3], various heuristics exist that can be used to get better orderings. We use the CUDD package [54] to construct the BDD, along with Rudell’s Sifting reordering technique [50].

The main disadvantage of DTs compared to BDDs is that isomorphic subgraphs are not merged (DTs are trees, BDDs are directed acyclic graphs); and even if merging was allowed, it would not save much. Indeed, since DT may choose different predicates on the same level (which is an advantage in contrast to BDD with a fixed variable ordering) isomorphic subgraphs occur rarely. There are further advantages of DT, related to learning, that make them more compact than BDD in some contexts, e.g. [8, 9]. Firstly, they can be learnt fast, using the entropy-based heuristic, compared to the graph processing and variable re-ordering of BDDs. Secondly, a DT can ignore “don’t-care inputs”; these inputs are encodings of things that are not valid configuration-action pairs, in the sense that either the action is not available in the configuration or that it is not a valid configuration at all. In contrast, a BDD has to explicitly either allow or disallow these inputs. Thirdly, DT learning can also be used to represent the strategy imprecisely using a smaller DT, which can be model checked for safety. For the modifications described in Section 3.4, we do not even need to re-verify safety, because this property is preserved by both our size reduction techniques. Fourthly, DT can use much wider class of predicates, compared to single bit tests for a bit representation in a BDD. This final point is also a reason (together with the smaller size) why DT is a more understandable representation than a BDD [8, 9]. We also illustrate this point on a case-study in Remark 1.

4 Case Studies and Experimental Results

In this section, we evaluate the techniques discussed above on three different case studies: (1) the adaptive cruise control model introduced in the motivation; (2) a two tank case study introduced in [30]; and (3) the heating system of a two room apartment adapted from [26].

Table 1 compares representations for our case studies obtained in different ways. We discuss results for the three case studies, denoted cruise, twotanks, and tworooms respectively. Additionally, the first line displays cruise without the integrated Euler method, to illustrate the effect of Euler method on the final size. All the representations are safe and as optimal as $\sigma_{\mathit{opt}}$ produced by Uppaal Stratego.

For each of the models we display the following information: the third column lists the number of items in the explicit list representation of $\sigma_{\mathit{opt}}$ output by Uppaal Stratego. The fourth column lists the number of those items that are actually relevant, i.e. sets of configurations where an actual decision is to be made. The fifth and sixth column list the sizes of BDD and DT representations learnt from $\sigma_{\mathit{opt}}$, i.e. the upper path in Fig. 2. For BDDs, since the initial ordering plays a role in the size of the final result despite applying the re-ordering heuristics, we ran 40 experiments for each model with random initial variable orderings. For creating BDDs, we used the free Python library tulip-control/dd as an interface to CUDD.

We conclude that both BDDs and DTs reduce the size by several order of magnitude. DTs are slightly better in all cases, and 2 orders of magnitude smaller in the tworooms model. Note that reliably achieving good results when constructing the BDD relies on repeating the construction several times; since already constructing a single BDD and applying the heuristics [50] already took roughly 10 times longer than DT learning, DT can be obtained one or two orders of magnitude faster than BDDs, depending on how many times one tries constructing the BDD. Further, for the two tanks, only DT realizes that the strategy is actually trivial. The main reason for BDD not to spot this is the point of ignoring “don’t-care” inputs addressed in Section 3.5.

Table 2 shows how the size of the DT can be further reduced by the bottom path of Fig. 2, when the “exact representation” criterion is relaxed. It displays the performance, i.e. the aggregated distance to Front car, and size of $\mathcal{T}_{\mathit{opt}}^{k,p}$ for different combinations of the pruning parameters $k$ and $p$. Recall that using no pruning ($k=2,p=0$) yields the same DT as the upper path of Fig. 2, i.e. $\mathcal{T}_{\mathit{opt}}^{2,0}=\mathcal{T}_{\mathit{opt}}$.

We observed that for cruise, increasing the values of $k$ and $p$ buys a reduction in size of the DT against a reduction in performance. For instance, using $k=80,p=0$, one can decrease the size to 2485 (by 8.4%) while deteriorating the performance to 2907 (by 10%). Allowing for half the performance (double the aggregated distance), one can make the DT even smaller than half of its original size, e.g. by setting $k=10,p=2$. The shading and colouring of the table display different “trade-off zones”, each with comparable savings/losses. The same conclusions hold for cruise${}_{\texttt{non-Euler}}$, see the similar Table 4 in Appendix 0.A.3. For tworooms (Table 3), the best performance is observed not with $k=2,p=0$, but with $k=50,p=0$. We conjecture that the less permissive safe strategy assists Stratego in performing the optimisation faster by reducing the size of the search space. As a result, here we get a both smaller and more performant strategy. In the case of twotanks, already $\mathcal{T}_{\mathit{opt}}$ has only a single node, hence no further reductions are possible.

Remark 1

Interestingly, domain knowledge can reduce the DT size further and make the representation more understandable. Indeed, for the cruise model we were able to construct a DT with only 25 nodes, designing our predicates based on the car kinematics. For example, the expected time until the front car reaches minimal velocity if it only decelerates from now on (1) plays an important role in the decision making and (2) can be easily expressed by solving the standard kinematics equation $v(t)=v_{\text{current}}-a_{\text{dec}}\cdot t$. The resulting DT (illustrated in Appendix 0.A.4) is thus very small and easy to interpret, as each of the few nodes has a clear kinematic interpretation. The DT thus open the possibility for strategy representation to profit from predicate/invariant synthesis.

5 Conclusion

We have provided a framework for producing small representations of safe and (near-)optimal strategies, without compromising safety. As to (near-)optimality, we can choose between two options: (i) not compromising it, or (ii) finding a suitable trade-off between compromising it (causing drops of performance) and additional size reductions. Compared to the original sizes, we achieve orders-of-magnitude reductions, allowing for efficient usage of the strategies in e.g. embedded devices. Compared to BDD representation, the size of the DT representation is smaller and can be computed faster; additionally trivial solutions are represented by trivial DTs. DTs are more readable as argued in [9, 8].

A detailed examination of the latter point in the hybrid context remains future work. Further, candidates for more complex predicates could be automatically generated based on given domain knowledge or learnt from the data similarly to invariants from program runs [24, 53]. As illustrated in Remark 1, this could lead to further reduction in size and improved understandability. Additionally, isomorphic/similar subtrees could be merged as in decision diagrams and further optimizations for algebraic decision diagrams [57] could be employed. Finally, we plan to visualize the DT representation of the strategies directly in Uppaal Stratego+ for convenience of the users.

Appendix 0.A Appendix

0.A.1 Description of case studies

Two rooms model.

This case study is based on a simple model of a two-room apartment, heated by one heater in each room. In this example, the objective is to control the temperature of both rooms by switching on or off the heaters in the rooms. There is heat exchange between the two rooms and with the environment (external temperature, which varies randomly within a set).

Cruise Control.

Two cars Ego and Front are driving on a road as shown in Figure 1. We are capable of controlling Ego but not Front. Both cars can drive a maximum of 20 m/s forward and a maximum of 10 m/s backwards. The cars have three different possible accelerations: -2 m/s2, 0 m/s2 and 2 m/s2, between which they can switch instantly. For the cars to be safe, there should be a distance of at least 5 m between them. Any distance less than 5 m between the cars is considered unsafe. Ego’s sensors can detect the position of Front only within 200 meters. If the distance between the cars is more than 200 meters, then Front is considered to be far away.

In this example, the aim is to synthesize a strategy for controllable car Ego such that it always stays far enough from uncontrollable car Front.

For the adaptive cruise control model, we differentiate between the model that is only safe at time points where an action is possible, called cruise${}_{\texttt{non-Euler}}$; and the model improved with the Euler method to be safe at all time points between two actions, called just cruise.

Two Tanks.

The two-tank system, illustrated in Figure 5, is a linear example taken from [30]. The system consists of two tanks and two valves. The first valve ($Q_{1}$ in Fig. 5) adds to the inflow of tank 1 and the second valve ($Q_{2}$) is a drain valve for tank 2. There is a constant outflow from tank 2 caused by a pump ($Q_{B}$), as well as a constant inflow into tank 1 ($Q_{0}$). There is also a flow from tank 1 to tank 2 ($Q_{A}$) which depends on the water level in tank 1. The system is linearised at a desired operating point. The objective is to keep the water level in both tanks within limits using a discrete open/close switching strategy for the valves.

0.A.2 Guaranteed over-approximation using the Euler Method

We briefly recall the technique used in [35] to compute strategies that are safe at all time points, not just at multiples of the period $P$.

Let us consider an HMDP $\mathcal{M}=({C},{U},X,{F},\delta)$ where the dynamics of each continuous variable $x_{i}\in X$ is subject to a differential equation of the form

[TABLE]

with $c\in C$ and $u\in U$. For every $\gamma=(c,u,\vec{x})$ and $\tau\in\mathbb{R}$, the update $\gamma\stackrel{{\scriptstyle\tau}}{{\rightarrow}}(c,u,{F}_{(c,u)}(\tau,\vec{x}))$ must match the solution of the differential equation (1), i.e.

[TABLE]

It is easy to compute the solution of a linear differential equation [12]. However, in the general case, computing the integral on the right-hand side of (2) is not possible exactly. Approximate solutions can be obtained with the use of numerical schemes, such as Euler or Runge-Kutta schemes, but in order to ensure absolute safety of the system, they should be associated with guaranteed error bounds. Furthermore, one has to ensure that the system is safe between time steps ($\gamma^{\prime}\in S$ whenever $\gamma_{i}\stackrel{{\scriptstyle\tau}}{{\rightarrow}}\gamma^{\prime}$ with $\tau\leq P$). In order to achieve that, [35] proceeds as follows. First, the given HMDP $\mathcal{M}=({C},{U},X,{F},\delta)$ is extended into an HMDP $\mathcal{M}^{\prime}=({C},{U},(X^{\min},X^{\max}),{F}^{\prime},\delta^{\prime})$ where $X^{\min}=(x_{1}^{\min},\ldots,x_{n}^{\min})$ and $X^{\max}=(x_{1}^{\max},\ldots,x_{n}^{\max})$ will form a lower and an upper bound on the actual valuation of $X$ at all times, and $\delta^{\prime}$ is an abstract transition function for the opponent. From a given global configuration $\gamma^{\prime}=(c,u,(\vec{x}^{min},\vec{x}^{max}))$ of $\mathcal{M}^{\prime}$, $\delta^{\prime}$ enables all possible transitions that have non zero probability from $\gamma=(c,u,\vec{x})$ in $\mathcal{M}$ for some value of $\vec{x}$ between $\vec{x}^{min}$ and $\vec{x}^{max}$, i.e. $\delta^{\prime}=\{u|\delta_{(c,u,\vec{x})}(u)>0,\vec{x}^{min}\leq\vec{x}\leq\vec{x}^{max}\}$. Then the flow function ${F}^{\prime}_{c,u}:\mathbb{R}_{>0}\times\mathbb{R}^{(X_{\min},X_{\max})}\rightarrow\mathbb{R}^{(X_{\min},X_{\max})}$ implements a guaranteed (set-based) Euler method which ensures the following property: whenever

• •

$(\vec{w}^{\min},\vec{w}^{\max})={F}^{\prime}_{(c,u)}(P,(\vec{v}^{\min},\vec{v}^{\max}))$ and

• •

$\vec{w}={F}_{(c,u)}(t,\vec{v})$ for some $t\leq P$ and $\vec{v}^{\min}\leq\vec{v}\leq\vec{v}^{\max}$

then also $\vec{w}^{\min}\leq\vec{w}\leq\vec{w}^{\max}$. For further details, we refer the reader to [37, 35].

From the augmented HMDP $\mathcal{M}^{\prime}$, we can build a standard timed game [35] $\mathcal{TG}$ by under-approximating $X^{\min}$ to its floor integer part, and $X^{\max}$ to its ceiling integer part. Consequently, one can use Uppaal Tiga to synthesize a strategy that ensures the safety of the initial HMDP. A simulation showing the bounding of the continuous trajectory of $\mathcal{M}$ by its timed-game abstraction $\mathcal{TG}$ is given in Fig. 6.

0.A.3 More experimental results

Table 4 shows the trade-off between size and performance for the cruise${}_{\texttt{non-Euler}}$ model. Figure 7 shows a simulation run of tworooms.

0.A.4 Handcrafted Small DT for Adaptive Cruise Control