Reactive Control Meets Runtime Verification: A Case Study of Navigation

TL;DR

This paper integrates formal runtime verification with reactive control for mobile robots, enabling safety and mission compliance through layered architecture and formal specifications, demonstrated via simulation.

Contribution

It introduces a layered control architecture embedding runtime monitors from formal specs into robot navigation, enhancing reactive control with verification techniques.

Findings

Successful simulation of robot navigation with integrated runtime verification

Formal specifications improve safety and mission adherence

Non-intrusive, compositional approach to control architecture

Abstract

This paper presents an application of specification based runtime verification techniques to control mobile robots in a reactive manner. In our case study, we develop a layered control architecture where runtime monitors constructed from formal specifications are embedded into the navigation stack. We use temporal logic and regular expressions to describe safety requirements and mission specifications, respectively. An immediate benefit of our approach is that it leverages simple requirements and objectives of traditional control applications to more complex specifications in a non-intrusive and compositional way. Finally, we demonstrate a simulation of robots controlled by the proposed architecture and we discuss further extensions of our approach.

Figures

Equations

$$\text{inside\_eastway implies (going\_east since entered\_eastway})$$

$$\text{inside\_westway implies (going\_west since entered\_westway})$$

$$\text{forall X. inside(X) implies (going(X) since entered(X)})$$

Full text

1 Introduction

Mobile robots are designed to work either in static and fully predictable environments such as automated warehouses or in open, partially unknown, and constantly changing environments such as road traffic. Classical deliberative control (complete planning before execution) often work well for the former case while being inadequate or very inefficient for the latter. Alternatively, in reactive control, robots continuously observe the environment and thus are able to react and adapt to previously unknown circumstances. Runtime verification (RV), on the other hand, is a branch of formal methods that deals with checking correctness temporal sequences against high-level specifications [3, 11, 16]. A common point between reactive control and runtime verification is that they both trade the completeness guarantees of deliberate control and model checking for online computation, practicality, and scalability. Following this synergy and growing interest in robotics using formal specifications, we think runtime verification techniques can be very useful to raise the level of abstraction and assurance for reactive controllers in robotic applications.

In this paper, we explore the combination of reactive control and runtime verification techniques to construct controllers for mobile robots that satisfy given safety requirements and high-level mission specifications. To this end, we employ a multi-layered architecture that can be seen in many reactive controllers and enhance each layer with runtime monitors to enforce desired properties on-the-fly. Compared to existing deliberative control approaches based on game theory [1, 7, 13], model checking [6, 4], and optimization [20, 17, 15], our proposal has several advantages summarized as follows. First, runtime verification techniques require fewer assumptions about the environment and robots as well as scale much better than those exhaustive methods. Second, we can use more expressive specification languages for runtime monitor construction. For example, it is possible to construct efficient runtime monitors from timed, quantitative, and first-order extensions of linear temporal logic (LTL) and regular expressions whereas game-theoretic reactive synthesis is usually limited to a fragment of LTL. Hence RV techniques cover a larger class of requirements we need in robotic applications. Third, most runtime verification techniques are compositional and it is easier to build modular robotic systems using them. All these advantages would suggest a wider applicability of runtime verification techniques in robotics.

We depict our navigation architecture that contains several components from reactive control and runtime verification domains in Figure 1. At the bottom layer of the architecture, we employ limited trajectory search to devise the short-time motion of the robot. Runtime monitors are embedded to check generated (candidate) trajectories and enforce low-level safety properties such as collision avoidance and one-way regulations. The middle layer addresses the shortcomings of short-horizon trajectories by searching a route over a connectivity graph of the environment. Mid-level safety properties for the graph traversal (e.g avoiding specific areas) are similarly enforced using runtime monitors in this layer. Once undesired trajectories and routes are filtered out, we use a number of features and heuristics to select the best one among the remaining. Repeating these procedures in real-time produces a safe motion for the robot to reach a specific (goal) location relative to trajectory/route generation specifics. Finally, the top layer is designated for high-level mission control that enforces the correct order of locations to be visited. In our study, we similarly employ runtime monitors constructed from mission specifications for the mission control.

The structure of this paper is as follows. First we describe our setup for the case study in Section 2. We then explain the use of runtime monitors to produce safe motion in Section 3 and to guide missions in Section 4. The paper is concluded in Section 5 by a discussion of simulation results and future directions.

2 Environment, Robots, and Specifications

For our case study, we will work on a relatively complex 2D environment designed to give a representative view of real challenges without introducing too much detail. Depicted on the left of Figure 2, our environment represents an office space with rooms (R1-R6), narrow passages (such as doors D1-D6), named locations (A-D), and some regulations at certain regions (one-way regions) including other (possibly uncontrolled) agents. We use a unicycle velocity-controlled model for the robot dynamics where the state space is defined by robot’s position $(x,y)$ and orientation $\theta$, and controlled by forward and angular velocity commands $u=(v,\omega)$.

It is of critical importance that the complexity of the environment determines the complexity of specifications and monitoring. For a static environment (that is to say, nothing changes outside of our control), we do not need any runtime monitoring at all. This is obviously a very strong assumption for many cases. On the other hand, if dynamic obstacles (such other agents) exist in the environment, we have to at least add a basic monitoring mechanism that checks simple propositions —will the robot collide with anything soon or did the robot reach its goal? Moreover, if we have more complex regulations and tasks to complete in the environment, rich specification languages to describe them becomes a preferable option. Therefore, our robots are assigned to perform complex navigation missions, specified by regular expressions, while avoiding static and dynamic obstacles as well as satisfying desired properties and regulations, specified by temporal logic formulas.

Finally we explain our use of environment maps depicted in Figure 2. In the real world, robots sense their immediate vicinity through their various sensors, which we do not model in this case study. Instead we assume that the locations of nearby static and dynamic obstacles are available to the robot at any time. Our control strategy does not depend on the full real-time geometric knowledge of the environment nor its naive discretization (grid-world). On the other hand, we heavily use the connectivity graph of the environment depicted in the right of Figure 2. Using such topological maps together with local motion planning are much more scalable and reliable than directly planning a full trajectory on a geometric map [5].

3 Search for Safe Motion

In this paper, we use the past fragment of linear temporal logic to specify safety properties due to the causality of the formalism and efficiency of constructed monitors. The semantics of past temporal operators always, once, since, and previously, their extensions, and monitor constructions from these specifications can be found in the papers [12, 10, 19].

We here show an application of runtime monitors to enforce the desired safe behavior inside trajectory and route search algorithms. The general procedure can be summarized in three steps: (1) Generating a number of alternative behaviors (trajectories or routes), (2) checking unsafe/undesired behaviors using runtime monitors, and (3) selecting the best remaining (thus safe) behaviors according to a predefined set of heuristics. Importantly, the extent of these search processes is limited due to available computational resources as well as that long-term complete plans may become invalid very quickly in dynamic and uncertain environments. In the following, we give more details about search procedures and actual properties used in the case study.

Trajectory Search

Dynamic window approach (DWA) [9] is a well-known collision avoidance and local motion planning algorithm that uses search procedures to find control actions (velocity commands) while considering robot’s dynamics. The search space of DWA is limited by maximum acceleration available to the robot as depicted on the left of Figure 3 and the algorithm samples a set of control actions from this space typically over a grid of some resolution. Then it calculates the future trajectories (over a limited time horizon) of each alternative action as illustrated on the right of the figure.

Originally being a collision avoidance algorithm, the only safety requirement over these trajectories considered in DWA is never getting dangerously close to obstacles, which is usually hard-coded into the algorithm. On the other hand, we are interested in checking such requirements using runtime monitors so that we can extend the approach for any temporal logic formula. We start our case study by expressing the collision avoidance requirement in temporal logic as follows.

[TABLE]

where dangerously_close is a predicate that computes whether any intersection occurs between obstacles and robot’s extended footprint.

In this case study, besides collision avoidance, we also want our robot to obey one-way regulations of the environment, which state that robots have to move in a single direction inside certain regions. The direction of one-way regions is either west or east in our environment. We call these regions westways and eastways accordingly. Predicates inside_westway and inside_eastway check whether the robot in these regions. Moreover, we define some auxiliary formulas to detect whether the robot just entered a one-way region such that

[TABLE]

The correct direction in a one-way region is checked by predicates

[TABLE]

where orientation denotes the current orientation of the robot in degrees (0-360) and the zero degree denote the north. Finally we write our safety properties for each type of one-way regions as follows.

[TABLE]

However, notice that having many one-way specifications can lead to a linear growth in formula and monitor size. A better way to handle these requirements is to use parametric specifications where the direction of one-way region is considered as a parameter in the formula. The conjuction of formulas (OW-W) and (OW-E) can be expressed more concisely as follows.

[TABLE]

where $\texttt{X}\in\{\texttt{eastway},\texttt{westway}\}$. Monitoring such first-order temporal formulas is solved very efficiently in [10]. Finally, we construct our runtime monitor to check the conjunction of (CA) and (OW) requirements over trajectories. Control actions that produces violating trajectories are discarded before the selection phase. This ensures the safety of selected control action if there exists one in alternatives otherwise we apply full break.

The last piece of trajectory search is to select the best one among safe trajectories according to a weighted sum of some predefined heuristics, namely final speed of the trajectory (higher is better), final-distance-to-goal (lower is better), minimum-distance-to-obstacles (higher is better). In the case study, the actual values of weights are found empirically.

Route Search

A well-known problem of local trajectory search algorithms like DWA is that they may cause a robot to be stuck at a corner if the navigable space is highly non-convex. This problem can be mitigated by stacking an additional layer of control to steer the robot over key locations (such as doors, intersections, etc.) of the environment . Given a connectivity graph of these locations, we can search a route from the current location to the actual goal location and each node on the route is passed to the lower layer as a (sub) goal. In search of a suitable route, we need to take into account some extra requirements. First, it is often desired the chosen route do not contain any loops, thus be a simple path over the graph. We can specify the simple path property as follows.

[TABLE]

The SP property is usually embedded into graph search algorithms via marking visited nodes; therefore, we may or may not use an external monitor depending on our route generation technique. On the other hand, external runtime monitors are desirable to enforce application-specific properties as in trajectory search rather than generating a new graph search algorithm for each and every of them. For example, consider a property such that the robot never uses the door D6A when going from the location D to A, which can be expressed as follows.

[TABLE]

We then construct a runtime monitor from the property ND (and SP if needed) to check routes generated over the graph. In particular, we use an off-the-shelf implementation of the shortest path algorithm [21] that generates simple paths starting from the shortest one in this paper. Sequentially checking these paths using runtime monitors constructed from temporal logic formulas [12, 19] ensures that the we select the shortest route that satisfies specified properties and then we can update the route of the robot accordingly.

4 Navigate by Regular Expressions

In this section, we use regular expressions to specify complex navigation missions and guide the mission execution via runtime monitors constructed from the specification. Navigation missions describe the desired behavior of the robot over a set of observations and regular operations of sequential composition (;), alternative choice (|), and repetition (*) are used to express the ordering between these observations. For example, a robot is said to reach a region A when it was outside for a while and then entered the region A. We can specify such a behavior using regular expressions as follows:

[TABLE]

where atomic propositions inside(A) and outside(A) check whether the robot is in the region A or not. Similarly more complex missions are obtained by composing simple missions as below.

[TABLE]

which specifies a (robot) behavior to repeatedly visit the regions A, and D with visiting B or C in-between. From this expression, we construct a runtime monitor [18] that associates a Boolean state variable for each proposition and updates them according to previous states and robot’s position at each time step.

Recall that the purpose of the mission layer is to guide the mission execution by sending the next goal location to the lower levels. Therefore, we extend the runtime monitor to output goal locations according to the state of the mission in the following. For that we augment each state variable corresponding to a proposition with a set of goal locations. For example, the proposition inside(C) is augmented with $\{\texttt{B},\texttt{C}\}$ according to the follow sets (see [18]) and outside(A) with the empty set. Intuitively it means that the robot is ordered to go to the locations B or C when it is outside and go nowhere if it is inside. The final output of the monitor obtained by taking the union of activated goals as we may have several alternative ways to complete a mission. Notice that this is essentially due to non-determinism induced by choice and repetition operators of regular expressions. Finally we note that we randomly select one goal location in this study if the output of the monitor contains more than one location without any further consideration.

Finally we present our simulation results of four robots G1-G4 operated in the same environment and controlled by the proposed architecture. We assign the first robot G1 with the mission M1 and the rest G2-G4 with missions M2-M4 below, respectively.

[TABLE]

In Figure 4, we separately show the simulated trajectories of the robot for a certain duration that covers several loops as specified in the mission. The initial position of the robot is marked by a yellow star. Robots get close to each other quite frequently and evading maneuvers cause small variations among loops seen in the figure. Overall we see that the robots successfully avoid each other and static obstacles and obey regulations of the environment while performing their formally-specified missions over achieving near-optimal trajectories.

5 Discussion

In this paper, we presented an example and novel use of provably correct runtime monitors to control a mobile robot subject to complex safety requirements and mission specifications in a dynamic environment. To this end, we embedded runtime monitors into a layered reactive control architecture together with other simple and scalable components to achieve a navigation solution that does not require strong assumptions. Our approach amounts to a more active use of runtime monitors beyond checking assumptions of an offline planner at runtime [14, 2, 8]. We believe the simplicity and breadth of runtime monitors would make them ideal to cover many use cases and increase the level of assurance in robotic applications. In the future, we would like to explore collective missions for a team of robots as well as some relations among missions (e.g. priority). We think the compositionality of runtime monitors used in this study would be important to realize these much needed features.

We finally note that, unlike traditional end-to-end motion planning, we have not been interested in generating a complete trajectory to the destination for the robot in this study. The main drawback as we see is that accurate long-term plans can be invalidated quickly in a highly dynamic environment. Hence there is no point of making such plans for the robot as we need to re-plan anyways, perhaps frequently. On the other hand, it may be still better to envisage these deliberative techniques in a reactive framework to generate short-term trajectories or build/update the connectivity graph. In that case, we can use runtime monitors to enforce safety requirements as explained in this paper.