Monitor-Based Runtime Assurance for Temporal Logic Specifications

TL;DR

This paper presents a runtime safety assurance architecture for systems with specifications in Linear Temporal Logic, utilizing monitors and backup strategies to ensure safety in real-time applications.

Contribution

It introduces a novel safety controller architecture combining performance, backup, and assurance components with FSM-based monitors for LTL specifications.

Findings

Successfully implemented on a cyber-physical system

Guarantees safety by detecting and preventing bad system trajectories

Demonstrates effectiveness through a detailed case study

Abstract

This paper introduces the safety controller architecture as a runtime assurance mechanism for system specifications expressed as safety properties in Linear Temporal Logic (LTL). The safety controller has three fundamental components: a performance controller, a backup controller, and an assurance mechanism. The assurance mechanism uses a monitor, constructed as a finite state machine (FSM), to analyze a suggested performance control input and search for system trajectories that are bad prefixes of the system specification. A fault flag from the assurance mechanism denotes a potentially dangerous future system state and triggers a sequence of inputs that is guaranteed to keep the system safe for all time. A case study is presented which details the construction and implementation of a safety controller on a non-deterministic cyber-physical system.

Figures

Equations

$$[w\models \phi ]=\{\begin{array}{ll}\top & \text{if }\forall \sigma \in {\Sigma }^{\omega }:w\sigma \models \phi \\ \perp & \text{if }\forall \sigma \in {\Sigma }^{\omega }:w\sigma /\models \phi \\ ?& \text{otherwise.}\end{array}$$

$$x^{+}=f(x,u,d)$$

$$x^{+}=f(x,u)$$

$$x_k\in \mathcal{X}\subseteq {\mathbb{R}}^n,u_k\in \mathcal{U}\subseteq {\mathbb{R}}^m,k\in \mathbb{N}.$$

$$\begin{array}{rl}{R}_1& =\{(x,q)\mid x=f(x_0,g_0(x_0),d),\\ & d\in \mathcal{D},q=\delta (q_0,L(x))\}\\ R_{i+1}& =\{(x,q)\mid x=f(\bar{x},g_i(\bar{x}),d),(\bar{x},\bar{q})\in R_i,\\ & d\in \mathcal{D},q=\delta (\bar{q},L(x))\}\end{array}$$

$$L(x,v)=\{\begin{array}{ll}\varnothing & x<2.54,v<2\\ Tower& x\ge 2.54,v<2\\ Fast& x<2.54,v\ge 2\\ Tower\wedge Fast& x\ge 2.54,v\ge 2.\end{array}$$

$$S^b=\{(x,v,q)\mid q=q_{\top }\text{ or }v\le -0.69x+1.66,q=q_{?}\}.$$

Full text

I Introduction

Modern cyber-physical systems (CPS) are complex and sometimes do not behave as expected. Correctness can be partially addressed with offline verification, however, the end-to-end verification of an entire system is often prevented by its complexity. In order to compensate for the lack of assurances, it is desirable to enforce correctness online.

For purely cyber systems, runtime correctness can be checked online using monitors [1, 2, 3, 4, 5]. In this context, correctness is evaluated with respect to a temporal logic specification; a monitor observes the temporal behaviors of the cyber system and notifies the system operator if a fault is suspected. Such monitors are convenient for system verification because they can be algorithmically generated from temporal logic specifications. Monitors fail, however, to assure correct system behavior; monitors can only detect system faults and do not have the ability to intervene. As an alternative, edit automata read a sequence of system inputs and, should it recognize a harmful string in that sequence, edits the control input before it is passed on in the software [6]. Edit automata are formed corresponding to temporal logic specifications, however, it is unclear how hard it is to generate an edit automaton given such a specification. It was shown by [7], for instance, that an edit automaton for a given specification is not unique, and that the algorithm presented in [6] for constructing edit automata is not optimal.

For physical control systems, runtime assurance can be performed by identifying a controlled forward invariant region of the state space, and then ensuring that the system does not exceed the boundary of this region. Verification techniques of this nature include level set methods [8], barrier certificate based methods [9], and certain model predictive control (MPC) based methods [10, 11]. Computing invariant sets, however, is generally computationally expensive, and moreover, this approach typically is only well suited to analyze invariance conditions or reach conditions. CPS could, for instance, use an invariance check to avoid stationary obstacles or to patrol a static region of the state space; however, this method is ineffective for more complex system properties, for example, properties which specify that system goals are met in a certain order.

It is not overtly clear how one might combine results for purely cyber systems with results for physical systems in order to ensure correct behavior of modern CPS against complex specifications. For example, by the time a monitor recognizes that a physical system is about to violate its operating specification, the system may have entered an invariant region of the state space from which it is impossible to satisfy the system specification going forward. A basic idea that has emerged in different contexts is to verify correct system behavior at runtime, and then protect the potentially faulty complex controller with a less sophisticated, but demonstrably safer, backup controller. This technique is referred to as “runtime assurance” or the Simplex Architecture [12].

In this paper, we investigate runtime assurance for system specifications that can be expressed in Linear Temporal Logic (LTL). In particular, we restrict to the class of safety properties. An LTL property is a safety property if each invalid infinite trace contains a finite prefix which cannot be extended to any valid, satisfying trace [13]. For instance, completing a set of CPS tasks in a specified order is a safety property, as is returning to a region periodically. We restrict to safety properties due to certain technical properties of monitors; however, these technical properties correspond to reasonable restrictions on the ability of any runtime assurance mechanism. Informally, if an LTL specification is not a safety property, then it contains a liveness condition requiring that some desirable property eventually becomes true. For example, reaching a goal region is a liveness property. Ensuring that a cyber-physical system does not violate a liveness property appears to be essentially equivalent to solving the controller synthesis problem, which we expressly attempt to avoid in this paper. We elaborate on the justification and implications of restricting to safety properties in Section 2.

For system specifications that are expressible as safety properties, we introduce the safety controller as a provably correct runtime assurance mechanism. The safety controller (Figure 1) has three fundamental components: a performance controller, a backup controller and an assurance mechanism. The assurance mechanism uses a monitor automaton to analyze a suggested performance control input and determine whether the resulting system trajectory is a bad prefix for the system specification. A fault flag from the assurance mechanism denotes a potentially dangerous future system state and triggers an input sequence which is guaranteed to keep the system safe for all time.

The backup controller is characterized by a subset of the product of the system and monitor state spaces where correct performance can be provided on an infinite time horizon; we refer to this subset as the high assurance region. Importantly, the assurance mechanism allows the performance controller to steer the system outside its known high assurance region, provided that the performance controller can demonstrate safety beforehand. This creates a trade-off between the a priori development of a backup controller and the real-time burden placed on the performance controller.

This paper is organized in the following way. We provide a discussion on the construction and application of monitor automata in Section 2. Section 3 presents the problem formulation and then introduces the safety controller architecture as a correct-by-construction runtime assurance mechanism for deterministic system models. This architecture is expanded in Section 4, to assure non-deterministic CPS system models. We provide a discussion on the trade-off between offline platform development and online assurance in Section 5, and the paper concludes with a final case study, provided in Section 6.

II Preliminaries on Monitoring for Linear Temporal Logic Properties

In this section, we introduce monitor automata as a runtime verification tool from automata based model checking.

II-A Monitor Construction in LTL3

To formally describe the execution of a CPS, we encode system events as atomic propositions; a sequence of events, or a word, therefore denotes the progression of the system through time. We use $AP$ to denote a set of atomic propositions, $\Sigma=2^{AP}$ to denote a finite alphabet, and $\Sigma^{*}$ and $\Sigma^{\omega}$ to denote the sets of finite and infinite system traces over $\Sigma$, respectively. System properties are specified in Linear Temporal Logic (LTL). For an in depth discussion of the LTL semantics, we refer the reader to [14] Section 2.1.

Consider an LTL specification $\varphi$ and a finite path fragment $w\in\Sigma^{*}$. Note that there may be no continuations of $w$ which satisfy $\varphi$, or equivalently, the system may have reached a state where it can no longer satisfy its specification under any possible future execution. We therefore introduce the definitions of bad and good prefixes in order to describe the set of finite words from which it is impossible to satisfy or violate a system specification.

Definition 1** (Good and Bad Prefixes).**

Consider a finite word $w_{1}\in\Sigma^{*}$ and an LTL property $\varphi$. $w_{1}$ is said to be a good prefix for $\varphi$ if $w_{1}w_{2}\models\varphi$ for all $w_{2}\in\Sigma^{\omega}$. Similarly, $w_{1}$ is said to be a bad prefix for $\varphi$ if $w_{1}w_{2}\not\models\varphi$ for all $w_{2}\in\Sigma^{\omega}$.

Further, we introduce the notion of a truth value, in order to classify whether a finite word is a good or bad prefix for $\varphi$.

Definition 2** (LTL3 Semantics, [2] Section 2.2).**

Let $w\in\Sigma^{*}$ denote a finite word. The truth value of an LTL3 formula $\varphi$ with respect to $w$, denoted $[w\models\varphi]$, is an element of $\mathbb{B}_{3}=\{\top,\perp,?\}$ defined as follows:

[TABLE]

Equivalently, the truth value $\varphi$ with respect to $w$ is true $``\top"$ if $w$ is a good prefix for $\varphi$, false $``\bot"$ if $w$ is a bad prefix for $\varphi$, and inconclusive $``?"$ otherwise.

Finally, we formalize the automata-based monitoring procedure for LTL3 (Definition 3). We refer the reader to [2] for a comprehensive discussion on monitor construction, and we provide a sample monitor construction in Figure 2.

Definition 3** (Monitors in LTL3).**

For a given property $\varphi$ a monitor automaton $\mathcal{M}^{\varphi}$ is a finite state machine that reads finite words $w\in\Sigma^{*}$ and outputs $[w\models\varphi]$.

Note that a monitor state with output $\top$ or $\perp$ will always be a trap state, as, for any LTL property, any continuation of a good/bad prefix for that property will also be a good/bad prefix. Consequently, a monitor $\mathcal{M}^{\varphi}$ will never have more than one state with output $\top$ and one state with output $\perp$ after minimization. We therefore use $q_{\top}$ and $q_{\perp}$ to denote monitor states with outputs $\top$ and $\perp$, respectively.

II-B Monitoring Safety Properties

Given a LTL property $\varphi$, the monitor automaton $\mathcal{M}^{\varphi}$ may not be able to reach all of $\mathbb{B}_{3}$. For instance, a monitor $\mathcal{M}^{\varphi}$ for $\varphi=\square a$, $\Sigma=\{\varnothing,\,a\}$, does not include a state $q_{\top}$. We therefore focus the scope of our study to LTL properties which guarantee certain monitor output behaviors. Specifically, we recall the definition of safety properties [15].

Definition 4** (Safety Property).**

An LTL property $\varphi_{safe}$ is said to be a safety property if all words which violate $\varphi_{safe}$ contain a bad prefix for $\varphi_{safe}$.

LTL safety properties make up a broad class of system specifications; for example, $\varphi=\square\varnothing\vee\bigcirc a$ (Figure 2) is a safety property in LTL. Furthermore, applying Definition 2.3, we can guarantee system safety by ensuring that the trace of every finite prefix trajectory does not contain a bad prefix for $\varphi_{safe}$. We formalize this result in Proposition 1.

Proposition 1**.**

An infinite word $w\in\Sigma^{\omega}$ satisfies $\varphi_{safe}$ if $[\hat{w}\models\varphi_{safe}]\neq\perp$ for all prefixes $\hat{w}\in\text{Pref}(w)$.

Note that a monitor $\mathcal{M}^{\varphi_{safe}}$, for a safety property $\varphi_{safe}$ not semantically equal to true, is guaranteed to have a state with output $\perp$. Moreover, we can verify system trajectories against $\varphi_{safe}$ by ensuring the system run over $\mathcal{M}^{\varphi_{safe}}$ never enters $q_{\bot}$.

III The Safety Controller Architecture

Here we apply monitor automata in a framework which enforces system objectives at runtime. For system objectives which are expressible as safety properties in LTL, we create a notion of system safety and describe a control architecture which is guaranteed to keep the system safe for all time. We refer to this control architecture as a safety controller. The safety controller has three fundamental components: a high-performance controller, a backup controller, and an assurance mechanism. The assurance mechanism is implemented through two algorithms which ensure system safety by continually choosing between the high-performance control input and the high-assurance control input.

III-A Preliminaries and Notation

Consider a discrete-time non-deterministic control system

[TABLE]

where, $x_{k}\in\mathcal{X}\subseteq\mathbb{R}^{n}$, $u_{k}\in\mathcal{U}\subseteq\mathbb{R}^{m}$ and $d_{k}\in\mathcal{D}\subset\mathbb{R}^{p}$ represent the system state, control input, and a non-deterministic bounded disturbance, at a time $k\in\mathbb{N}_{\geq 0}$, respectively. We make no assumptions on the stochastic properties of $d_{k}$ within $\mathcal{D}$, i.e. $d_{k}$ is not assumed to conform to any probability distribution.

Associated with the system (1) is a set of atomic propositions $AP$ and a labeling function $L:\mathcal{X}\rightarrow{}2^{AP}$. As before, let $\Sigma=2^{AP}$ denote a finite alphabet, and let $\Sigma^{*}$ and $\Sigma^{\omega}$ denote the sets of finite and infinite traces of the system (2) over $\Sigma$, respectively. Additionally, let $\varphi$ be property in LTL. We aim to construct a string of inputs $u_{0},u_{1},\cdots$ which, when fed to the system, will create a system trace $L(x_{0}\,x_{1}\cdots)\models\varphi$.

III-B Assurance Through Monitoring

We first consider the case with no disturbance $d$. After developing a general framework for approaching this deterministic formulation, we return to the non-deterministic setting of (1). To that end, consider a system

[TABLE]

[TABLE]

We aim to ensure that a safety property $\varphi\in\text{LTL}$ is satisfied over a (infinite) system trace. Following Proposition 1, we say that a finite system trajectory $x_{0},\cdots{},x_{k}$ is safe if $[L(x_{0}\cdots x_{k})\models\varphi]\in\{\top,?\}$, and unsafe if $[L(x_{0}\cdots x_{k})\models\varphi]=\;\perp$. A controller which is implemented on the system must first ensure the system stays safe before pursuing any auxiliary system objectives, such as enforcing optimality constraints or attempting to satisfy additional LTL properties.

Assume we have access to a controller which is claimed to be able to keep the system safe, while also possibly meeting some auxiliary system objective. We denote this a performance controller. Here, the performance controller is characterized by three assumptions:

Assumption III.1**.**

At each time $k$, the performance controller proposes a control input to be applied to the system.

Assumption III.2**.**

If requested, the performance controller can propose future inputs $\tilde{u}_{k},\cdots,\tilde{u}_{k+N_{max}}$, for some $N_{max}\in\mathbb{N}$, such that at time $j$, $k\leq j\leq k+N_{max}$ the performance controller intends to apply $\tilde{u}_{j}$ to the system. The performance controller is not obligated to use these control inputs at future time steps.

Assumption III.3**.**

The performance controller might bear faulty, i.e. applying the performance control input to (2) may eventually cause the system to violate its specification $\varphi$.

This definition of the performance controller is quite broad and encompasses general unverified feedback control laws. For example, a human operator, whose effectiveness cannot be verified a priori, can be thought of as a performance controller for a manned CPS. Despite the lack of global assurances, we assume that certain aspects of the performance control law make it preferable if safety can be determined beforehand. For example, the performance control may be designed to optimize some objective or achieve some auxiliary goal.

We additionally assume the existence of a controller which is known to satisfy the safety objective, but might be limited in abilities or performance. We denote this mechanism a backup controller, formalized next.

Definition 5** (Backup Controller and High Assurance Region).**

For a system of the form (1), a safety property $\varphi\in\text{LTL}$, and a corresponding monitor $\mathcal{M}^{\varphi}=(\Sigma,\,Q,\,q_{0},\,\delta,\,\lambda)$, let $S=\mathcal{X}\times Q$ denote the total state space of the combined system and monitor. A backup controller is characterized by a subset of the state space $S^{b}\subseteq S$ such that for any $(x,q)\in S^{b}$, there exists an infinite sequence of control inputs known to the backup controller such that the resulting infinite horizon system trace satisfies $\varphi$. $S^{b}$ is referred to as the high assurance region of the backup controller.

Let us fix a safety property $\varphi$, a corresponding monitor $\mathcal{M}^{\varphi}=(\Sigma,\,Q,\,q_{0},\,\delta,\,\lambda)$, a backup controller and a high assurance region $S^{b}$ for the remainder of this section. We recall the problem formulation: given a system of the form (2), generate a sequence of control inputs which, when fed to the system, will create a system trace which satisfies $\varphi$. Trivially, the system can be kept safe for all time by applying the backup control input to the system at each time step. This method of input generation, however, restricts the system to operating inside the high assurance region, and removes the possibility of reaching any auxiliary goals. For this reason, we interpret our problem formulation as follows: create a logical architecture which chooses whether to apply the performance control input or the backup control input to the system, at each time step, such that the resulting system trace satisfies $\varphi$. In this case, whenever possible, the chosen input should be that of the performance controller. We refer to this embedded decision logic as the assurance mechanism of the safety controller. Importantly, we give the system the ability to leave $S^{b}$ by applying the performance control input to the system in instances where the assurance mechanism can provide assurance in the form of a suggested input sequence, certifying that the system can return to the high assurance region once it has left. We justify this decision with Proposition 2.

Proposition 2**.**

Let $x_{0},\cdots,x_{k}$ denote a finite trajectory of system (1), and let $q_{0},\cdots,q_{k}$ be the corresponding run of the trajectory over $\mathcal{M}^{\varphi}$. If $(x_{k},q_{k})\in S^{b}$, then $L(x_{0}\cdots x_{k})$ is not a bad prefix for $\varphi$.

It follows from Proposition 2 that if the performance controller is able to suggest a path back to the high assurance region $S^{b}$ from every point along a system trajectory, then the performance control input is safe. We therefore create a procedure which takes an initial state $(x,q)\in\mathcal{X}\times Q$ and returns a finite sequence of control inputs $\mu_{r}$ such that:

$\mu_{r}=\varnothing$ signifies a fault in the performance controller, and 2. 2.

$\mu_{r}=u_{0},\cdots,u_{k}$ signifies that applying the sequence of control inputs will return the system to $S^{b}$.

For an initial system monitor state, we use the term recovery input sequence to denote such a sequence of control inputs which drive the system state into $S^{b}$.

We implement this procedure by calling Recovery$(x,q)$, provided in Algorithm 1. Succinctly, Recovery$(x,q)$ simulates the system dynamics using the current system monitor state and a non-empty sequence of suggested future performance control inputs; if the future system monitor state is contained in $S^{b}$, then the suggested input sequence is returned, and, if not, the null sequence is returned, signaling a system fault. Therefore, if the performance controller is not faulty, then the output of Algorithm 1 is a non-empty recovery input sequence for the current system monitor state.

We use Algorithm 1 to design a logical architecture for our safety controller as follows:

At each time $k$ the decision logic calls $\textsc{Recovery}(x_{k},q_{k})$ and stores the output in a variable $\mu_{r}$. 2. 2.

If $\mu_{r}$ is non-empty, then $u_{0}$ is applied to the system and $u_{1},\cdots,u_{j}$ is stored to memory. 3. 3.

If $\mu_{r}=\varnothing$ then the performance controller has suggested an input sequence that cannot be verified. The memorized recovery input sequence is applied to return the system to $S^{b}$, and the backup control input is then applied for all future time.

We implement this procedure through Algorithm 2. Algorithms 2 calls Algorithm 1 once per discrete time step, prompting the performance controller for a string of future inputs which steer the system to $S^{b}$. The performance controller will be considered functional if such a sequence is found. In the case that the performance controller is functional, the aforementioned procedure will create a finite series of inputs known to create a safe trajectory, but then only apply the first input to the system. In this way, the method resembles a model predictive control framework. Note that the assurance mechanism will need to simulate the system dynamics as many as $N_{max}+1$ times per discrete system timestep, therefore it is assumed that the assurance mechanism has the necessary functionality to perform these computations. Choosing control inputs using Algorithm 2 guarantees system safety for all time. We formalize this result in Theorem 1.

Theorem 1** (Runtime Assurance for Deterministic CPS).**

Let $\varphi\in\text{LTL}$ be a safety property, and let $w=L(x_{0}\,x_{1}\cdots)$ be the trace of an infinite trajectory resulting from a sequence of inputs chosen using Algorithm 2. If the system is initialized in the high assurance region, i.e. $(x_{0},q_{0})\in S^{b}$, then $w\models\varphi$.

In Section 4, we expand upon the results of this section in order to design a runtime assurance procedure for non-deterministic systems. To that end, we omit a proof for Theorem 1, with the knowledge that a later theorem encapsulates the findings of this section (Theorem 2).

IV Runtime Assurance for Non-Deterministic CPS

In practice, it is important to consider CPS models which account for potential system disturbances. We therefore turn our study toward assuring for non-deterministic systems.

IV-A Preliminaries and Notation

Reconsider the discrete-time non-deterministic CPS model (1). We retain the definitions of the system parameters $x$, $u$ and $d$, as well as the associated sets $AP$, $\Sigma$, $\Sigma^{*}$, and $\Sigma^{\omega}$, from Section 3. Additionally let $\varphi$ denote a mission objective that is a safety property in LTL.

IV-B Runtime Assurance in the Presence of Disturbances

We aim to extend our results from Section 3 to assure the non-deterministic system (1) against $\varphi$. To that end, we retain the definition of a backup controller from Section 2, now applied to (1), and we use the term performance controller to denote a controller which claims it will keep the system safe while also meeting some auxiliary objective. Here, we take the following assumption on the performance control law, replacing Assumptions III.2:

Assumption IV.1**.**

If requested, the performance controller can also propose a sequence $(X_{k},g_{k}),$ $\cdots,(X_{k+N_{max}},g_{k+N_{max}})$ of feedback control laws $g_{i}:\mathcal{X}\rightarrow\mathcal{U}$ and regions of the state space $X_{i}\subseteq\mathcal{X}$, such that at a future time $i$, the performance controller intends to choose its inputs using $g_{i}$ provided the current state of the system $x_{i}\in X_{i}$. The performance controller is not obligated to choose future inputs using these policies.

Note that Assumption IV.1 subsumes Assumption III.2 as a special case. In particular, the potential sequence of proposed inputs in Assumption III.2 can be considered a certain static feedback map $g_{i}$ such that $g_{i}(x)=u_{i}$ for all $x$.

For an initial state $(x_{0},q_{0})\in S$, and a sequence of feedback control laws $g_{0},g_{1},\cdots$, we denote the set of reachable states after $i$ steps by $R_{i}$, i.e.

[TABLE]

for all $i>1$. While calculating reachable sets can be computationally expensive, numerous methods exist to approximate reachable sets efficiently [16]. Therefore, let $\tilde{R}_{i}$ denote an over-approximation of $R_{i}$, i.e. $R_{i}\subseteq\tilde{R}_{i}$.

Using the approach described in Section 3 as a framework, we create a procedure which takes a current state $(x,q)\in S$ and returns a sequence of feedback control law $\gamma_{r}$ such that:

$\gamma_{r}=\varnothing$ signifies a fault in the performance controller, and 2. 2.

$\gamma_{r}=g_{0},\cdots,g_{k}$ signifies that choosing inputs according to the sequence of feedback control laws sequential will return the system to $S^{b}$.

We implement this procedure by calling a function RecoveryD$(x,q)$ (Algorithm 3). In the non-deterministic setting, we redefine the term recovery input sequence to denote a sequence of feedback control laws which is guaranteed to steer the system to a state contained in $S^{b}$. Therefore, if the performance controller is not faulty, then the output of Algorithm 3 can be thought of as a non-empty recovery input sequence for the current state.

We use Algorithm 3 to design a logical architecture for our safety controller as follows:

At each time $k$ the decision logic calls RecoveryD$(x_{k},q_{k})$ and stores the output in a variable $\gamma_{r}$. 2. 2.

If $\gamma_{r}$ is non-empty, then $g_{0}(x_{k})$ is applied to the system and $g_{1},\cdots,g_{j}$ is stored to memory. 3. 3.

If $\gamma_{r}=\varnothing$, then the performance controller has suggested an input sequence that cannot be verified. The memorized recovery input sequence is applied to return the system to $S^{b}$, and the backup control input is then applied for all future time.

This procedure is implemented using Algorithm 4.

Theorem 2** (Runtime Assurance for Non-Deterministic CPS).**

Let $\varphi\in\text{LTL}$ be a safety property, and let $w=L(x_{0}\,x_{1}\cdots)$ be the trace of an infinite trajectory resulting from a sequence of inputs chosen using Algorithm 4. If the system is initialized in the high assurance region, i.e. $(x_{0},q_{0})\in S^{b}$, then $w\models\varphi$.

Proof.

Let $(x_{0},q_{0})\in S^{b}$ be the initial system monitor state. Therefore $q_{0}\neq q_{\perp}$. The performance controller is prompted for a non-empty recovery input sequence $\gamma_{r}$ for the current state (Line 2, Line 7). If $\gamma_{r}=g_{0},\,\cdots,\,g_{N}$ is returned (Line 3), then the $u_{0}=g_{0}(x_{0})$ is passed to the system, which brings the system to a current state $(x_{1},\,q_{1})$, and $g_{1},\,\cdots,\,g_{N}$ is saved to memory as a recovery input sequence for $(x_{1},\,q_{1})$. The existence of a recovery input sequence for $(x_{1},\,q_{1})$ guarantees $q_{1}\neq q_{\perp}$. It follows inductively that if the performance controller is always able to supply a recovery input sequence for the current state, then $L(x_{0}\,x_{1}\cdots)\models\varphi$. If instead there exists a finite time $k$ such that the performance controller is unable to generate a recovery input sequence for $(x_{k},\,q_{k})$ then the previous recovery input sequence will be applied to the system and then the backup control input is applied for all time (Line 8 and 9). This forces the system to remain in $S^{b}$ indefinitely and therefore guarantees system safety by Proposition 2. ∎∎

Note that when $\mathcal{D}=\varnothing$, the non-deterministic system (1) is equivalent to the deterministic system (2). Therefore, Theorem 1 is a special case of Theorem 2.

V Classifying the Trade-off Between A Priori Development and Effectiveness

Here, we discuss the feasibility of designing and implementing a safety controller architecture. Specifically, we address the offline computation involved in constructing a backup controller and the computational complexity of the algorithms which run online in the assurance mechanism.

V-A Developing a Safety Controller Offline

Two steps are required to construct a safety controller from an LTL safety specification $\varphi$ and a given system model: the first step is to convert the system specification to a monitor automaton and the next step is to design a backup controller.

We refer the reader to [2] for a detailed discussion on monitor construction. In short, this process involves realizing two deterministic finite automata (DFAs) and then computing their minimal product automaton. There are well-defined procedures for constructing a DFA from an LTL specification, as well as procedures for computing product automata [13]. The resulting DFA is reduced to its minimal form by removing every unreachable state and every pair of non-distinguishable states. This procedure is implemented using Moore’s algorithm [17], which has an average complexity $O(n\cdot{}\text{log}(n))$ when minimizing a DFA with $n$ states. This procedure will only need to be performed once in the CPS development process.

A backup control law is developed by identifying a controlled invariant region of the system monitor state space $S^{b}\subseteq\mathcal{X}\times Q$, such that for all $(x,q)\in S^{b}$, $q\neq q_{\perp}$. This follows from Proposition 2, i.e. in order to ensure system safety the backup controller must only ensure the system trace never enters the false monitor state $q_{\perp}$. In order to compute such an invariant region of the system monitor state space, abstraction based methods are possible [14, 18].

V-B Online Computation for the Assurance Mechanism

Consider a CPS outfitted with a safety controller architecture. We would like to characterize the computational resources which will be necessary online for assurance.

First, we propose that Assumption III.2 (IV.2), which requires the performance controller to suggest potential future inputs, fits well with existing control architectures; for instance, all MPC controllers employ this functionality. Moreover, since the performance controller is assumed to be provided in advance of the safety controller construction process, we do not discuss the computational complexity of designing a performance controller for a given CPS. Instead, let us discuss the requisite online computation requirements of the assurance mechanism and the backup controller.

The assurance mechanism will call Algorithm 1 (or 3) once per discrete time step, in order to access the performance control input. Therefore, the assurance mechanism must have sufficient computational capabilities to over-approximate reachable system states at runtime. Reachable set computation is a very well-studied problem in the controls and hybrid systems literature, with numerous efficient algorithms. See [19, Chapter 29] for an overview.

V-C Discussion

The assurance mechanism will only ever apply a performance control input sequence if the set of reachable states resulting from that sequence is contained inside the high assurance region. There is, therefore, an intuitive trade-off between the a priori development of the assurance mechanism and the amount of computational resources which are necessary online. For example, the likelihood of finding a safe performance control input sequence is maximized for safety controllers with large, well developed, high assurance regions. Similarly, an assurance mechanism which computes tight approximations of reachable sets will be less likely to return a fault flag, in comparison to an assurance mechanism which uses conservative approximations. In general, therefore, developing a comprehensive backup control policy, will reduce the burden placed on the assurance mechanism at runtime. This constitutes a trade-off between the a priori development of the assurance mechanism and the effectiveness of the safety controller architecture.

Here we include some additional methods for increasing the capabilities of the assurance mechanism. In the instance that the system leaves $S^{b}$, with assurance from the performance controller, an assurance mechanism might choose to expand $S^{b}$ on the fly with the knowledge of the new system state and its corresponding recovery input sequence. As the high assurance region expands, the system will effectively learn how to stay safe in previously unverified product states, equivalently increasing system performance. Safe learning is an active research area in the controls and formal methods communities. One modern technique, referred to as shielding, enforces LTL safety properties in a run-time assurance framework [20]. Shields, however, only assure discrete-time discrete-state systems, whereas the safety controller architecture is applicable to systems with a continuous state space. Shielding also assumes a probabilistic system disturbance, which we expressly attempt to avoid in our construction. Additionally, in the instance that the performance controller is determined to be faulty, Algorithms 2 and 4 first apply the recovery input sequence to the system, forcing the system monitor trajectory to reenter $S^{b}$, and then pass the backup control input to the system for all time; an assurance mechanism may instead re-activate the preforming controller once $S^{b}$ is reached. In this case, the performance controller is certainly faulty and may again suggest an unsafe sequence of inputs at some-point in the future, however, even in this instance, the safety controller architecture will be able to assure the system against the mission objective.

VI Case Study: An Accelerating DeLorean

A safety controller architecture was implemented on a modified F1/10 race car (Figure 4(a)). F1/10 is an open-source 1/10 scale autonomous vehicle test-bed designed primarily for use by academic researchers [21].

VI-A System Characterization

When traveling along a straight line, the plant dynamics of the system conform to a non-deterministic discrete-time double integrator model. Here the system state at a time $k\in\mathbb{N}_{\geq 0}$, is described by the car’s position along the road $x(k)\in\mathbb{R}_{\geq 0}$ and the car’s forward velocity $v(k)\in\mathbb{R}_{\geq 0}$. Control inputs were suggested by a human operator, who chose the applied motor torque with a wireless Logitech Gamepad F710 controller (Figure 4(a)); this input is therefore proportional to the experienced acceleration. Additionally, a non-deterministic factor was included in the system model in order to encapsulate the effects of drag on the vehicle.

VI-B Generating a Safety Controller given a Mission Objective

Our mission objective is taken from the movie Back to the Future: when the car passes the clock tower, the car’s velocity must be greater than 2 meters per second. We give the car, hereafter referred to as a DeLorean, an initial position $(x_{0},v_{0})=(0,0)$, and arbitrarily place the clock tower a distance 2.54 meters from the origin.

Without an enforcement mechanism, the human operator has the ability to suggest an input sequence which causes the vehicle to pass the clock tower with inadequate speed, thus violating the mission objective. We therefore design an assurance mechanism to act as a filter between the the human operator and the plant, and ensure that the runtime performance of the DeLorean meets the mission objective.

We convert our system specification to an LTL safety property as follows. Let $AP=\{Tower,Fast\}$ be the set of events, where $Tower$ indicates that the DeLorean has driven past the clock tower, and $Fast$ indicates that the velocity of the DeLorean is greater than 2 m/s. The trace of a system trajectory is therefore given by the labeling function $L:\mathbb{R}^{2}\rightarrow 2^{AP}$

[TABLE]

In order to ensure that the DeLorean does not pass the clock tower with insufficient velocity, we enforce the LTL safety specification $\varphi=(\neg Tower)\>U\>(Tower\wedge Fast)$ whose monitor $\mathcal{M}^{\varphi}$ is provided in Figure 3. We take $S^{b}$ to be a triangular region of the state space from which the DeLorean can decelerate to zero velocity safely:

[TABLE]

In this case, if the DeLorean is in a current state $(x,v,q)\in S^{b}$, then the backup controller will suggest that the DeLorean brake such that the vehicle decelerates to a stop. A safety controller architecture is created by integrating Algorithms 3 and 4 into an assurance mechanism.

VI-C Case Study Implementation

We present the scenario where the vehicle driver, who initially suggested safe inputs, suggests an unsafe control policy (Figure 4(b)). Performance control inputs are passed to the system 250 milliseconds after the driver sent them via remote control; this lag-time allowed the assurance mechanism to analyze control inputs as though they were suggested as a string. The driver first suggested an input sequence that guaranteed the that DeLorean would satisfy the mission objective $\varphi$. This allows the DeLorean to leave $S^{b}$. At a future timestep, the driver suggests a control input sequence which allowed for the possibility that the DeLorean would violate $\varphi$. The assurance mechanism then applies the memorized recovery input sequence, and the DeLorean passes the clock tower with sufficient velocity.

VII Acknowledgements

The authors wish to thank Will Stuckey for his work with test-bed development.

VIII Conclusions

This paper introduces the safety controller as a runtime assurance mechanism for system objectives expressed in linear temporal logic. A case study is presented which details the construction and implementation of a safety controller on a non-deterministic cyber-physical system.