Synthesis of Admissible Shields

TL;DR

This paper introduces admissible shields for runtime safety enforcement in reactive systems, improving upon k-stabilizing shields by enabling collaboration with the system and handling failures during recovery, demonstrated in UAV mission planning.

Contribution

It proposes the concept of admissible shields, which are more flexible and capable than k-stabilizing shields, especially when such shields cannot be constructed.

Findings

Admissible shields can be generated for UAVs where k-stabilizing shields cannot.

They improve recovery times by collaborating with the system.

They handle system failures during recovery phases.

Abstract

Shield synthesis is an approach to enforce a set of safety-critical properties of a reactive system at runtime. A shield monitors the system and corrects any erroneous output values instantaneously. The shield deviates from the given outputs as little as it can and recovers to hand back control to the system as soon as possible. This paper takes its inspiration from a case study on mission planning for unmanned aerial vehicles (UAVs) in which k-stabilizing shields, which guarantee recovery in a finite time, could not be constructed. We introduce the notion of admissible shields, which improves k-stabilizing shields in two ways: (1) whereas k-stabilizing shields take an adversarial view on the system, admissible shields take a collaborative view. That is, if there is no shield that guarantees recovery within k steps regardless of system behavior, the admissible shield will attempt to work with the system to recover as soon as possible. (2) Admissible shields can handle system failures during the recovery phase. In our experimental results we show that for UAVs, we can generate admissible shields, even when k-stabilizing shields do not exist.

Figures

Tables

Table 1. Table 1 : δ u superscript 𝛿 𝑢 \delta^{u} of 𝒰 𝒰 \mathcal{U} of Example 5.0.1 .

	$\neg o_1\neg o_2$	$\neg o_1{o}_2$ or $o_1\neg o_2$	$o_1{o}_2$
{F}	{F}	{F,S}$↯$	{S}
{S}	{T}$↯$	{T}$↯$	{T}
{T}	{F}$↯$	{F}$↯$	{F}
{F,S}	{F}	{F,S,T}$↯$	{S,T}
{S,T}	{F,T}$↯$	{F,T}$↯$	{F,T}
{F,T}	{F}	{F,S,T}$↯$	{F,S}
{F,S,T}	{F}	{F,S,T}$↯$	{F,S,T}

Table 2. Table 2 : Results of m ​ a ​ p 8 𝑚 𝑎 subscript 𝑝 8 map_{8} and m ​ a ​ p 31 𝑚 𝑎 subscript 𝑝 31 map_{31} .

Example	Property	$\left|Q\right|$	$\left|I\right|$	$\left|O\right|$	$l$	Time [sec]
Map8	1	9	0	3	3	0.52
	1+4	12	0	3	3	1.2
	1+5a	46	1	3	4	6.2
	1+5b	32	1	3	3	7
	1+4+5a	55	1	3	4	17
	1+4+5b	36	1	3	3	12
Map31	1	32	0	5	6	122
Map31	1+2	32	0	5	6	143
Map31	1+2+3	34	0	5	6	183
Map31	1+2+3+4	38	0	5	6	238

Table 3. Table 3 : Results of m ​ a ​ p 15 𝑚 𝑎 subscript 𝑝 15 map_{15} .

Example	Property	$\left|Q\right|$	$\left|I\right|$	$\left|O\right|$	$l$	Time [sec]
Map15	1	16	0	4	5	12
	1+2	16	0	4	5	14
	1+2+3	19	0	4	5	19
	1+2+3+4	23	0	4	5	28
	1+5a	84	1	4	6	173
	1+5a+2	84	1	4	6	205
	1+5a+2+3	100	1	4	6	307
	1+5b	64	1	4	6	169
	1+5b+2	64	1	4	6	195
	1+6	115	1	4	7	690

Equations

$$\mathcal{S}(\overline{\sigma }\cdot ({\sigma }_I,{{\sigma }_O}^f)\cdot ({\overline{{\sigma }_I}}^{\prime }||{\overline{{\sigma }_O}}^{\prime })\cdot ({\overline{{\sigma }_I}}^{\prime \prime }||{\overline{{\sigma }_O}}^{\prime \prime }))=\overline{{\sigma }_O}\cdot {{\sigma }_O}^{\#}\cdot {\overline{{\sigma }_O}}^{\#}\cdot {\overline{{\sigma }_O}}^{\prime \prime }$$

$$(\overline{{\sigma }_I}||\overline{{\sigma }_O})\cdot ({\sigma }_I,{{\sigma }_O}^{\#})\cdot ({\overline{{\sigma }_I}}^{\prime }||{\overline{{\sigma }_O}}^{\#})\cdot ({\overline{{\sigma }_I}}^{\prime \prime }||{\overline{{\sigma }_O}}^{\prime \prime })\models \phi .$$

$$\mathcal{S}(\overline{\sigma }\cdot ({\sigma }_I,{{\sigma }_O}^f)\cdot ({\overline{{\sigma }_I}}^{\prime }||{\overline{{\sigma }_O}}^{\prime })\cdot ({\overline{{\sigma }_I}}^{\prime \prime }||{\overline{{\sigma }_O}}^{\prime \prime }))=\overline{{\sigma }_O}\cdot {{\sigma }_O}^{\#}\cdot {\overline{{\sigma }_O}}^{\#}\cdot {\overline{{\sigma }_O}}^{\prime \prime }$$

$$(\overline{{\sigma }_I}||\overline{{\sigma }_O})\cdot ({\sigma }_I,{{\sigma }_O}^{\#})\cdot ({\overline{{\sigma }_I}}^{\prime }||{\overline{{\sigma }_O}}^{\#})\cdot ({\overline{{\sigma }_I}}^{\prime \prime }||{\overline{{\sigma }_O}}^{\prime \prime })\models \phi .$$

$$\bigl{(}\delta^{u}[u,({\sigma_{I}},({\sigma_{O}},z))],\delta^{t}[t,({\sigma_{O}},{\sigma_{O}}^{\prime})],\delta[q,({\sigma_{I}},{\sigma_{O}}^{\prime})]\bigr{)},$$

Full text

1 Introduction

Technological advances enable the development of increasingly sophisticated systems. Smaller and faster microprocessors, wireless networking, and new theoretical results in areas such as machine learning and intelligent control are paving the way for transformative technologies across a variety of domains – self-driving cars that have the potential to reduce accidents, traffic, energy consumption, and pollution; and unmanned systems that can safely and efficiently operate on land, under water, in the air, and in space. However, in each of these domains, concerns about safety are being raised [16],[7]. Specifically, there is a concern that due to the complexity of such systems, traditional test and evaluation approaches will not be sufficient for finding errors, and alternative approaches such as those provided by formal methods are needed [17].

Formal methods are often used to verify systems at design time, but this is not always realistic. Some systems are simply too large to be fully verified. Others, especially systems that operate in rich dynamic environments or those that continuously adapt their behavior through methods such as machine learning, cannot be fully modeled at design time. Still others may incorporate components that have not been previously verified and cannot be modeled, e.g., proprietary components or pre-compiled code libraries.

Also, even systems that have been fully verified at design time may be subject to external faults such as those introduced by unexpected hardware failures or human inputs. One way to address this issue is to model nondeterministic behaviours (such as faults) as disturbances, and verify the system with respect to this disturbance model [18]. However, it is impossible to model all potential unexpected behavior at design time.

An alternative in such cases is to perform runtime verification to detect violations of a set of specified properties while a system is executing [14]. An extension of this idea is to perform runtime enforcement of specified properties, in which violations are not only detected but also overwritten in a way that specified properties are maintained.

A general approach for runtime enforcement of specified properties is shield synthesis, in which a shield monitors the system and instantaneously overwrites incorrect outputs. A shield must ensure both correctness, i.e., it corrects system outputs such that all properties are always satisfied, as well as minimum deviation, i.e., it deviates from system outputs only if necessary and as rarely as possible. The latter requirement is important because the system may satisfy additional noncritical properties that are not considered by the shield but should be retained as much as possible.

Bloem et al. [4] proposed the notion of $k$-stabilizing shields. Since we are given a safety specification, we can identify wrong outputs, that is, outputs after which the specification is violated (more precisely: after which the environment can force the specification to be violated). A wrong trace is then a trace that ends in a wrong output. The idea of shields is that they may modify the outputs so that the specification always holds, but that such deviations last for at most $k$ consecutive steps after a wrong output. If a second violation happens during the $k$-step recovery phase, the shield enters a mode where it only enforces correctness, but no longer minimizes the deviation. This proposed approach has two limitations with significant impact in practice. (1) The $k$-stabilizing shield synthesis problem is unrealizable for many safety-critical systems, because a finite number of deviations cannot be guaranteed. (2) $k$-stabilizing shields make the assumption that there are no further system errors during the recovery phase.

In this paper, we introduce admissible shields, which overcome the two issues of $k$-stabilizing shields. To address shortcoming (1), we guarantee the following: (a) Admissible shields are subgame optimal. That is, for any wrong trace, if there is a finite number $k$ of steps within which the recovery phase can be guaranteed to end, the shield will always achieve this. (b) The shield is admissible, that is, if there is no such number $k$, it always picks a deviation that is optimal in that it ends the recovery phase as soon as possible for some possible future inputs. (This is defined in more detail below.) As a result, admissible shields work well in settings in which finite recovery can not be guaranteed, because they guarantee correctness and may well end the recovery period if the system does not pick adversarial outputs. To address shortcoming (2), admissible shields allow arbitrary failure frequencies and in particular failures that arrive during recovery, without losing the ability to recover.

As a second contribution, we demonstrate the use of admissible shields through a case study involving mission planning for an unmanned aerial vehicle (UAV). Manually creating and executing mission plans that meet mission objectives while addressing all possible contingencies is a complex and error-prone task. Therefore, having a shield that changes the mission only if absolutely necessary to enforce certain safety properties has the potential to lower the burden on human operators, and ensures safety during mission execution. We show that admissible shields are applicable in this setting, whereas $k$-stabilizing shields are not.

Related Work: Our work builds on synthesis of reactive systems [20], [3] and reactive mission plans [9] from formal specifications, and our method is related to synthesis of robust [1] and error-resilient [10] systems. However, our approach differs in that we do not synthesize an entire system, but rather a shield that considers only a small set of properties and corrects the output of the system at runtime. Li et al. [15] focused on the problem of synthesizing a semi-autonomous controller that expects occasional human intervention for correct operation. A human-in-the-loop controller monitors past and current information about the system and its environment. The controller invokes the human operator only when it is necessary, but as soon as a specification is violated ahead of time, such that the human operator has sufficient time to respond. Similarly, our shields monitor the behavior of systems at run time, and interfere as little as possible. Our work relates to more general work on runtime enforcement of properties [12], but shield synthesis [4] is the first appropriative work for reactive systems, since shields act on erroneous system outputs immediately without delay. While [4] focuses on shield synthesis for systems assumed to make no more than one error every $k$ steps, this work assumes only that systems generally have cooperative behavior with respect to the shield, i.e., the shield ensures a finite number of deviations if the system chooses certain outputs. This is similar in concept to cooperative synthesis as considered in [2], in which a synthesized system has to satisfy a set of properties (called guarantees) only if certain environment assumptions hold. The authors present a synthesis procedure that maximizes the cooperation between system and environment for satisfying both guarantees and assumptions as far as possible.

Outline: In what follows, we begin in Section 2 by motivating the need for admissible shields through a case study involving mission planning for a UAV. In Sections 3, 4, 5, we define preliminary concepts, review the general shield synthesis framework, and describe our approach for synthesizing admissible shields. Section 6 provides experimental results, and Section 7 concludes.

2 Motivating Example

In this section, we apply shields on a scenario in which a UAV must maintain certain properties while performing a surveillance mission in a dynamic environment. We show how a shield can be used to enforce the desired properties, where a human operator in conjunction with a lower-level autonomous planner is considered as the reactive system that sends commands to the UAV’s autopilot. We discuss how we would intuitively want a shield to behave in such a situation. We show that the admissible shields provide the desired behaviors and address the limitations of $k$-stabilizing shields.

To begin, note that a common UAV control architecture consists of a ground control station that communicates with an autopilot onboard the UAV [5]. The ground control station receives and displays updates from the autopilot on the UAV’s state, including position, heading, airspeed, battery level, and sensor imagery. It can also send commands to the UAV’s autopilot, such as waypoints to fly to. A human operator can then use the ground control station to plan waypoint-based routes for the UAV, possibly making modifications during mission execution to respond to events observed through the UAV’s sensors. However, mission planning and execution can be very workload intensive, especially when operators are expected to control multiple UAVs simultaneously [8]. To address this issue, methods for UAV command and control have been explored in which operators issue high-level commands, and automation carries out low-level execution details.

Several errors can occur in this type of human-automation paradigm [6]. For instance, in issuing high-level commands to the low-level planner, a human operator might neglect required safety properties due to high workload, fatigue, or an incomplete understanding of exactly how the autonomous planner might execute the command. The planner might also neglect these safety properties either because of software errors or by design. Waypoint commands issued by the operator or planner could also be corrupted by software that translates waypoint messages between ground station and autopilot specific formats or during transmission over the communication link.

As the mission unfolds, waypoint commands will be sent periodically to the autopilot. If a waypoint that violates the properties is received, a shield that monitors the system inputs and can overwrite the waypoint outputs to the autopilot would be able to make corrections to ensure the satisfaction of the desired properties.

Consider the mission map in Fig. 1 [13], which contains three tall buildings (illustrated as blue blocks), over which a UAV should not attempt to fly. It also includes two unattended ground sensors (UGS) that provide data on possible nearby targets, one at location $loc_{1}$ and one at $loc_{x}$, as well as two locations of interest, $loc_{y}$ and $loc_{z}$. The UAV can monitor $loc_{x}$, $loc_{y}$, and $loc_{z}$ from several nearby vantage points. The map also contains a restricted operating zone (ROZ), illustrated with a red box, in which flight might be dangerous, and the path of a possible adversary that should be avoided (the pink dashed line). Inside the communication relay region (large green area), communication links are highly reliable. Outside this region, communication relies on relay points with lower reliability.

Given this scenario, properties of interest include:

Connected waypoints. The UAV is only allowed to fly to directly connected waypoints. 2. 2.

No communication. The UAV is not allowed to stay in a location with reduced communication reliability. 3. 3.

Restricted operating zones. The UAV has to leave a ROZ within 2 time steps. 4. 4.

Detected by an adversary. Locations on the adversary’s path cannot be visited more than once over any window of 3 time steps. 5. 5.

UGS. If a UGS reports a possible nearby target, the UAV should visit a respective waypoint within 7 steps (for $UGS_{1}$ visit $loc_{1}$, for $UGS_{2}$ visit $loc_{5}$, $loc_{6}$, $loc_{7}$, or $loc_{8}$). 6. 6.

Go home. Once the UAV’s battery is low, it should return to a designated landing site at $loc_{14}$ within 10 time steps.

The task of the shield is to ensure these properties during operation. In this setting, the operator in conjunction with a lower-level planner acts as a reactive system that responds to mission-relevant inputs; in this case data from the UGSs and a signal indicating whether the battery is low. In each step, the next waypoint is sent to the autopilot, which is encoded in a bit representation via outputs $l_{4}$, $l_{3}$, $l_{2}$, and $l_{1}$. We attach the shield as shown in Fig. 2. The shield monitors mission inputs and waypoint outputs, correcting outputs immediately if a violation of the safety properties becomes unavoidable.

We represent each of the properties by a safety automaton, the product of which serves as the shield specification. Fig. 3 models the “connected waypoints” property, where each state represents a waypoint with the same number. Edges are labeled by the values of the variables $l_{4}\dots l_{1}$. For example, the edge leading from state $s_{5}$ to state $s_{6}$ is labeled by $\neg l_{4}l_{3}l_{2}\neg l_{1}$. For clarity, we drop the labels of edges in Fig. 3. The automaton also includes an error state, which is not shown. Missing edges lead to this error state, denoting forbidden situations.

How should a shield behave in this scenario? If the human operator wants to monitor a location in a ROZ, he or she would like to simply command the UAV to “monitor the location in the ROZ and stay there”, with the planner handling the execution details. If the planner cannot do this while meeting all the safety properties, it is appropriate for the shield to revise its outputs. Yet, the operator would still expect his or her commands to be followed to the maximum extent possible, leaving the ROZ when necessary and returning whenever possible. Thus, the shield should minimize deviations from the operator’s directives as executed by the planner.

Using a $k$-stabilizing shield. As a concrete example, assume the UAV is currently at $loc_{3}$, and the operator commands it to monitor $loc_{12}$. The planner then sends commands to fly to $loc_{11}$ then $loc_{12}$, which are accepted by the shield. The planner then sends a command to loiter at $loc_{12}$, but the shield must overwrite it to maintain Property 3, which requires the UAV to leave the ROZ within two time steps. The shield instead commands the UAV to go to $loc_{15}$. Suppose the operator then commands the UAV to fly to $loc_{13}$, while the planner is still issuing commands as if the UAV is at $loc_{12}$. The planner then commands the UAV to fly to $loc_{13}$, but since the actual UAV cannot fly from $loc_{15}$ to $loc_{13}$ directly, the shield directs the UAV to $loc_{14}$ on its way to $loc_{15}$. The operator might then respond to a change in the mission and command the UAV fly back to $loc_{12}$, and the shield again deviates from the route assumed by the planner, and directs the UAV back to $loc_{15}$, and so on. Therefore, a single specification violation can lead to an infinitely long deviation between the UAV’s actual position and the UAV’s assumed position. A $k$-stabilizing shield is allowed to deviate from the planner’s commands for at most $k$ consecutive time steps. Hence, no $k$-stabilizing shield exists.

Using an admissible shield. Recall the situation in which the shield caused the actual position of the UAV to “fall behind” the position assumed by the planner, so that the next waypoint the planner issues is two or more steps away from the UAV’s current waypoint position. The shield should then implement a best-effort strategy to “synchronize” the UAV’s actual position with that assumed by the planner. Though this cannot be guaranteed, the operator and planner are not adversarial towards the shield, so it will likely be possible to achieve this re-synchronization, for instance when the UAV goes back to a previous waypoint or remains at the current waypoint for several steps. This possibility motivates the concept of an admissible shield. Assume that the actual position of the UAV is $loc_{14}$ and the its assumed position is $loc_{13}$. If the operator commands the UAV to loiter at $loc_{13}$, the shield will be able to catch up with the state assumed by the planner and to end the deviation by the next specification violation.

3 Preliminaries

We denote the Boolean domain by $\mathbb{B}=\{\mathsf{true},\mathsf{false}\}$, the set of natural numbers by $\mathbb{N}$, and abbreviate $\mathbb{N}\cup\{\infty\}$ by $\mathbb{N}^{\infty}$. We consider a reactive system with a finite set $I=\{i_{1},\ldots,i_{m}\}$ of Boolean inputs and a finite set $O=\{o_{1},\ldots,o_{n}\}$ of Boolean outputs. The input alphabet is $\Sigma_{I}=2^{I}$, the output alphabet is $\Sigma_{O}=2^{O}$, and $\Sigma=\Sigma_{I}\times\Sigma_{O}$. The set of finite (infinite) words over $\Sigma$ is denoted by $\Sigma^{*}$ ($\Sigma^{\omega}$), and $\Sigma^{\infty}=\Sigma^{*}\cup\Sigma^{\omega}$. We will also refer to words as (execution) traces. We write $|\overline{\sigma}|$ for the length of a trace $\overline{\sigma}\in\Sigma^{*}$. For ${\overline{\sigma_{I}}}=x_{0}x_{1}\ldots\in\Sigma_{I}^{\infty}$ and ${\overline{\sigma_{O}}}=y_{0}y_{1}\ldots\in\Sigma_{O}^{\infty}$, we write ${\overline{\sigma_{I}}}||{\overline{\sigma_{O}}}$ for the composition $(x_{0},y_{0})(x_{1},y_{1})\ldots\in\Sigma^{\infty}$. A set $L\subseteq\Sigma^{\infty}$ of words is called a language. We denote the set of all languages as $\mathcal{L}=2^{\Sigma^{\infty}}$.

Reactive Systems. A Mealy machine (reactive system, design) is a 6-tuple $\mathcal{D}=(Q,q_{0},\\ \Sigma_{I},\Sigma_{O},\delta,\lambda)$, where $Q$ is a finite set of states, $q_{0}\in Q$ is the initial state, $\delta:Q\times\Sigma_{I}\rightarrow Q$ is a complete transition function, and $\lambda:Q\times\Sigma_{I}\rightarrow\Sigma_{O}$ is a complete output function. Given the input trace ${\overline{\sigma_{I}}}=x_{0}x_{1}\ldots\in\Sigma_{I}^{\infty}$, the system $\mathcal{D}$ produces the output trace ${\overline{\sigma_{O}}}=\mathcal{D}({\overline{\sigma_{I}}})=\lambda(q_{0},x_{0})\lambda(q_{1},x_{1})\ldots\in\Sigma_{O}^{\infty}$, where $q_{i+1}=\delta(q_{i},x_{i})$ for all $i\geq 0$. The set of words produced by $\mathcal{D}$ is denoted $L(\mathcal{D})=\{{\overline{\sigma_{I}}}||{\overline{\sigma_{O}}}\in\Sigma^{\infty}\mid\mathcal{D}({\overline{\sigma_{I}}})={\overline{\sigma_{O}}}\}$.

Let $\mathcal{D}=(Q,q_{0},\Sigma_{I},\Sigma_{O},\delta,\lambda)$ and $\mathcal{D}^{\prime}=(Q^{\prime},q_{0}^{\prime},\Sigma,\Sigma_{O},\delta^{\prime},\lambda^{\prime})$ be reactive systems. A serial composition of $\mathcal{D}$ and $\mathcal{D}^{\prime}$ is realized if the input and output of $\mathcal{D}$ are fed to $\mathcal{D}^{\prime}$. We denote such composition as $\mathcal{D}\circ\mathcal{D}^{\prime}=(\hat{Q},\hat{q_{0}},\Sigma_{I},\Sigma_{O},\hat{\delta},\hat{\lambda})$, where $\hat{Q}=Q\times Q^{\prime}$, $\hat{q_{0}}=(q_{0},q_{0}^{\prime})$, $\hat{\delta}((q,q^{\prime}),{\sigma_{I}})=(\delta(q,{\sigma_{I}}),\delta^{\prime}(q^{\prime},({\sigma_{I}},\lambda(q,{\sigma_{I}}))))$, and $\hat{\lambda}((q,q^{\prime}),{\sigma_{I}})=\lambda^{\prime}(q^{\prime},({\sigma_{I}},\lambda(q,{\sigma_{I}})))$.

Specifications. A specification $\varphi$ is a set $L(\varphi)\subseteq\Sigma^{\infty}$ of allowed traces. $\mathcal{D}$ realizes $\varphi$, denoted by $\mathcal{D}\models\varphi$, iff $L(\mathcal{D})\subseteq L(\varphi)$. A specification $\varphi$ is realizable if there exists a design $\mathcal{D}$ that realizes it. A safety specification $\varphi^{s}$ is represented by an automaton $\varphi^{s}=(Q,q_{0},\Sigma,\delta,F)$, where $\Sigma=\Sigma_{I}\cup\Sigma_{O}$, $\delta:Q\times\Sigma\rightarrow Q$, and $F\subseteq Q$ is a set of safe states. The run induced by trace $\overline{\sigma}=\sigma_{0}\sigma_{1}\ldots\in\Sigma^{\infty}$ is the state sequence $\overline{q}=q_{0}q_{1}\ldots$ such that $q_{i+1}=\delta(q_{i},\sigma_{i})$; the run is accepting if $\forall i\geq 0\operatorname{\mathbin{.}}q_{i}\in F$. Trace $\overline{\sigma}$ (of a design $\mathcal{D}$) satisfies $\varphi^{s}$ if the induced run is accepting. The language $L(\varphi^{s})$ is the set of all traces satisfying $\varphi^{s}$.

Games. A (2-player, alternating) game is a tuple $\mathcal{G}=(G,g_{0},\Sigma_{I},\Sigma_{O},\delta,\mathsf{win})$, where $G$ is a finite set of game states, $g_{0}\in G$ is the initial state, $\delta:G\times\Sigma_{I}\times\Sigma_{O}\rightarrow G$ is a complete transition function, and $\mathsf{win}:G^{\omega}\rightarrow\mathbb{B}$ is a winning condition. The game is played by two players: the system and the environment. In every state $g\in G$ (starting with $g_{0}$), the environment first chooses an input letter ${\sigma_{I}}\in\Sigma_{I}$, and then the system chooses some output letter ${\sigma_{O}}\in\Sigma_{O}$. This defines the next state $g^{\prime}=\delta(g,{\sigma_{I}},{\sigma_{O}})$, and so on. Thus, a (finite or infinite) word over $\Sigma$ results in a (finite or infinite) play, a sequence $\overline{g}=g_{0}g_{1}\ldots$ of game states. A play is won by the system iff $\mathsf{win}(\overline{g})$ is $\mathsf{true}$. A safety game defines $\mathsf{win}$ via a set $F^{s}\subseteq G$ of safe states: $\mathsf{win}(g_{0}g_{1}\ldots)$ is $\mathsf{true}$ iff $\forall i\geq 0\operatorname{\mathbin{.}}g_{i}\in F^{s}$, i.e., if only safe states are visited. Let $\inf(\overline{g})$ denote the states that occur infinitely often in $\overline{g}$. A Büchi game defines $\mathsf{win}$ via a set $F^{b}\subseteq G$ of accepting states: $\mathsf{win}(\overline{g})$ is $\mathsf{true}$ iff $\inf(\overline{g})\cap F^{b}\neq\emptyset$.

It is easy to transform a safety specification into a safety game such that a trace satisfies the specification iff the corresponding play is won. Given a safety specification $\varphi^{s}$. A finite trace $\overline{\sigma}\in\Sigma^{*}$ is wrong, if the corresponding play is not won, i.e., if there is no way for the system to guarantee that any extension of the trace satisfies the specification. An output is called wrong, if it makes a trace wrong; i.e., given $\varphi^{s}$, a trace $\overline{\sigma}\in\Sigma^{*}$ an input ${\sigma_{I}}\in\Sigma_{I}$, and an output ${\sigma_{O}}\in\Sigma_{O}$, ${\sigma_{O}}$ is wrong iff $\overline{\sigma}$ is not wrong, but $\overline{\sigma}\cdot({\sigma_{I}},{\sigma_{O}})$ is.

A deterministic (memoryless) strategy for the environment is a function $\rho_{e}:G\rightarrow\Sigma_{I}$. A deterministic (memoryless) strategy for the system is a function $\rho_{s}:G\times\Sigma_{I}\rightarrow\Sigma_{O}$. A strategy $\rho_{s}$ is winning for the system, if for all strategies $\rho_{e}$ of the environment the play $\overline{g}$ that is constructed when defining the outputs using $\rho_{e}$ and $\rho_{s}$ satisfies $\mathsf{win}(\overline{g})$. The winning region $W$ is the set of states from which a winning strategy exists. A strategy is cooperatively winning if there exists a strategy $\rho_{e}$ and $\rho_{s}$, such that the play $\overline{g}$ constructed by $\rho_{e}$ and $\rho_{s}$ satisfies $\mathsf{win}(\overline{g})$.

For a Büchi game $\mathcal{G}$ with accepting states $F^{b}$, consider a strategy $\rho_{e}$ of the environment, a strategy $\rho_{s}$ of the system, and a state $g\in G$. We set the distance $dist(g,\rho_{e},\rho_{s})=k$, if the play $\overline{g}$ defined by $\rho_{e}$ and $\rho_{s}$ reaches from $g$ an accepting state that occurs infinitely often in $\overline{g}$ in $k$ steps. If no such state is visited, we set $dist(g,\rho_{e},\rho_{s})=\infty$. Given two strategies $\rho_{s}$ and $\rho_{s}^{\prime}$ of the system, we say that $\rho_{s}^{\prime}$ dominates $\rho_{s}$ if: (i) for all $\rho_{e}$ and all $g\in G$, $dist(g,\rho_{e},\rho_{s}^{\prime})\leq dist(g,\rho_{e},\rho_{s})$ , and (ii) there exists $\rho_{e}$ and $g\in G$ such that $dist(g,\rho_{e},\rho_{s}^{\prime})<dist(g,\rho_{e},\rho_{s})$.

A strategy is admissible if there is no strategy that dominates it.

4 Admissible Shields

Bloem et al. [4] presented the general framework for shield synthesis. A shield has two main properties: (i) For any design, a shield ensures correctness with respect to a specification. (ii) A shield ensures minimal deviation. We revisit these properties in Sec. 4.1. The definition of minimum deviation is designed to be flexible and different notions of minimum deviation can be realized. $k$-stabilizing shields represent one concrete realization. In Sec. 4.2, we present a new realization of the minimum deviation property resulting in admissible shields.

4.1 Definition of Shields

A shield reads the input and output of a design as shown in Fig. 2. We then address the two properties, correctness and minimum deviation, to be ensured by a shield.

The Correctness Property. With correctness we refer to the property that the shield corrects any design’s output such that a given safety specification is satisfied. Formally, let $\varphi$ be a safety specification and $\mathcal{S}=(Q^{\prime},q_{0}^{\prime},\Sigma,\Sigma_{O},\delta^{\prime},\lambda^{\prime})$ be a Mealy machine. We say that $\mathcal{S}$ ensures correctness if for any design $\mathcal{D}=(Q,q_{0},\Sigma_{I},\Sigma_{O},\delta,\lambda)$, it holds that $(\mathcal{D}\circ\mathcal{S})\models\varphi$.

Since a shield must work for any design, the synthesis procedure does not need to consider the design’s implementation. This property is crucial because the design may be unknown or too complex to analyze. On the other hand, the design may satisfy additional (noncritical) specifications that are not specified in $\varphi$ but should be retained as much as possible.

The Minimum Deviation Property. Minimum deviation requires a shield to deviate only if necessary, and as infrequently as possible. To ensure minimum deviation, a shield can only deviate from the design if a property violation becomes unavoidable. Given a safety specification $\varphi$, a Mealy machine $\mathcal{S}$ does not deviate unnecessarily if for any design $\mathcal{D}$ and any trace ${\overline{\sigma_{I}}}||{\overline{\sigma_{O}}}$ that is not wrong, we have that $\mathcal{S}({\overline{\sigma_{I}}}||{\overline{\sigma_{O}}})={\overline{\sigma_{O}}}$. In other words, if $\mathcal{D}$ does not violate $\varphi$, $\mathcal{S}$ keeps the output of $\mathcal{D}$ intact.

A Mealy machine $\mathcal{S}$ is a shield if $\mathcal{S}$ ensures correctness and does not deviate unnecessarily.

Ideally, shields end phases of deviations as soon as possible, recovering quickly. This property leaves room for interpretation. Different types of shields differentiate on how this property is realized.

4.2 Defining Admissible Shields

In this section we define admissible shields using their speed of recovery. We distinguish between two situations. In states of the design in which a finite number $k$ of deviations can be guaranteed, an admissible shield takes an adversarial view on the design: it guarantees recovery within $k$ steps regardless of system behavior, for the smallest $k$ possible. In these states, the strategy of an admissible shield conforms to the strategy of $k$-stabilizing shield. In all other states, admissible shields take a collaborative view: the admissible shield will attempt to work with the design to recover as soon as possible. In particular, an admissible shield plays an admissible strategy, that is, a strategy that cannot be beaten in recovery speed if the design acts cooperatively.

We will now define admissible shields. For failures of the system that are corrected by the shield, we consider four phases:

The innocent phase consisting of inputs ${\overline{\sigma_{I}}}$ and outputs ${\overline{\sigma_{O}}}$, in which no failure occurs; i.e., $({\overline{\sigma_{I}}}||{\overline{\sigma_{O}}})\models\varphi$. 2. 2.

The misstep phase consisting of a input ${\sigma_{I}}$ and a wrong output ${\sigma_{O}}^{f}$; i.e., $({\overline{\sigma_{I}}}||{\overline{\sigma_{O}}})\cdot({\sigma_{I}},{\sigma_{O}}^{f})\not\models\varphi$. 3. 3.

The deviation phase consisting of inputs ${\overline{\sigma_{I}}}^{\prime}$ and outputs ${\overline{\sigma_{O}}}^{\prime}$ in which the shield is allowed to deviate, and for a correct output ${\sigma_{O}}^{c}$ we have $({\overline{\sigma_{I}}}||{\overline{\sigma_{O}}})\cdot({\sigma_{I}},{\sigma_{O}}^{c})\cdot({\overline{\sigma_{I}}}^{\prime}||{\overline{\sigma_{O}}}^{\prime})\models\varphi$. 4. 4.

The final phase consisting ${\overline{\sigma_{I}}}^{\prime\prime}$ and ${\overline{\sigma_{O}}}^{\prime\prime}$ in which the shield does not deviate, and $({\overline{\sigma_{I}}}||{\overline{\sigma_{O}}})\cdot({\sigma_{I}},{\sigma_{O}}^{c})\cdot({\overline{\sigma_{I}}}^{\prime}||{\overline{\sigma_{O}}}^{\prime})\cdot({\overline{\sigma_{I}}}^{\prime\prime}||{\overline{\sigma_{O}}}^{\prime\prime})\models\varphi$.

Adversely $k$-stabilizing shields have a deviation phase of length at most $k$.

Definition 1

A shield $\mathcal{S}$ adversely $k$-stabilizes a trace $\overline{\sigma}={\overline{\sigma_{I}}}||{\overline{\sigma_{O}}}\in\Sigma^{*}$, if for any input ${\sigma_{I}}\in\Sigma_{I}$ and any wrong output ${\sigma_{O}}^{f}\in\Sigma_{O}$, for any correct output ${\sigma_{O}}^{c}\in\Sigma_{O}$ and for any correct trace ${\overline{\sigma_{I}}}^{\prime}||{\overline{\sigma_{O}}}^{\prime}\in\Sigma^{k}$ there exists a trace ${\sigma_{O}}^{\#}{\overline{\sigma_{O}}}^{\#}\in\Sigma_{O}^{k+1}$ such that for any trace ${\overline{\sigma_{I}}}^{\prime\prime}||{\overline{\sigma_{O}}}^{\prime\prime}\in\Sigma^{\omega}$ such that $({\overline{\sigma_{I}}}||{\overline{\sigma_{O}}})\cdot({\sigma_{I}},{\sigma_{O}}^{c})\cdot({\overline{\sigma_{I}}}^{\prime}||{\overline{\sigma_{O}}}^{\prime})\cdot({\overline{\sigma_{I}}}^{\prime\prime}||{\overline{\sigma_{O}}}^{\prime\prime})\models\varphi$, we have

[TABLE]

and

[TABLE]

Note that it is not always possible to adversely $k$-stabilize a shield for a given $k$ or even for any $k$.

Definition 2 (Adversely $k$-Stabilizing Shields

[4])

A shield $\mathcal{S}$ is adversely $k$-stabilizing if it adversely $k$-stabilies any finite trace.

An adversely $k$-stabilizing shield guarantees to end deviations after at most $k$ steps and produces a correct trace under the assumption that the failure of the design consists of a transmission error in the sense that the wrong letter is substituted for a correct one. We use the term adversely to emphasize that finitely long deviations are guaranteed for any future inputs and outputs of the design.

Definition 3 (Adversely Subgame Optimal Shield)

A shield $\mathcal{S}$ is adversely subgame optimal if for any trace $\overline{\sigma}\in\Sigma^{*}$, $\mathcal{S}$ adversely $k-$stabilizes $\overline{\sigma}$ and there exists no shield that adversely $l$-stabilizes $\overline{\sigma}$ for any $l<k$.

An adversely subgame optimal shield $\mathcal{S}$ guarantees to deviate in response to an error for at most $k$ time steps, for the smallest $k$ possible.

Definition 4

A shield $\mathcal{S}$ collaboratively $k$-stabilizes a trace $\overline{\sigma}={\overline{\sigma_{I}}}||{\overline{\sigma_{O}}}\in\Sigma^{*}$, if for any input ${\sigma_{I}}\in\Sigma_{I}$ and any wrong output ${\sigma_{O}}^{f}\in\Sigma_{O}$, there exists a correct output ${\sigma_{O}}^{c}\in\Sigma_{O}$, a correct trace ${\overline{\sigma_{I}}}^{\prime}||{\overline{\sigma_{O}}}^{\prime}\in\Sigma^{k}$, and a trace ${\sigma_{O}}^{\#}{\overline{\sigma_{O}}}^{\#}\in\Sigma_{O}^{k+1}$ such that for any trace ${\overline{\sigma_{I}}}^{\prime\prime}||{\overline{\sigma_{O}}}^{\prime\prime}\in\Sigma^{\omega}$ such that $({\overline{\sigma_{I}}}||{\overline{\sigma_{O}}})\cdot({\sigma_{I}},{\sigma_{O}}^{c})\cdot({\overline{\sigma_{I}}}^{\prime}||{\overline{\sigma_{O}}}^{\prime})\cdot({\overline{\sigma_{I}}}^{\prime\prime}||{\overline{\sigma_{O}}}^{\prime\prime})\models\varphi$, we have

[TABLE]

and

[TABLE]

Definition 5 (Collaborative $k$-Stabilizing Shield)

A shield $\mathcal{S}$ is collaboratively $k$-stabilizing if it collaboratively $k$-stabilizes any finite trace.

A collaborative $k$-stabilizing shield requires that it must be possible to end deviations after $k$ steps, for some future input and output of $\mathcal{D}$. It is not necessary that this is possible for all future behavior of $\mathcal{D}$ allowing infinitely long deviations.

Definition 6 (Collaborative Subgame Optimal Shield)

A shield $\mathcal{S}$ is collaborative subgame optimal if for any trace $\overline{\sigma}\in\Sigma^{*}$, $\mathcal{S}$ collaboratively $k-$stabilizes $\overline{\sigma}$ and there exists no shield that adversely $l$-stabilizes $\overline{\sigma}$ for any $l<k$.

Definition 7 (Admissible Shield)

A shield $\mathcal{S}$ is admissible if for any trace $\overline{\sigma}$, whenever there exists a $k$ and a shield $\mathcal{S}^{\prime}$ such that $\mathcal{S}^{\prime}$ adversely $k$-stabilizes $\overline{\sigma}$, then $\mathcal{S}$ adversely $k$-stabilizes $\overline{\sigma}$. If such a $k$ does not exist for trace $\overline{\sigma}$, then $\mathcal{S}$ collaboratively $k$-stabilizes $\overline{\sigma}$ for a minimal $k$.

An admissible shield ends deviations whenever possible. In all states of the design $\mathcal{D}$ where a finite number of deviations can be guaranteed, an admissible shield deviates for each violation for at most $k$ steps, for the smallest $k$ possible. In all other states, the shield corrects the output in such a way that there exists design’s inputs and outputs such that deviations end after $l$ steps, for the smallest $l$ possible.

5 Synthesizing Admissible Shields

The flow of the synthesis procedure is illustrated in Fig. 4. Starting from a safety specification $\varphi=(Q,q_{0},\Sigma,\delta,F)$ with $\Sigma=\Sigma_{I}\times\Sigma_{O}$, the admissible shield synthesis procedure consists of five steps.

5.0.1 Step 1. Constructing the Violation Monitor $\mathcal{U}$.

From $\varphi$ we build the automaton $\mathcal{U}=(U,u_{0},\Sigma,\delta^{u})$ to monitor property violations by the design. The goal is to identify the latest point in time from which a specification violation can still be corrected with a deviation by the shield. This constitutes the start of the recovery period, in which the shield is allowed to deviate from the design. In this phase the shield monitors the design from all states that the design could reach under the current input and a correct output. A second violation occurs only if the next design’s output is inconsistent with all states that are currently monitored. In case of a second violation, the shield monitors the set of all input-enabled states that are reachable from the current set of monitored states.

The first phase of the construction of the violation monitor $\mathcal{U}$ considers $\varphi=(Q,q_{0},\\ \Sigma,\delta,F)$ as a safety game and computes its winning region $W\subseteq F$ so that every reactive system $\mathcal{D}\models\varphi$ must produce outputs such that the next state of $\varphi$ stays in $W$. Only in cases in which the next state of $\varphi$ is outside of $W$ the shield is allowed to interfere.

The second phase expands the state space $Q$ to $2^{Q}$ via a subset construction, with the following rationale. If the design makes a mistake (i.e., picks outputs such that $\varphi$ enters a state $q\not\in W$), we have to “guess” what the design actually meant to do and we consider all output letters that would have avoided leaving $W$ and continue monitoring the design from all the corresponding successor states in parallel. Thus, $\mathcal{U}$ is essentially a subset construction of $\varphi$, where a state $u\in U$ of $\mathcal{U}$ represents a set of states in $\varphi$.

The third phase expands the state space of $\mathcal{U}$ by adding a counter $d\in\{0,1,2\}$ and a output variable $z$. Initially $d$ is 0. Whenever a property is violated$d$ is set to 2. If $d>0$, the shield is in the recovery phase and can deviate. If $d=1$ and there is no other violation, $d$ is decremented to 0. In order to decide when to decrement $d$ from 2 to 1, we add an output $z$ to the shield. If this output is set to $\mathsf{true}$ and $d=2$, then $d$ is set to 1.

The final violation monitor is $\mathcal{U}=(U,u_{0},\Sigma^{u},\delta^{u})$, with the set of states $U=(2^{Q}\times\{0,1,2\})$, the initial state $u_{0}=(\{q_{0}\},0)$, the input/output alphabet $\Sigma^{u}=\Sigma_{I}\times\Sigma_{O}^{u}$ with $\Sigma_{O}^{u}=\Sigma_{O}\cup z$, and the next-state function $\delta^{u}$ , which obeys the following rules:

\delta^{u}((u,d),({\sigma_{I}},{\sigma_{O}}))=\bigl{(}\{q^{\prime}\!\in\!W\mid\exists q\in u,{\sigma_{O}}^{\prime}\in\Sigma_{O}^{u}\operatorname{\mathbin{.}}\delta(q,({\sigma_{I}},{\sigma_{O}}^{\prime}))=q^{\prime}\},2\bigr{)}

if $\forall q\in u\operatorname{\mathbin{.}}\delta(q,({\sigma_{I}},{\sigma_{O}}))\not\in W$, and 2. 2.

\delta^{u}((u,d),\sigma)\!=\!\bigl{(}\{q^{\prime}\!\in\!W\mid\exists q\!\in\!u\operatorname{\mathbin{.}}\delta(q,\sigma)=q^{\prime}\},\textsf{dec}(d)\bigr{)} if $\exists q\!\in\!u\operatorname{\mathbin{.}}\delta(q,\sigma)\!\in\!W$, and $\textsf{dec}(0)=\textsf{dec}(1)=0$, and if $z$ is $\mathsf{true}$ then $\textsf{dec}(2)=1$, else $\textsf{dec}(2)=2$.

Our construction sets $d=2$ whenever the design leaves the winning region, and not when it enters an unsafe state. Hence, the shield $\mathcal{S}$ can take a remedial action as soon as “the crime is committed”, before the damage is detected, which would have been too late to correct the erroneous outputs of the design.

Example 1.

We illustrate the construction of $\mathcal{U}$ using the specification $\varphi$ from Fig. 5 over the outputs $o_{1}$ and $o_{2}$. (Fig. 5 represents a safety automaton if we make all missing edges point to an (additional) unsafe state.) The winning region consists of all safe states, i.e., $W=\{F,S,T\}$. The resulting violation monitor is $\mathcal{U}=(\{\text{F},\text{S},\text{T},\text{FS},\text{ST},\text{FT},\\ \text{FST}\}\times\{0,1,2\},(\text{F},0),\Sigma^{u},\delta^{u})$. The transition relation $\delta^{u}$ is illustrated in Table 1 and lists the next states for all possible present states and outputs. Lightning bolts denote specification violations. The update of counter $d$, which is not included in Table 1, is as follows: Whenever the design commits a violation $d$ is set to $2$. If no violation exists, $d$ is decremented in the following way: if $d=1$ or $d=0$, $d$ is set to 0. If $d=2$ and $z$ is $\mathsf{true}$, $d$ is set to 1, else $d$ remains 2. In this example, $z$ is set to $\mathsf{true}$, whenever we are positive about the current state of the design (i.e. in $(\{F\},d)$, $(\{S\},d)$, and $(\{T\},d)$).

Let us take a closer look at some entries of Table 1. If the current state is $(\{F\},0)$ and we observe the output $\neg o_{2}o_{1}$, a specification violation occurs. We assume that $\mathcal{D}$ meant to give an allowed output, either $o_{2}o_{1}$ or $\neg o_{2}\neg o_{1}$. The shield continues to monitor both $F$ and $S$; thus, $\mathcal{U}$ enters the state $(\{F,S\},2)$. If the next observation is $o_{2}o_{1}$, which is allowed from both possible current states, the possible next states are $S$ and $T$, therefore $\mathcal{U}$ traverses to state $(\{S,T\},2)$. However, if the next observation is again $\neg o_{2}o_{1}$, which is neither allowed in $F$ nor in $S$, we know that a second violation occurs. Therefore, the shield monitors the design from all three states and $\mathcal{U}$ enters the state $(\{F,S,T\},2)$.

5.0.2 Step 2. Constructing the Deviation Monitor $\mathcal{T}$.

We build $\mathcal{T}=(T,t_{0},\Sigma_{O}\times\Sigma_{O},\delta^{t})$ to monitor deviations between the shield and design outputs. Here, $T=\{t_{0},t_{1}\}$ and $\delta^{t}(t,({\sigma_{O}},{\sigma_{O}}^{\prime}))=t_{0}$ iff ${\sigma_{O}}={\sigma_{O}}^{\prime}$. That is, if there is a deviation in the current time step, then $\mathcal{T}$ will be in $t_{1}$ in the next time step. Otherwise, it will be in $t_{0}$. This deviation monitor is shown in Fig. 6.

5.0.3 Step 3. Constructing and Solving the Safety Game $\mathcal{G}^{s}$.

Given the automata $\mathcal{U}$ and $\mathcal{T}$ and the safety automaton $\varphi$, we construct a safety game $\mathcal{G}^{s}=(G^{s},g_{0}^{s},\Sigma_{I}^{s},\Sigma_{O}^{s}$ $\delta^{s},F^{s})$, which is the synchronous product of $\mathcal{U}$, $\mathcal{T}$, and $\varphi$, such that $G^{s}=U\times T\times Q$ is the state space, $g_{0}^{s}=(u_{0},t_{0},q_{0})$ is the initial state, $\Sigma_{I}^{s}=\Sigma_{I}\times\Sigma_{O}$ is the input of the shield, $\Sigma_{O}^{s}=\Sigma_{O}\cup\{z\}$ is the output of the shield, $\delta^{s}$ is the next-state function, and $F^{s}$ is the set of safe states such that \delta^{s}\bigl{(}(u,t,q),({\sigma_{I}},{\sigma_{O}}),({\sigma_{O}}^{\prime},z)\bigr{)}=

[TABLE]

and $F^{s}=\{(u,t,q)\in G^{s}\mid q\in F\wedge u=(w,0)\rightarrow t=t_{0}\}$.

We require $q\in F$, which ensures that the output of the shield satisfies $\varphi$, and that the shield can only deviate in the recovery period (i.e., if $d=0$, no deviation is allowed). We use standard algorithms for safety games (cf. [11]) to compute the winning region $W^{s}$ and the most permissive non-deterministic winning strategy $\rho_{s}:G\times\Sigma_{I}\rightarrow 2^{\Sigma_{O}}$ that is not only winning for the system, but also contains all deterministic winning strategies.

5.0.4 Step 4. Constructing the Büchi Game $\mathcal{G}^{b}$.

Implementing the safety game ensures correctness ($\mathcal{D}\circ\mathcal{S}\models\varphi$) and that the shield $\mathcal{S}$ keeps the output of the design $\mathcal{D}$ intact, if $\mathcal{D}$ does not violate $\varphi$. The shield still has to keep the number of deviations per violation to a minimum. Therefore, we would like the recovery period to be over infinitely often. This can be formalized as a Büchi winning condition. We construct the Büchi game $\mathcal{G}^{b}$ by applying the non-deterministic safety strategy $\rho^{s}$ to the game graph $\mathcal{G}^{s}$.

Given the safety game $\mathcal{G}^{s}=(G^{s},g_{0}^{s},\Sigma_{I}^{s},\Sigma_{O}^{s},\delta^{s},F^{s})$ with the non-deterministic winning strategy $\rho^{s}$ and the winning region $W^{s}$, we construct a Büchi game $\mathcal{G}^{b}=(G^{b},g_{0}^{b},\Sigma_{I}^{s},\\ \Sigma_{O}^{s},\delta^{b},F^{b})$ such that $G^{b}=W^{s}$ is the state space, the initial state $g_{0}^{b}=g_{0}^{s}$ and the input/output alphabet $\Sigma_{I}^{b}=\Sigma_{I}^{s}$ and $\Sigma_{O}^{b}=\Sigma_{O}^{s}$ remain unchanged, $\delta^{b}=\delta^{s}\cap\rho^{s}$ is the transition function, and $F^{b}=\{(u,t,q)\in W^{s}\mid(u=(w,0)\vee u=(w,1))\}$ is the set of accepting states. A play is winning if $d\leq 1$ infinitely often.

5.0.5 Step 5. Solving the Büchi Game $\mathcal{G}^{b}$.

Most likely, the Büchi game $\mathcal{G}^{b}$ contains reachable states, for which $d\leq 1$ cannot be enforced infinitely often. We implement an admissible strategy that enforces to visit $d\leq 1$ infinitely often whenever possible. This criterion essentially asks for a strategy that is winning with the help of the design.

The admissible strategy $\rho^{b}$ for a Büchi game $\mathcal{G}^{b}=(G^{b},g_{0}^{b},\Sigma_{I}^{b},\Sigma_{O}^{b},\delta^{b},F^{b})$ can be computed as follows[11]:

Compute the winning region $W^{b}$ and a winning strategy $\rho_{w}^{b}$ for $\mathcal{G}^{b}$ (cf. [19]). 2. 2.

Remove all transitions that start in $W^{b}$ and do not belong to $\rho_{w}^{b}$ from $\mathcal{G}^{b}$. This results in a new Büchi game $\mathcal{G}_{1}^{b}=(G^{b},g_{0}^{b},\Sigma_{I}^{b},\Sigma_{O}^{b},\delta_{1}^{b},F^{b})$ with $(g,({\sigma_{I}},{\sigma_{O}}),g^{\prime})\in\delta_{1}^{b}$ if $(g,{\sigma_{I}},{\sigma_{O}})\in\rho_{w}^{b}$ or if $\forall{\sigma_{O}}^{\prime}\in\Sigma_{O}^{b}\operatorname{\mathbin{.}}(g,{\sigma_{I}},{\sigma_{O}}^{\prime})\notin\rho_{w}^{b}\wedge(g,({\sigma_{I}},{\sigma_{O}}),g^{\prime})\in\delta^{b}$. 3. 3.

In the resulting game $\mathcal{G}_{1}^{b}$, compute a cooperatively winning strategy $\rho^{b}$. In order to compute $\rho^{b}$, one first has to transform all input variables to output variables. This results in the Büchi game $\mathcal{G}_{2}^{b}=(G^{b},g_{0}^{b},\emptyset,\Sigma_{I}^{b}\times\Sigma_{O}^{b},\delta_{1}^{b},F^{b})$. Afterwards, $\rho^{b}$ can be computed with the standard algorithm for the winning strategy on $\mathcal{G}_{2}^{b}$.

The strategy $\rho^{b}$ is an admissible strategy of the game $\mathcal{G}^{b}$, since it is winning and cooperatively winning [11]. Whenever the game $\mathcal{G}^{b}$ starts in a state of the winning region $W^{b}$, any play created by $\rho_{w}^{b}$ is winning. Since $\rho^{b}$ coincides with $\rho_{w}^{b}$ in all states of the winning region $W^{b}$, $\rho^{b}$ is winning. We know that $\rho^{b}$ is cooperatively winning in the game $\mathcal{G}_{1}^{b}$. A proof that $\rho^{b}$ is also cooperatively winning in the original game $\mathcal{G}^{b}$ can be found in [11].

Theorem 5.1

A shield that implements the admissible strategy $\rho^{b}$ in the Büchi game $\mathcal{G}^{b}=(G^{b},g_{0}^{b},\Sigma_{I}^{b},\Sigma_{O}^{b},\delta^{b},F^{b})$ in a new reactive system $\mathcal{S}=(G^{b},g^{b}_{0},\Sigma_{I}^{b},\Sigma_{O}^{b},\delta^{\prime},\rho^{b})$ with $\delta^{\prime}(g,{\sigma_{I}})=\delta^{b}(g,{\sigma_{I}},\rho^{b}(g,{\sigma_{I}}))$ is an admissible shield.

Proof 1

First, the admissible strategy $\rho^{b}$ is winning for all winning states of the Büchi game $\mathcal{G}^{b}$. Since winning strategies for Büchi games are subgame optimal, a shield that implements $\rho^{b}$ ends deviations after the smallest number of steps possible, for all states of the design in which a finite number of deviations can be guaranteed. Second, $\rho^{b}$ is cooperatively winning in the Büchi game $\mathcal{G}^{b}$. Therefore, in all states in which a finite number of deviation cannot be guaranteed, a shield that implements the strategy $\rho^{b}$ recovers with the help of the design as soon as possible.

The standard algorithm for solving Büchi games contains the computation of attractors; the $i$-th attractor for the system contains all states from which the system can “force” a visit of an accepting state in $i$ steps. For all states $g\in G^{b}$ of the game $\mathcal{G}^{b}$, the attractor number of $g$ corresponds to the smallest number of steps within which the recovery phase can be guaranteed to end, or can end with the help of the design if a finite number of deviation cannot be guaranteed.

Theorem 5.2

Let $\varphi=\{Q,q_{0},\Sigma,\delta,F\}$ be a safety specification and $|Q|$ be the cardinality of the state space of $\varphi$. An admissible shield with respect to $\varphi$ can be synthesized in $\mathcal{O}(2^{|Q|})$ time, if it exists.

Proof 2

Our safety game $\mathcal{G}^{s}$ and our Büchi game $\mathcal{G}^{b}$ have at most $m=(2\cdot 2^{|Q|}+|Q|)\cdot 2\cdot|Q|$ states and at most $n=m^{2}$ edges. Safety games can be solved in $\mathcal{O}(m+n)$ time and Büchi games in $\mathcal{O}(m\cdot n)$ time [19].

6 Experimental Results

We implemented our admissible shield synthesis procedure in Python, which takes a set of safety automata defined in a textual representation as input. The first step in our synthesis procedure is to build the product of all safety automata and construct the violation monitor 5.0.1. This step is performed on an explicit representation. For the remaining steps we use Binary Decision Diagrams (BDDs) for symbolic representation. The synthesized shields are encoded in Verilog format. To evaluate the performance of our tool, we constructed three sets of experiments, the basis of which is the safety specification of Fig. 1. This example represents a map with 15 waypoints and the six safety properties 1-6. First, we reduced the complexity of the example by only considering 8 out of 15 waypoints. This new example, called Map8, consists of the waypoints $loc_{1}$ to $loc_{8}$ with their corresponding properties. The second series of experiments, called Map15, considers the original specification of Fig. 1 over all 15 waypoints. The synthesized shields behave as described in Section 2. The third series of experiments, called Map31, considers a map with $31$ waypoints, essentially adding a duplicate of the map in Fig. 1. All results are summarized in Table 2 and in Table 3. For both tables, the first columns list the set of specification automata and the number of states, inputs, and outputs of their product automata. The next column lists the smallest number of steps $l$ under which the shield is able to recover with the help of the design. The last column lists the synthesis time in seconds. All computation times are for a computer with a 2.6 GHz Intel i5-3320M CPU with 8 GB RAM running an 64-bit distribution of Linux. Source code, input files, and instructions to reproduce our experiments are available for download111http://www.iaik.tugraz.at/content/research/design_verification/others/ .

7 Conclusion

We have proposed a new shield synthesis procedure to synthesize admissible shields. We have shown that admissible shields overcome the limitations of previously developed $k$-stabilizing shields. We believe our approach and first experimental results over our case study involving UAV mission planning open several directions for future research. At the moment, shields only attend to safety properties and disregard liveness properties. Integrating liveness is therefore a preferable next step. Furthermore, we plan to further develop our prototype tool and apply shields in other domains such as in the distributed settings or for Safe Reinforcement Learning, in which safety constraints must be enforced during the learning processes. We plan to investigate how a shield might be most beneficial in such settings.