Analyzing and revising synthesized controllers for robots with sensing and actuation errors

Abstract

The synthesis of verifiable robot controllers from a set of high-level task specifications provides a valuable tool for creating robot controllers for complex tasks. Such an approach can offer a number of advantages over more traditional programming methods, including the guarantee that the synthesized controller will satisfy all of its underlying specifications when operating with perfect sensing and actuation. This paper relaxes that assumption, and describes a method for probabilistically analyzing the behavior of a robot controller that is synthesized from a set of temporal logic specifications, when the robot operates with uncertainty in its sensing and actuation. The described approach creates a probabilistic model of the system and uses probabilistic model checking techniques to find the probability that it satisfies some set of specifications. In addition, the paper proposes a method which leverages that analysis to provide automated feedback to the user in the form of suggested revisions to the task specification or low-level components, in order to increase the probability that the robot successfully accomplishes its task.

Keywords

Probabilistic analysis temporal logic planning controller synthesis

1. Introduction

Recent research in the fields of robotics and automation has adapted techniques from the formal methods community to enable the synthesis of correct-by-construction robot controllers for complex tasks (Loizou and Kyriakopoulos, 2004; Fainekos et al., 2006; Kloetzer and Belta, 2006; Tabuada and Pappas, 2006; Conner et al., 2007; Kress-Gazit et al., 2007b,a). Such techniques take a specification of the desired robot behavior, and create an abstract controller that is guaranteed to satisfy those specifications (if such a controller exists). Doing so offers a number of advantages over a more traditional controller design process.

Synthesis lowers the level of technical expertise required to design and build a controller for a complex task by abstracting away many lower-level details and avoiding traditional programming languages.

Synthesis reduces the time investment typically required to implement a robot controller by allowing the designer to create and edit the controller directly from the task specification.

Synthesis techniques also typically offer guarantees on the behavior of the robot with respect to the specified task; such guarantees ease the burden of validation and testing of the controller.

Research on the synthesis of robot controllers has led to a number of different approaches, each with their own advantages and disadvantages. Fainekos et al. (2007) and Wongpiromsarn et al. (2009), for example, proposed methods that use feedback controllers to control the motion of the robot, while Bhatia et al. (2010) and Karaman and Frazzoli (2009) sacrifice completeness and use sampling-based methods for robots with more complex dynamics. Kloetzer and Belta (2006) and Karaman and Frazzoli (2009) use synthesized controllers to complete complex motion tasks in static environments, while Kress-Gazit et al. (2009) and Wongpiromsarn et al. (2010), by contrast, synthesize controllers that react to dynamic events in the environment.

Each of these proposed approaches provides some guarantee on the execution of the synthesized controller. The approach by Kress-Gazit et al. (2009), for example, synthesizes a controller in such a way that it is guaranteed to satisfy all of the underlying specifications, if one assumes that the abstract sensors and actuators operate without error. Such an assumption is, however, typically infeasible in real-world scenarios. As such, it is important to provide guarantees that account for the errors and uncertainties that occur when operating in complex, real-world environments.

The work described in this paper presents a method for analyzing the probabilistic behavior of a robot operating with errors in its sensing and actuation, as well as a method to leverage that analysis and provide feedback to the user to improve the performance of the robot. First, a formally synthesized controller is composed with probabilistic models of the robot’s environment, and probabilistic models of the errors in the robot’s sensing and actuation. This model is then analyzed using probabilistic model checking software to determine the probability that it satisfies a set of temporal logic formulas describing the robot’s behavior. In addition, a method is presented to automatically generate multiple types of revision suggestions (which are provided to the user) in order to improve the probabilistic behavior of the robot.

Johnson and Kress-Gazit (2011, 2012) assess the impact of errors in the robot’s perception of the environment. In these papers, they create sensor propositions which, in the error-free case, mimic the set of environment event propositions. By probabilistically modeling false positives and false negatives, they include the probability of erroneous sensor values in a discrete model of the overall system. They then use probabilistic model checking techniques to compute the probability that the robot satisfies some set of linear temporal logic (LTL) formulas, and use the analysis to inform design choices for the synthesized controller. They apply this approach to the scenario of an autonomous car in Johnson et al. (2012).

Similarly, Johnson and Kress-Gazit (2013) model errors in the robot’s actuation by the inclusion of probabilistic transitions to unintended states. Again, a discrete, probabilistic model of the system is created, and a probabilistic model checker is used to compute the probability that the robot satisfies some set of LTL formulas. The paper then extends the analysis by providing a preliminary method for the automatic determination of revisions to the original specification that may result in a controller with a higher likelihood of satisfying the given task. This process of computing specification revisions for the user provides a valuable tool in the design of synthesized robot controllers, as it provides the designer with important feedback to improve the probability that the robot exhibits a particular behavior. Furthermore, by including the designer in the feedback loop (i.e. returning the suggested revision to the user, rather than automatically including it in the specification and re-synthesizing), the process helps to prevent the emergence of unexpected or unwanted behavior from the generated revisions.

The work presented in this paper builds upon the authors’ earlier work in Johnson and Kress-Gazit (2011, 2012, 2013). First, this paper discusses composition and analysis of a probabilistic model of the system, which includes both sensor and actuator error. The simultaneous consideration of both sensor and actuator error, which is necessary in real-world applications, requires significant adaptations of the composition algorithms presented in Johnson and Kress-Gazit (2012, 2013); the new algorithms, and the required adaptations are detailed in Section 4. In addition, this paper expands on the preliminary approach described in Johnson and Kress-Gazit (2013) for automatically generating revision suggestions for the original specification. This paper presents an improvement to the revision algorithm described in the authors’ earlier work, as well as presenting three additional methods for generating complimentary revision suggestions.

1.1. Related work

Kloetzer and Belta (2006) present an approach for generating a feedback control strategy from LTL specifications in such a way that all closed-loop trajectories for the controller will satisfy the specification, despite disturbances in the continuous system. Lahijanian et al. (2009, 2010) extend that work by modeling the uncertainty on the outcomes of the low-level motion primitives, and altering the synthesis algorithm such that it generates the motion plan that has the highest probability of satisfying the specification. Ding et al. (2012) improve the computational feasibility of the approach via dynamic programming. Each of these approaches enables the synthesis of a complex control policy that maximizes the probability of satisfying a specification; unlike these works, the approach presented in this paper considers synthesized controllers that react to changes in the robot’s environment, and uses an analysis of the synthesized controller to generate revision specifications which are returned to the user (the cited works directly account the effects of uncertainty in the synthesis step).

Medina Ayala et al. (2012) present a method to maximize the probability of satisfying a specification within a specific time bound. In that work, the synthesized controller reacts to time-varying properties of the environment, which are modeled stochastically. Ding et al. (2011) allow for time-varying observations of the robot’s environment (modeled as propositions that may be either true or false at each vertex in the environment), and generate a controller that maximizes the probability that the robot satisfies some specification (which may be reactive with respect to those observations). Lyons et al. (2013) present a Process-Algebra-based method for probabilistically validating robot mission software in an uncertain environment, described by random variables. The work presented here differs from these papers in the formulation of the uncertainty and errors in the system, and in the abstract, non-motion actions the robot may activate. This formulation allows for a description of the task and errors in sensing and actuation that is general enough to be applied to a wide variety of applications.

In each of the aforementioned works, the probabilistic information about the system is incorporated directly into the synthesis process. In contrast, the approach presented in this paper takes a controller that is synthesized assuming perfect sensing and actuation (the ideal case), and describes a method for assessing the probabilistic performance of that controller, post-synthesis. Such a process provides a different, complimentary method for accounting for errors in the robot’s sensing and actuation, in that it allows for a formal analysis of the controller, and it provides feedback to the user (rather than directly incorporating it into the synthesis process). The additional application of this analysis to generate revisions to be returned to the user provides an alternate method for improving the robot’s behavior. While inclusion of the generated revisions is not guaranteed to optimize the probabilistic behavior of the robot (as the related synthesis approaches do), it has the advantage of involving the user in the process (which may help to avoid possible unintuitive or undesirable behaviors that may result from the optimization process).

The generation of revisions for controller synthesis is, at this point, largely unexplored. In a recent paper, Cizelj and Belta (2013) present a method for the supervised synthesis of and revision of a motion control policy for a Dubins vehicle, where the control policy is synthesized from a temporal logic specification. Furthermore, the algorithms provide the user with suggestions for specification relaxation in order to improve the performance of the robot. The work presented in this paper differs from Cizelj and Belta (2013) in several ways, most notably in the formulation of the problems considered: this work allows for the inclusion of non-motion actions (rather than synthesizing a motion control policy), and assumes that the robot must react to a dynamic (rather than static) environment.

Other related work in the literature is that of Kim et al. (2012) and Fainekos (2011). In these papers, the authors present approaches for revising an unsynthesizable temporal logic specification by relaxing the restrictions on the initial condition of the robot in such a way that the specification becomes synthesizable. Raman and Kress-Gazit (2013) describe techniques for automatically generating a concise explanation for an unsynthesizable LTL specification; the approach provides feedback to the user to aid in debugging the specification and enable the synthesis of a feasible robot controller. In each of these works, the authors address a related but distinct problem in revising an unsynthesizable specification so that it becomes synthesizable. In contrast, this work assumes that the specification is already synthesizable, and suggests revisions to improve the probabilistic behavior of the robot.

The paper is organized as follows. Section 2 presents some necessary background information, and Section 3 formally defines the problem statement. Sections 4 and 5 detail the methods for modeling and analyzing the controllers and for generating revision suggestions. The approach is illustrated by an example in Section 6. Concluding remarks are given in Section 7.

2. Preliminaries

2.1. Linear temporal logic

LTL is a logical formalism that allows for the expression of linear-time temporal properties. An LTL formula ϕ is defined over a set of Boolean propositions Π. The syntax for a formula ϕ is defined recursively as

ϕ : : = true | π \in Π | \neg ϕ | ϕ \land ϕ | ◯ ϕ | ϕ U ϕ

(1)

The semantics of an LTL formula is defined over an infinite sequence of states σ, where a state σ_i , which occurs at time i in the sequence, is a set of truth assignments to the atomic propositions π ∈ Π. A state σ_i satisfies an LTL formula (denoted by σ_i ⊨ϕ) as defined by the following conditions:

\begin{matrix} \begin{matrix} \begin{matrix} σ_{i} ⊨ π iff π \in σ_{i} \\ σ_{i} ⊨ \neg ϕ iff σ_{i} ⊭ ϕ \end{matrix} \\ σ_{i} ⊨ ϕ_{1} \land ϕ_{2} iff σ_{i} ⊨ ϕ_{1} and σ_{i} ⊨ ϕ_{2} \end{matrix} \\ σ_{i} ⊨ ◯ ϕ iff σ_{i + 1} ⊨ ϕ \\ σ_{i} ⊨ ϕ_{1} U ϕ_{2} iff \exists k | k \geq i s . t . σ_{k} ⊨ ϕ_{2} \\ and \forall j | i \leq j < k : σ_{j} ⊨ ϕ_{1} \end{matrix}

(2)

A sequence of states σ is said to satisfy a formula ϕ if, for all initial states σ ₀, σ ₀⊨ϕ.

Intuitively, the formula ◯ϕ is true when ϕ holds true in the next state in the sequence, and $ϕ_{1} U ϕ_{2}$ is true when the formula ϕ ₁ holds until ϕ ₂ becomes true (and ϕ ₂ becomes true at some point). Additional common operators can be derived from the operators in Equation (1). The disjunction operator (∨) can be defined from the negation (¬) and conjunction (∧) operators, as can implication (→) and bi-conditional (↔). In addition, the temporal operators for eventually (♢) and always (□) can be defined using the until ( $U$ ) operator. More details on the syntax and semantics of LTL can be found in Emerson (1990).

2.2. Controller synthesis

The synthesized controllers used in this work were created using the approach described by Kress-Gazit et al. (2009). That approach requires a set of propositions $X$ that model abstract events in the environment, which the robot must observe and react to; similarly, the state and actions of the robot are described by a set of abstract propositions $Y$ , which includes propositions to track the location of the robot in a discretized workspace, as well as abstract actions that the robot can perform (such as opening a door, or signaling an operator). Consider, for example, a scenario where a robot is required to pass from one room to another through a doorway, which may be either closed or open. The set of environment propositions would, in this case, consist of a proposition that identifies whether or not the door is open $X = {Open}$ , where the proposition Open is true if, and only if, the door is open. The set of robot propositions would, in this case, consist of a pair of propositions representing each of the rooms $Y = {r_{1}, r_{2}}$ , where each proposition is true precisely when the robot is in the corresponding room.

The desired task for the robot is then described by an LTL formula that is restricted to the general reactivity (1) class of formulas, as described in Piterman et al. (2006). This class of formulas takes the form

ϕ = (φ_{i}^{e} \land φ_{t}^{e} \land φ_{g}^{e}) \to (φ_{i}^{s} \land φ_{t}^{s} \land φ_{g}^{s})

(3)

In the above formula, the specification for the robot is given as a desired robot behavior (defined by $φ_{i, t, g}^{s}$ ) in response to changes in the environment (defined by $φ_{i, t, g}^{e}$ ). The formulas $φ_{i}^{e}$ and $φ_{i}^{s}$ are defined as Boolean formulas B_i over $X \cup Y$ , and represent the initial conditions of the environment and robot, respectively. The formulas $φ_{t}^{e}$ and $φ_{t}^{s}$ are of the form □B_t , where B_t is a Boolean formula over $X \cup Y \cup ◯ X \cup ◯ Y$ , and represent the restrictions on the possible transitions that the environment and robot can make, often referred to as safety specifications. Finally, the formulas $φ_{g}^{e}$ and $φ_{g}^{s}$ take the form □♢B_g , where B_g is a Boolean formula defined over $X \cup Y$ , and represent the goals of the environment and robot; they are referred to as fairness and liveness conditions, respectively.

Returning to the example of a robot attempting to move through a doorway, the initial condition of the environment might specify whether the door is initially open ( $φ_{i}^{e} = Open$ ) or closed ( $φ_{i}^{e} = \neg Open$ ); the initial condition of the robot (e.g. $φ_{i}^{s} = r_{1}$ ) would specify which room the robot starts in. The safety specification would then require that the robot not move between rooms if the door is closed: $φ_{t}^{s} = □ (\neg Open \to \neg ((r_{1} \land ◯ r_{2}) \lor (r_{2} \land ◯ r_{1})))$ . The liveness conditions (i.e. the goals) for the robot in this example might be to repeatedly visit each of the rooms: $φ_{g}^{s} = □ ♦ r_{1} \land □ ♦ r_{2}$ . Finally, in order to ensure that the robot can complete its task, a fairness condition must be applied to the environment, which requires that the door cannot remain closed indefinitely: $φ_{g}^{e} = □ ♦ Open$ .

From the abstracted environment $X$ and robot $Y$ propositions, as well as the task specification ϕ, a controller is synthesized using the approach described by Piterman et al. (2006). The synthesized controller takes the form of a finite-state automaton $A = {S, S_{0}, X, Y, δ, L}$ , where S is the set of states, and S ₀⊆S is the set of possible initial states. The sets of environment and robot propositions are given by $X$ and $Y$ as described above. Here $δ : S \times 2^{X} \to S$ is a transition function that maps a state and set of environment (input) propositions to a successor state, and $L : S \to 2^{Y}$ is a labeling function that maps each state to a subset of the robot propositions $Y$ . As additional information, the synthesis algorithm can provide a function $X_{0} : S_{0} \to 2^{X}$ that maps initial states to sets of environment propositions, and a ranking function $Γ : S \to ℕ$ that maps each state to the index of the liveness condition that state is working towards completing.

By restricting the specification to the class of general reactivity (1) formulas, the computational cost of the synthesis algorithm is reduced from doubly exponential in the size of the formula to polynomial in the size of the state space. Even with this computational improvement, however, synthesis of a controller can become intractable for large state spaces. Such issues can become apparent when specifying a task for multiple vehicles, or explicitly modeling time (rather than temporal relationships).

2.3. Probabilistic model checking

A number of different options exist for performing probabilistic model checking, depending on the type of model and the type of properties to be checked. The work in this paper relies on model checking a discrete-time Markov chain (DTMC) model against LTL properties. The probabilistic model is defined as a DTMC $D = {Q, Q_{0}, Δ, Π, L, Γ}$ , where Q is the set of states and Q ₀⊆Q is the set of initial states. The transition function Δ: Q × p→Q maps one state to another, with probability p. The labeling function $L : Q \to 2^{Π}$ maps each state to a subset of the propositions Π. Note that the definition of a DTMC used here differs slightly from the standard definition of a DTMC (Kwiatkowska and Parker, 2012) by the inclusion of the ranking function $Γ : Q \to ℕ$ that maps each state to the index of its corresponding liveness condition.

While a number of different algorithms and off-the-shelf model checkers exist, the work presented in this paper uses PRISM probabilistic model checker (Kwiatkowska et al., 2011), which offers, among other capabilities, the ability to compute the probability that a DTMC satisfies a particular LTL formula, and is available online.

3. Problem statement

The work presented in this paper considers correct-by-construction controllers such that, when the robot’s sensors and actuators operate without error, the controller is guaranteed to satisfy all of its underlying specifications. This paper investigates the affects of errors in sensing and actuation on the behavior of the robot, and the revision of the controller to improve the behavior of the robot under those erroneous conditions. To include these effects, the behavior of the environment, sensors, and actuation of the robot are all defined probabilistically.

The changes in the environment are described by a set of probabilities P(X′|X,Y) that represent the changes in the abstract environment propositions $X$ . In this set of probabilities, each new environment configuration $X' \subseteq X$ (that is, the subset of environment propositions that are true in the next step) is modeled to depend only on the previous configuration of the environment $X \subseteq X$ (the subset of environment propositions that are true in the current step) and the previous configuration of the robot $Y \subseteq Y$ (the subset of robot propositions that are true in the current step).

To model the sensors, an additional set of propositions $\bar{X}$ is used to represent the robot’s perception of the environment propositions such that $\bar{X} = {\bar{x_{i}} | x_{i} \in X}$ where each $\bar{x_{i}}$ proposition represents the sensed value of the corresponding environment proposition x_i . For the doorway example introduced previously this means the set of sensor propositions $\bar{X} = {\bar{Open}}$ contains a proposition describing whether or not the robot senses the door to be open (in contrast to the environment proposition Open, which denotes whether or not the door is actually open). The evolution of the sensor propositions, then, is given by the set of probabilities $P (\bar{X}' | X', \bar{X}, Y)$ , such that the new sensor configuration $\bar{X}'$ is dependent only on the new environment configuration X′ and the current sensor and robot configurations, $\bar{X}$ and Y, respectively. In this model, the sensor error is represented through false positives (where $\bar{x'_{i}} = true$ and x′_i = false) and false negatives (where $\bar{x'_{i}} = false$ and x′_i = true) in how the sensor propositions mimic the environment propositions.

To model the actuation error, changes in the robot configuration are modeled by the set of probabilities $P (Y' | \bar{Y}', Y)$ , where the new robot configuration Y′ is dependent only on the previous robot configuration Y and the intended next robot configuration $\bar{Y}'$ . Note that the new robot configuration is indirectly dependent on environment and sensor values through the intended next robot configuration, which is chosen by the controller based on its observations of the environment. This model accounts for actuation error through differences between the intended next robot configuration $\bar{Y}'$ (as determined by the synthesized controller) and the actual configuration Y′ that results from attempting to make that transition. In terms of the doorway example, the synthesized controller may specify that the robot should move from r ₁ to r ₂ (i.e. Y = {r ₁} and $\bar{Y}' = {\bar{r_{2}}}$ ), but the robot may fail to actually do so (Y′ = {r ₁}) due to colliding with the door frame.

These probabilities each represent a discrete set of probabilities for the changes in the abstract propositions representing the state of the environment, sensors, and robot. That is, each possible change in the state is assigned a single value, representing the probability that the event occurs; the set of these probabilities describes the probabilistic evolution of the state of the system. Each of these sets of probabilities (for the environment, sensors, and robot actuation) can be estimated using statistical data gathered from experiments or simulations. Lahijanian et al. (2010), for example, use experimental data to determine the probabilistic outcomes of different motion primitives during the operation of their robot. Similarly, Johnson et al. (2012) use statistical information gathered from a simulation to model the changes in the abstracted environment and sensors for an autonomous vehicle.

Problem. Given a synthesized robot controller $A$ and probabilistic models of the environment P(X′|X,Y), imperfect sensors $P (\bar{X}' | X', \bar{X}, Y)$ , and imperfect robot actuation $P (Y' | \bar{Y}', Y)$ , find the probability that a robot using the synthesized controller will satisfy a set of LTL specifications. Furthermore, provide revision suggestions to the user to improve the probability that the robot satisfies the specifications.

4. Modeling and analysis

An overview of the approach presented in this paper for composing and analyzing a model of the robot with sensor and actuator error is shown in Figure 1. The model of the probabilistic system is composed from the synthesized controller and probabilistic models of the environment, sensors, and actuation; it is then analyzed with a probabilistic model checker to calculate the likelihood that the robot will satisfy a given set of task specifications. Sections 4.1 and 4.2 detail the process of including the sensor error and the actuator error in a probabilistic model of the system. Although both types of error could be incorporated into the model simultaneously, they are presented separately here to simplify both the implementation and the explanation of the process.

Fig. 1.

Diagram of the approach used to compose and analyze a probabilistic model of the robot, including the effects of sensor and actuator error.

4.1. Sensor error

Algorithm 1 describes the process of composing the environment probabilities and sensor error with the synthesized controller to create a probabilistic model of the system with imperfect sensors. This algorithm is a modified version of that given by Johnson and Kress-Gazit (2012), and has been changed to facilitate the integration of actuator error by including the correspondence between each probabilistic state and its originating automaton state. In addition, the algorithm was changed such that it creates new probabilistic states for any transition with probability greater than zero, and includes transitions to deadlock states and states that correspond to unconnected automaton states. This change allows for arbitrary probabilistic models of the sensors (of the form $P (\bar{X}' | X', \bar{X}, Y)$ ), instead of requiring that the sensor model adhere to any environmental assumptions, as was the case in Johnson and Kress-Gazit (2012).

Algorithm 1. Include sensor error in the system model.
1: procedure SensErr( $A = {S, S_{0}, X, Y, δ, L}, X_{0}, Γ, \bar{X}, P (X' \| X, Y), P (\bar{X}' \| X', \bar{X}, Y)$ )
2: Q = ∅, Q ₀ = ∅, Q ^* = ∅, Δ = ∅, Λ = ∅, Γ_q = ∅
3: for s_i ∈S do
4: if s_i ∈S ₀ then
5: X_i = X ₀(s_i )
6: Q ₀ = Q ₀ ∪ q_i
7: else
8: $X_{i} \subseteq X s . t . \exists s_{h} \in S \| (s_{h}, X_{i}, s_{i}) \in δ$
9: $\bar{X_{i}} = X_{i}, Y_{i} = L (s_{i})$
10: $L (q_{i}) = X_{i} \cup \bar{X_{i}} \cup Y_{i}$
11: Q = Q ∪ q_i , Q ^* = Q ^* ∪ q_i
12: Λ(q_i ) = s_i , Γ_q(q_i ) = Γ(s_i )
13: while Q^* ≠∅do
14: Choose q_i ∈Q ^, Q ^ = Q ^* \ q_i
15: $s_{i} = Λ (q_{i}), X_{i} = L (q_{i}) \cap X, \bar{X_{i}} = L (q_{i}) \cap \bar{X}, Y_{i} = L (q_{i}) \cap Y$
16: for $X_{j} \in 2^{X} s . t . p (X_{j} \| X_{h}, Y_{i}) > 0$ do
17: for $\bar{X_{k}} \in 2^{\bar{X}} s . t . p (\bar{X_{k}} \| X_{j}, \bar{X_{i}}, Y_{i}) > 0$ do
18: $p_{ijk} = p (X_{j} \| X_{i}, Y_{i}) \cdot p (\bar{X_{k}} \| X_{j}, \bar{X_{i}}, Y_{i})$
19: if $\exists s_{k} \in S s . t . (s_{i}, \bar{X_{k}}, s_{k}) \in δ$ then
20: Y_k = L(s_k )
21: if $\exists q_{jk} \in Q s . t . L (q_{jk}) = X_{j} \cup \bar{X_{k}} \cup Y_{k}$ and Λ(q_jk ) = s_k then
22: Δ = Δ ∪ (q_i , p_ijk , q_jk )
23: else
24: $L (q_{jk}) = X_{j} \cup \bar{X_{k}} \cup Y_{k}$
25: Q = Q ∪ q_jk , Q ^* = Q ^* ∪ q_jk
26: Λ(q_jk ) = s_k , Γ_q(q_jk ) = Γ (s_k )
27: Δ = Δ ∪ (q_i , p_ijk , q_jk )
28: else if∃s_h , s_k ∈S s.t. L(s_h ) = L(s_i ) and $(s_{h}, \bar{X_{k}}, s_{k}) \in δ$ then
29: $(s_{h}^{}, s_{k}^{}) = {argmin}_{(s_{h}, s_{k})}$ ((Γ(s_i ) −Γ(s_h )) modulo max_s _∈S(Γ(s)))
30: if $\exists q_{jk} \in Q s . t . L (q_{jk}) = X_{j} \cup \bar{X_{k}} \cup Y_{k}$ and $Λ (q_{jk}) = s_{k}^{*}$ then
31: Δ = Δ ∪ (q_i , p_ijk , q_jk )
32: else
33: $L (q_{jk}) = X_{j} \cup \bar{X_{k}} \cup Y_{k}$
34: Q = Q ∪ q_jk , Q ^* = Q ^* ∪ q_jk
35: $Λ (q_{jk}) = s_{k}^{}, Γ_{q} (q_{jk}) = Γ (s_{k}^{})$
36: Δ = Δ ∪ (q_i , p_ijk , q_jk )
37: else
38: Y_k = Y_i
39: $L (q_{jk}) = X_{j} \cup \bar{X_{k}} \cup Y_{k}$
40: Q = Q ∪ q_jk
41: Λ(q_jk ) = None, Γ_q(q_jk ) = Γ_q(q_i )
42: Δ = Δ ∪ (q_i , p_ijk , q_jk ) ∪ (q_jk , 1, q_jk )
43: return $D = {Q, Q_{0}, Δ, Π = X \cup \bar{X} \cup Y, L, Γ_{q}}, Λ$

Algorithm 1 takes as input the synthesized automaton

A

, the set of initial environment configurations X ₀, the controller’s ranking function Γ, the set of sensor propositions

\bar{X}

, and probabilistic models of the environment and sensors, P(X′|X,Y) and

P (\bar{X}' | X', \bar{X}, Y)

, respectively. The output of this algorithm is the probabilistic model

D

of the system with sensor error, and a function Λ: Q→S that maps each state in the probabilistic model to its originating state in the synthesized automaton. The probabilistic model

D

is a DTMC, and contains a set of states Q, which are labeled (by the labeling function L) with subsets of the environment propositions

X

, sensor propositions

\bar{X}

, and robot propositions

Y

. The model also contains a set of initial states Q ₀, a probabilistic transition function Δ, and a new ranking function Γ_q. The resulting probabilistic model

D

includes transitions to incorrect states in the automaton as well as to states that were not in the synthesized controller, due to false positives and false negatives in the robot’s sensor propositions.

Consider the previously introduced scenario, where a robot moves through a doorway. The synthesized automaton, then, would include a state where the robot moves through the open door, and one where the robot waits at the closed door. In including the sensor error, Algorithm 1 would model not only if the door was open but also if the robot sensed that the door was open. The algorithm would create new states that include both the senor values and the state of the environment, and add transitions based on the specified probabilities. As a result, the model would include transitions to a state where the robot attempts to drive through a closed door (which it erroneously senses as open) and to a state where the robot mistakenly waits for the open door (which it senses as closed) to open, as well as to the correct states where it drives through the open door or waits for the closed door to open.

Intuitively, the algorithm loops through each state in the automaton s_i (line 3), and extracts the set of propositions for the environment X_i , which correspond to the incoming transitions (lines 4–8). The algorithm then adds a new state q_i to the probabilistic system, labeled with the environment–sensor–robot configuration $X_{i} \cup \bar{X_{i}} \cup Y_{i}$ , and with the appropriate rank Γ_q and automaton mapping Λ (lines 9–12). As each state is created, it is added to the set Q ^* of states for which the outgoing transitions are undefined (line 11). If the corresponding automaton state was an initial state, the new state is also added to the set of initial states for the probabilistic system (line 6).

While there are states in the set Q ^*, the algorithm selects one (q_i ∈ Q ^*) and removes it from the set (lines 13–14). It then extracts the appropriate labels for the environment X_i , sensors $\bar{X_{i}}$ , and robot Y_i , at that state (line 15). Lines 16 and 17 then loop through each allowable configuration of the environment X_j and sensors $\bar{X_{k}}$ , and the probability p_ijk of transitioning to those configurations is calculated in line 18.

If there exists some state s_k in the synthesized automaton such that there is a transition from s_i to s_k that is labeled with the given sensor values $\bar{X_{k}}$ , the robot configuration Y_k is extracted from that state (lines 19–20). If a state q_jk with the appropriate labels already exists in the probabilistic model, and that state corresponds to the automaton state s_k , a transition is created to it (lines 21–22); if no such state already exists, a new state is created and added to the set of states missing outgoing transitions Q ^*, and the appropriate transition is created in Δ (lines 23–27)

If there is no appropriate transition in the synthesized automaton (out of s_i ), then the algorithm looks for an identically labeled transition out of another state s_h , which shares the same configuration as s_i (line 28). If any such states exist, the algorithm takes the one with the most closely preceding goal rank Γ (line 29), and creates the appropriate transition. Again, if the destination state is already in the probabilistic system, the algorithm adds a transition to it (lines 30–31); if no such state exists, a new one is created and added to the set Q ^* (lines 32–36).

Finally, if there are no transitions in the synthesized automaton which match the considered labels, a sink state (with no outgoing transitions) is created, and a transition is added to that state (lines 37–42).

4.2. Actuator error

Algorithm 2 describes a similar process, which introduces the actuation error (in motion and non-motion actions) into the probabilistic model. This algorithm is adapted from that presented by Johnson and Kress-Gazit (2013), and is slightly modified to incorporate the actuation error into an existing DTMC, rather than creating a probabilistic model from the synthesized automaton. These modifications enable the algorithm to account for sensor configurations (in addition to environment and robot configurations), and to include the probabilities that were computed for each transition in Algorithm 1.

Algorithm 2. Include actuation error in the model.
1: procedure ActErr( $D = {Q, Q_{0}, Δ, Π, L, Γ_{q}}, X, \bar{X}, Y, Λ, P (Y' \| \bar{Y}', Y)$ )
2: Δ_Act = ∅
3: for (q_i , p_ij , q_j ) ∈Δdo
4: $X_{i} = L (q_{i}) \cap X, \bar{X_{i}} = L (q_{i}) \cap \bar{X}, Y_{i} = L (q_{i}) \cap Y$
5: $X_{j} = L (q_{j}) \cap X, \bar{X_{j}} = L (q_{j}) \cap \bar{X}, \bar{Y_{j}} = L (q_{j}) \cap Y$
6: for $Y_{k} \in 2^{Y} s . t . p (Y_{k} \| \bar{Y_{j}}, Y_{i}) > 0$ do
7: if $Y_{k} = \bar{Y_{j}}$ then
8: $Δ_{Act} = Δ_{Act} \cup (q_{i}, p_{ij} \cdot p (Y_{k} \| \bar{Y_{j}}, Y_{i}), q_{j})$
9: else if∃(q_h , q_k ) ∈Q×Q s.t. (q_h , p_hk , q_k ) ∈Δ and $L (q_{k}) = X_{j} \cup \bar{X_{j}} \cup Y_{k}$ then
10: $q_{l} = {argmin}_{q_{k}} ((Γ_{q} (q_{j}) - Γ_{q} (q_{k})) modulo \max_{q \in Q} (Γ_{q} (q)))$
11: $Δ_{Act} = Δ_{Act} \cup (q_{i}, p_{hl} \cdot (Y_{k} \| \bar{Y_{j}}, Y_{i}), q_{l})$
12: else
13: $L (q_{jk}) = X_{j} \cup \bar{X_{j}} \cup Y_{k}$
14: Q = Q ∪ q_jk
15: Λ(q_jk ) = Λ (q_j )
16: $Δ_{Act} = Δ_{Act} \cup (q_{i}, p_{ij} \cdot p (Y_{k} \| \bar{Y_{j}}, Y_{i}), q_{jk})$
17: Δ_Act = Δ_Act ∪ (q_jk , 1, q_jk )
18: return $D = {Q, Q_{0}, Δ_{Act}, Π, L, Γ}, Λ$

The inputs to the algorithm are the DTMC $D$ of the probabilistic model with sensor error (from Algorithm 1), the sets of environment $X$ , sensor $\bar{X}$ , and robot $Y$ propositions, the function Λ that maps states in $D$ to states in $A$ , and the probabilistic model of the actuation error $P (Y' | \bar{Y}', Y)$ . The outputs of the algorithm are the adjusted probabilistic model $D$ , which includes actuation error in addition to sensor error, and the expanded automaton–state mapping function Λ. The new probabilistic model includes new states and new transitions that are a result of unintended changes in the state of the robot.

Consider, again, the scenario where a robot is required to pass through a doorway, when open. The probabilistic model that results from Algorithm 2 would now include the possibility of the robot attempting and failing to exit through the door when it senses that it is open. This involves the creation of new states, in which the robot attempts and fails to move through a doorway it senses to be open. If such states are not planned for in the automaton, they result in deadlock states in the probabilistic model (no outgoing transitions).

This algorithm proceeds by looping through each transition in the input DTMC (line 3) and extracting the propositions associated with each state in the transition (lines 4–5). It then loops through each robot configuration that is a possible outcome of the attempted transition (line 6) and, if that outcome is the intended one, it adjusts the probability of the transition according to the actuation error model, and stores the transition in the new transition function Δ_Act (lines 7–8). Otherwise, if the outcome is not the intended one, but matches another state in the system, a new transition is created to the matching state with the most closely preceding goal (lines 9–11). Finally, if no such state exists in the system, a new one is created and added to the system (lines 12–16); in addition, this new state is set to be a sink state, which transitions to itself with probability 1 (line 17).

4.3. Model analysis

The model $D$ that is the output of Algorithm 2 is a discrete-time model that describes the probabilistic behavior of the robot, which is controlled by the synthesized automaton $A$ and operating with imperfect sensors and actuators. This model can be analyzed with respect to various LTL formulas as described in Johnson and Kress-Gazit (2011, 2012, 2013). These formulas may be any valid LTL formula describing the behavior of the robot, and are not restricted to the original task specification. Typically, these formulas are used to compute the probability that the robot exhibits a particular behavior in response to changes in the robot’s environment.

As in the previous papers, the PRISM probabilistic model checker (Kwiatkowska et al., 2011) was used to find the probabilities used for the analysis presented in Section 6. It was also used to perform the model-checking functionality in Algorithms 3 –6. The PRISM model checking software is available online at http://www.prismmodelchecker.org/.

Algorithm 3. Suggest additional safety requirements.
1: procedure SafetyRevs( $D = {Q, Q_{0}, Δ, X \cup \bar{X} \cup Y, L, Γ}$ , ϕ, N_max )
2: $Q_{goal} = {q \in Q : Γ (q) \neq Γ (q') \forall q' s . t . (q, \cdot, q') \in Δ}$
3: Q_deadlock = {q∈Q : (q, 1, q) ∈Δ}
4: Q_check = Q \ (Q ₀ ∪ Q_goal ∪ Q_deadlock )
5: for N = 0: N_max do
6: Q ^* = ∅
7: for q_i ∈Q_check do
8: $D_{i} = {Q, q_{i}, Δ, X \cup \bar{X} \cup Y, L, Γ}$
9: φ = ¬ϕ∧t = N
10: p← ModelCheck $(D_{i}, φ)$
11: if p > 0 then
12: Q ^* = Q ^* ∪ (q_i , p)
13: $Y'_{T} = Y'_{F} = Y; X'_{T} = X'_{F} = X; Ψ = \emptyset$
14: while Q^* ≠∅and Y′_T ∪ Y′_F≠∅do
15: $(q_{j}, p) = {argmax}_{(q_{i}, p) \in Q^{*}} (p)$
16: $Y'_{T} = Y'_{T} \cap L (q_{j}); Y'_{F} = Y'_{F} ∖ L (q_{j})$
17: $X'_{T} = X'_{T} \cap L (q_{j}); X'_{F} = X'_{F} ∖ L (q_{j})$
18: if Y′_T ∪ Y′_F≠∅then
19: $ψ = □ ((\underset{x \in X'_{T}}{⋀} ◯ x \land \underset{x \in X'_{F}}{⋀} \neg ◯ x)$ $\to \neg (\underset{y \in Y'_{T}}{⋀} ◯ y \land \underset{y \in Y'_{F}}{⋀} \neg ◯ y))$
20: if ψ∉Ψthen
21: Ψ = Ψ ∪ {ψ}
22: Q ^* = Q ^\ (q_j* , p)
23: ifΨ≠∅then
24: returnΨ
25: return∅

Algorithm 4. Suggest a restriction of the initial state.
1: procedure InitRevs( $D = {Q, Q_{0}, Δ, X \cup \bar{X} \cup Y, L, Γ}, ϕ$ )
2: P = ∅
3: for q ₀∈Q ₀ do
4: $D_{0} = {Q, q_{0}, Δ, X \cup Y, L, Γ}$
5: p← ModelCheck $(D_{0}, ϕ)$
6: $l = L (q_{0}) \cap Y$
7: P = P∪ (p, l)
8: $(p^{}, l^{}) = {argmax}_{(p, l) \in P} [{mean}_{(p', l') \in P \| l' = l} (p')]$
9: $ψ = \underset{y \in l^{}}{⋀} y \land \underset{y \in Y ∖ l^{}}{⋀} \neg y$
10: return ψ

Algorithm 5. Suggest revisions to the low-level components (abstract actuators/sensors).
1: procedure HWRevs( $D = {Q, Q_{0}, Δ, X \cup \bar{X} \cup Y, L, Γ},$ ϕ, P(·))
2: p← ModelCheck $(D, ϕ)$
3: P_δ = ∅
4: for p(·) ∈P(·) do
5: Δ_δ← replace p(·) with p(·) +δ for all p(·) ∈Δ
6: $D_{δ} = {Q, Q_{0}, Δ_{δ}, X \cup Y, L, Γ}$
7: p_δ ← ModelCheck $(D_{δ}, ϕ)$
8: P_δ = P_δ ∪ (p_δ , p(·))
9: $(p_{δ}^{}, p {(\cdot)}^{}) = {argmax}_{(p_{δ}, p (\cdot)) \in P_{δ}} (p_{δ} - p)$
10: return p(·)^*

Algorithm 6. Suggest removal of liveness condition.
1: procedure LivenessRevs( $D = {Q, Q_{0}, Δ, X \cup \bar{X} \cup Y, L, Γ}$ ,ϕ)
2: P_g = zeros(Γ_max)
3: for q_j ∈Q do
4: $φ = φ U (! ϕ \land ◯ q = q_{j})$
5: p← ModelCheck $(D, φ)$
6: P_g [Γ(q_j )] = P_g [Γ(q_j )]+p
7: $γ^{*} = {argmax}_{γ \in 1 : \| P_{g} \|} (P_{g} \| γ \|)$
8: return γ*

5. Revision suggestion

An overview of the presented approach for generating revision suggestions is shown in Figure 2. After composing a probabilistic model of the system, as described in Section 4, the model is analyzed with a probabilistic model checker, and used to provide feedback to the user in the form of an additional safety specification, a restriction on the initial condition, a low-level component to refine, or a liveness specification to remove.

Fig. 2.

Diagram of the presented approach for providing feedback to the user in the form of an additional safety specification, a restriction on the initial condition, a low-level component to refine, or a liveness specification to remove.

5.1. Safety specification revisions

Algorithm 3 describes the process used to provide specification revisions in the form of additional safety formulas ( $φ_{t}^{s}$ ) to be added to the original task specification. The inputs to the algorithm are the probabilistic system $D$ , a formula ϕ, and a maximum number of steps to check N_max . The formula ϕ is a Boolean formula over $X \cup Y \cup ◯ X \cup ◯ Y$ , which represents a desired behavior for the robot (typically, this takes the form of a conjunction of safety formulas, less the □ operator). Here N_max determines the maximum number of steps ahead of each state the algorithm will check for violations of the specification ϕ; the value of N_max serves as a termination criterion for the algorithm in the case that it is unable to find a suitable revision formula. The output of this algorithm is a set of safety formulas Ψ, which may be added to the original specification to modify the robot behavior.

Returning to the example scenario of a robot attempting to move through an open door, consider a situation in which there are two doorways that lead out of the room. If one of those doorways opens and closes more frequently, Algorithm 3 may detect that attempting to move through that doorway is the most likely source of collisions with a closed door, and return a revision suggestion that requires the robot to always avoid using that particular doorway.

The algorithm proceeds, first, by computing the set of goal states (where the robot satisfies a liveness condition and begins working towards the next one, line 2), and the set of deadlock states (where the robot has no transitions out of that state, line 3). The algorithm then reduces the set of states to check Q_check (line 4) to only those states that are not initial states (which are considered in Algorithm 4), goal states (which are considered in Algorithm 6), or deadlock states (which are either sink states that are not in the synthesized automaton, or are goal states).

Next, beginning with a value of N = 1, and increasing incrementally, the algorithm loops through each state in the system (lines 5–7). It then sets the initial state of the model to be the current state, and checks for the probability that the model violates ϕ in exactly N steps (lines 8–10). If the calculated probability is non-zero, it adds the state/probability pair to the list Q ^*.

After this is completed for each state in the system, the algorithm initializes a set of propositions to track which robot and environment propositions are true or false, in an incrementally increasing set of states (line 13). It then loops through the state/probability pairs in Q ^*, and chooses the one with the highest probability of violating ϕ in N steps (lines 14–15). In lines 16–17, the algorithm reduces each set of propositions to only those propositions which match the value in the current state (i.e. a proposition is removed from X′_T or Y′_T if it is false in the current state, and removed from X′_F or Y′_F if it is true in the current state). The resulting lists contain exactly the set of propositions that have a consistent value (true or false) over every state that is pulled from the list Q ^*.

After each set is reduced for the current state, if the set of robot propositions (either true or false) are non-empty, a formula ψ = □(◯X′→¬◯Y′) is created (lines 18–19), such that if the environment propositions take the values stored in the lists X′_T and X′_F, the robot is required to avoid the configuration stored in the lists Y′_T and Y′_F. If this equation ψ is not already in the list of safety revisions Ψ, then it is added (lines 20–21). The current state/probability pair is then removed from the list Q ^* (line 22), and the algorithm continues the while-loop.

After each value of N is checked, if one or more revisions has been found, the algorithm returns the set of LTL formulas Ψ (lines 23–24). If no revisions have been found for the current value of N, the algorithm increments the value and repeats the process. If no results are found for any value 0 ≤ N ≤ N_max , the algorithm terminates with no revisions (line 25).

The set Ψ that is output by Algorithm 3 is a set of LTL safety formulas that may be added to the original specification, to force the synthesized controller to avoid a certain behavior that is exhibited by the set of state-pairs used to create the formula. The first formula added to the set is the most specific (it corresponds to avoiding a single transition in the original automaton) and each subsequent formula becomes progressively more general (corresponding to avoiding progressively larger sets of transitions).

5.2. Initial-state revisions

Another type of automated feedback is described in Algorithm 4, which provides specification revisions in the form of restrictions on the initial configuration of the robot ( $φ_{i}^{s}$ ). The inputs to this algorithm are the probabilistic model of the system $D$ and the LTL formula ϕ describing the desired behavior of the robot. Unlike in Algorithm 3, this formula is not restricted beyond being an LTL formula over the set of propositions $X \cup Y$ . The output of Algorithm 4 is a Boolean formula ψ over the propositions in $Y$ , which describes the best initial configuration of the robot, from the set of possible initial states.

Algorithm 4 proceeds by looping through each initial state q ₀ ∈ Q ₀ and restricting the probabilistic system to only that initial state (lines 3–4). The algorithm then uses the probabilistic model checker to find the probability that this restricted system satisfies the desired behavior ϕ (line 5). This probability, along with the robot labels on the initial state, are stored in the set P (lines 6–7). After this process is completed for each initial state, the algorithm finds the stored pair with the highest average probability over all elements in the set which share the same labels (line 8). These labels are then used to create a Boolean formula ψ over the set of propositions $Y$ , which restricts the initial robot configuration to a single set of values (line 9).

The formula ψ that is created by Algorithm 4 can be added to the set of specifications for the robot’s initial configuration $φ_{i}^{s}$ to improve the overall behavior of the robot (with respect to the input formula ϕ), by restricting the initial state of the robot to the single configuration that has the highest probability of satisfying ϕ. It should be noted that this algorithm does not attempt to restrict the initial configuration of the environment, which is assumed to be outside of the user’s control. Furthermore, if the set of initial states Q ₀ does not contain multiple states, with different robot configurations, including ψ in the synthesis specifications will have no effect (as the initial configuration is already restricted to that valuation).

5.3. Low-level component revisions

The third type of automated revision presented in this paper is that of suggesting revisions to a low-level component that is represented by one of the abstract propositions that are used to represent the robot’s sensing or actuation. Algorithm 5 describes the process used to perform a sensitivity analysis on the low-level components, and identify the component ( $p (\cdot) \in P (\cdot) \subseteq P (\bar{X}' | X', \bar{X}, Y) \cup P (Y' | \bar{Y}', Y)$ ) for which the robot is most sensitive to improvements in performance. The inputs to the algorithm are the probabilistic system $D$ , the desired behavior ϕ (which, like in Algorithm 4, can be any LTL formula over the propositions in $X \cup Y$ ), and the set of low-level component probabilities to be analyzed P(·). In addition, a parameter δ must be defined for the small variation applied to each of the low-level component probabilities; this value is used to approximate the rate of change in the probabilistic behavior with respect to the component probabilities. The output of the algorithm is the single low-level (actuation or sensing) component that, if improved, would have the largest positive impact on the behavior of the robot (with respect to ϕ). This component could be improved separately by the user, by making changes to the underlying abstraction or algorithms, or by investing in more accurate hardware.

Algorithm 5 first finds the probability that the nominal model satisfies the input formula ϕ (line 2). It then loops through each low-level component p(·) ∈ P(·) and modifies the transition function in the original model by replacing each occurrence of p(·) with a slightly higher value p(·) + δ, and adjust the other probabilities in Δ accordingly (lines 4–5). The system model is then adjusted for the new transition function, and checked to find the probability that it satisfies the desired behavior ϕ (lines 6–7). The probability, along with the component that was adjusted, is then stored in the set P_δ (line 8). Finally, the algorithm finds the probability/component pair with the largest increase in probability (over the nominal), and returns that component to the user (lines 9–10).

5.4. Liveness condition revisions

The final automated revision discussed in this paper is the identification of a specific liveness condition from the set of liveness formulas ( $φ_{g}^{s}$ ), in pursuit of which the robot is most likely to exhibit an undesirable behavior. Algorithm 6 describes this process, where the inputs to the function are the probabilistic system $D$ , and the desired behavior ϕ. As in Algorithm 3, the desired behavior ϕ is restricted to a Boolean formula over $X \cup Y \cup ◯ X \cup ◯ Y$ . The output of this algorithm is the index γ ^* of the liveness condition which is most likely to result in a violation of the desired behavior ϕ.

This algorithm begins by creating a set of probabilities (initialized to 0) to track the probability that the robot violates ϕ while pursuing each particular goal (line 2). It then loops through each state q_j in the system, and finds the probability that the first time the robot violates ϕ is while transitioning to that state (lines 3–5). This value is then added to stored value that corresponds to the goal being pursued in state q_j (line 6). The algorithm then returns the goal index γ ^* that has the largest stored value for the probability of causing the initial violation of ϕ (lines 7–8). Note that, because the formula φ that is being analyzed finds the probability that each state is the first to violate ϕ, the sum of all entries in P_g will be no greater than 1.

5.5. Notes on revision suggestions

Algorithms 3 –6 describe four complimentary methods for providing feedback to the user in the form of suggested changes to the task specification or low-level components. It should be noted, however, that the suggested safety revisions (Algorithm 3) and the suggested liveness revisions (Algorithm 6) are not guaranteed to result in an improvement of the behavior of the robot. In each case, the suggested revision would alter the behavior of the robot by prohibiting the current most problematic behavior or by removing a behavior that leads to violation of the specifications. Synthesizing a new controller with the suggested revision will change the behavior of the robot, and may be probabilistically worse than the behavior being avoided by the revision. In addition, the addition of a new safety specification may even cause the overall specification to become unsynthesizable. As an example, consider a scenario where the robot must advance down a corridor to reach its goal; if the safety revision identifies this corridor as the most likely source of error (and therefore suggests avoiding it), and there is no other route to the robot’s goal, the resulting specification (after including this revision) would become unsynthesizable. Such an error would be identified by the synthesis algorithm, after the revision was included in the specification.

It is also worth noting that the removal of a liveness condition represents a more significant change in the original specification than the introduction of a safety specification (Algorithm 3) or a restriction of the initial condition (Algorithm 4). In this case, the revision causes a change in the task goals, and so must be handled with care. As such, it is typically better to revise the controller as described in Sections 5.1–5.3 prior to removing a liveness condition from the original task specification. The dramatic impact of such a change also underlines the value of keeping the user involved in the revision process, as an automation of this process would converge to a specification without any liveness conditions, where the robot could easily satisfy the specifications without needing to act.

In addition, note that there is a restriction on the formula ϕ (for the desired behavior) in Algorithms 3 and 6, where ϕ is restricted to a Boolean formula over $X \cup Y \cup ◯ X \cup ◯ Y$ . This restriction is because these two algorithms involve steps where the model checker is used to find the probability that a state-pair satisfies the formula (rather than the probability over the full model). As such, the restricted form of ϕ ensures that the desired behavior is defined only over pairs of states. Because these algorithms identify the state pairs that are most likely to violate ϕ, the resulting revision is akin to finding the revision which maximizes the probability that the robot satisfy a safety formula of the form □ϕ.

Finally, it should be noted that one can easily automate the process of adding or removing specification revisions and synthesizing a new controller, which can be used to create a new probabilistic model; the probabilistic performance of the new model can then be assessed in comparison to the original model, to determine whether the revision results in an improvement in performance. This can then be used to automatically compare and prioritize the different types of revisions and provide the user with only those which provide a significant improvement in the behavior of the robot (as well as to disregard any revisions that would cause the specification to become unsynthesizable). The authors have, in fact, implemented such functionality, although it is not discussed in detail in this paper.

In terms of computation, the most expensive part of each of these algorithms is that of model checking a probabilistic model to find the probability that it satisfies an LTL formula. Such LTL model checking is, in general, exponential in the size of the formula and polynomial in the size of the given model (Courcoubetis and Yannakakis, 1995). As such, Algorithms 3 and 6 are typically the most time consuming to run, as they usually require the most calls to the “ModelCheck” function. Compared with model checking, the other calculations in each of the algorithms have negligible computational costs. In the cases of Algorithms 3 and 6, this corresponds to a call to “ModelCheck” for nearly every state in the model. Such a process is computationally expensive for most realistic problems; the impact of this expense is reduced, however, due to the offline nature of each of these algorithms, which are meant to be run prior to deployment of the robot. A discussion of the run-times of the algorithms for an example problem is included in Section 6.

6. Example

Scenario. In this example, the robot is tasked with continuously visiting three different regions (labeled G ₁, G ₂, and G ₃ in Figure 3), while avoiding an adversarial robot that patrols the five regions in the middle of the map (R ₁–R ₅ in the figure). The robot can (imperfectly) sense the location of the adversarial robot, and (imperfectly) move between adjacent regions in the map. Note that the presented example only involves motion actions (i.e. changes in the robot’s region), though the approach can also include other abstract robot actions.

Fig. 3.

Discretized map of the workspace for the example problem.

A subset of the LTL formulas used to synthesize the controller are given below, where $A_{R_{i}}$ is an environment proposition describing the location of the adversary. The first formula specifies that the adversary can only transition between adjacent regions, while the second formula requires that the robot avoid being in the same region as the adversary. The final equation specifies the goals for the robot: repeatedly visiting regions G ₁, G ₂, and G ₃.

$□ \underset{i \in {1 : 5}}{⋀} (A_{R_{i}} \to \underset{j \in {i - 1 : i + 1}}{⋁} ◯ A_{R_{j}})$ ;

$□ \underset{i \in {1 : 5}}{⋀} (◯ A_{R_{i}} \to \neg ◯ R_{i})$ ;

□♢G ₁∧□♢G ₂∧□♢G ₃.

The synthesized controller has 75 states, with the initial state of the robot being restricted to G ₁, G ₂, or G ₃. When moving from G ₁ to G ₂, the robot traverses through region R ₁ when the adversary is in regions R ₂–R ₅ and through region R ₂ when the adversary is in region R ₁. When moving to and from G ₃, the robot waits until the adversary traverses to R ₁ or R ₂ before entering regions R ₃–R ₅. If the sensing of the adversary’s location and the movement of the robot both execute without failure, the synthesized controller is guaranteed to satisfy the specified behavior; if the robot operates imperfectly, however, it may end up in the same region as the adversary, violating the specification.

Probabilities. In this example, the movement of the adversarial is modeled such that it has a 0.25 probability of staying in its current region on any step, and a 0.75 probability of moving to one of the adjacent regions (split evenly among the adjacent regions). The nominal model of the robot’s sensors and actuators are such that the robot has a 0.9 probability of correctly determining the location of the adversary (with the remaining 0.1 being split between the regions adjacent to the actual location of the adversary) and a 0.9 probability of moving to the intended next region (with a 0.1 probability of erroneously remaining in its current region).

Analysis. Figure 4 shows the resulting probability that the robot will avoid the region with the adversary, over a time bound of 25 discrete transitions. The probability that the robot correctly sensed the location of the adversary and the probability that the robot moved to its intended next region were each independently varied between 0 and 1, and in each case the other probability was held constant at the nominal probability of 0.9. The model was analyzed to find the probability that the robot satisfied the LTL formula

□ (\underset{i \in {1 : 5}}{⋀} \neg (◯ A_{R_{i}} \land ◯ R_{i}))

(3)

Fig. 4.

Analysis results for the adversarial robot example: probability that the robot avoids the adversary.

These results show that, as the probability that the robot correctly senses the location of the adversary increases, the robot will be more likely to avoid the unwanted contact with the adversary. Owing to the other error present in the model (the motion of the robot), even when the sensor is perfect (i.e. it has a probability of 1.0 of correctly detecting the location of the adversary) the robot has a less than perfect probability of avoiding the adversary over the time bound (0.933).

When analyzed over a range of values for the probability that the robot correctly moves when directed to do so by the automaton, the resulting probabilities show that when the robot can never move correctly it will always avoid the adversary. This can be attributed to the fact that the robot will be completely unable to move and will simply remain in region G ₁ where it cannot encounter the adversary, but it will be unable to satisfy its goals. As the likelihood that the robot moves correctly increases (until about 0.4), this probability decreases, before rising again to a value of 0.891 when the robot moves without error. This behavior is due to the additional time required for the robot to reach a dangerous region when the probability of correctly moving is low; if the robot does not move into the central regions (where the adversary patrols), it will not violate the analyzed formula.

By contrast, Figure 5 shows the probability that the robot satisfies all three of the goals at least once, within the given time bound. In this case, the model was analyzed to find the probability that the robot satisfied the following formula:

♦ G_{1} \land ♦ G_{2} \land ♦ G_{3}

(3)

Fig. 5.

Analysis results for the adversarial robot example: probability that the robot satisfies all three goals within the time bound.

Figure 5 shows that, due to the likelihood that the robot remains stopped for long portions of time, low probabilities on the motion of the robot result in low likelihoods of satisfying all three goals. By contrast, errors in the sensing of the location of the adversary have relatively little effect on the likelihood that the robot satisfies each of its goals at least once; in this case, the sensor error prevents the robot from satisfying its goals only when causing it to enter deadlock states, for which the synthesized controller has no prescribed transition. This is unlike the first specification that was analyzed (i.e. Figure 4), and illustrates how, due to the complex behaviors exhibited by the controller, different aspects of the task specification can be affected differently by the sensing and actuation errors.

Revisions. In addition to the above analysis, Algorithms 3 –6 were used to find revisions to the task specification and lower-level components for this example. In each case, the analysis focused on the safety specifications for the robot, requiring that it avoid being in the same region as the adversary.

To find safety revisions for the controller specification, the specified undesirable behavior was given by the formula $ϕ = \underset{i \in {1 : 5}}{⋀} (A_{R_{i}} \land R_{i})$ , describing the situation in which the robot enters the same region as the adversary. Algorithm 3 was then run with a maximum step value of N_max = 5, which was sufficient to find a safety revision before terminating. The resulting safety revision found by the algorithm ( $□ (◯ \neg A_{R_{1}} \land ◯ \neg A_{R_{2}} \land ◯ \neg A_{R_{4}}) \to ◯ \neg R_{4}$ ), when included in the original specification, requires that the robot avoid region R ₄ while the adversary is in R ₃ or R ₅. The new controller results in an increase of 0.10 (at the nominal model probabilities) in the probability that the robot always satisfies the formula ϕ within the time bound. Figure 6 shows the probability that the robot satisfies $□ (\underset{i \in {1 : 5}}{⋀} \neg (◯ A_{R_{i}} \land ◯ R_{i}))$ for the original (solid lines) and revised (dashed lines) controllers. The results shown in this figure show an improvement in the behavior of the robot for all model probabilities close to the nominal values. Furthermore, this process can be repeated to find additional safety revisions for the controller (iteratively adding each revision and re-synthesizing the controller). Doing so after including this safety revision would likely result in a similar revision for another region (e.g., avoiding R ₃ when the adversary is in R ₂ or R ₄).

Fig. 6.

Analysis results for the revised controller in the adversarial robot example: probability that the robot avoids the adversary.

An initial state revision (Algorithm 4) was found for the formula $ϕ = □ \underset{i \in {1 : 5}}{⋀} \neg (A_{R_{i}} \land R_{i})$ , requiring that the robot never end up in the same region as the adversary. The resulting revision to the initial condition ψ = G ₃ specifies that the robot is most likely to succeed over the analyzed time bound (25 discrete transitions) when the robot starts in region G ₃. At the nominal model probabilities, Algorithm 4 found that the likelihood of satisfying ϕ from an initial state in G ₃ was 0.8697, while the robot had probabilities of 0.8225 and 0.8160 of satisfying ϕ when beginning in regions G ₂ and G ₁, respectively. This result is due to the process of traveling to region G ₃ being more likely to cause a failure than the process of leaving G ₃; as such, by beginning in G ₃, the robot is more likely to avoid that entry corridor within the analyzed time-bound. The difference between entering and exiting the corridor to region G ₃ is due to when the synthesized controller transitions into the corridor, rather than the actual path itself (which passes through the same regions in either case). When the robot is entering the corridor to G ₃, it may move to R ₃ while the adversary is in R ₂, before moving to R ₄ as the adversary moves to R ₃. In contrast, when leaving G ₃, the synthesized controller will only enter region R ₄ or R ₅ if the robot senses the adversary is in region R ₁ or R ₂. The result of these different behaviors is that the robot stays further away from the adversary when exiting G ₃ than when entering it, thereby reducing the probability that it ends up in the same region as the adversary and violates the specification.

Algorithm 5 was used to perform a sensitivity analysis on the low-level components for sensing the location of the adversary, and the motion of the robot. As before, the formula $ϕ = □ \underset{i \in {1 : 5}}{⋀} \neg (A_{R_{i}} \land R_{i})$ was tested against, requiring that the robot never end up in the same region as the adversary. The resulting analysis revealed that improvements to the robot’s sensing would have a greater positive impact on the overall performance of the robot than would improvements to the robot’s motion. This is unsurprising, given the results shown in Figure 4, which show a greater upward slope (at the nominal point) for the line representing changes in sensor accuracy.

Finally, Algorithm 6 was used to find the specified goal in pursuit of which the robot was most likely to violate $ϕ = \underset{i \in {1 : 5}}{⋀} (A_{R_{i}} \land R_{i})$ by finding itself in the same region as the adversary. The result of Algorithm 6 found that the robot was most likely to violate ϕ while pursuing its third goal □♢G ₃ (with a probability of 0.4998), than while pursuing either of its first two goals (probabilities of 0.2505 and 0.2164 for □♢G ₁ and □♢G ₂, respectively). Given the layout of the workspace (shown in Figure 3), this is unsurprising, as the robot must traverse through several dangerous regions when attempting to move to region G ₃. Note that, because the analysis is performed for a bounded time frame, there is a positive probability that the robot will successfully avoid the adversary for the entire time bound, and the sum of the probabilities of failure for the goals is less than 1.

Each of the revision methods presented in Section 5 gives, for this example, a revision suggestion that results in an improvement in the behavior of the robot. In fact, multiple revisions could be included simultaneously to have a greater impact on the behavior of the robot. In doing so, it is important to consider the effects of each revision. For example, if one were to remove the third liveness condition they would likely not want to restrict the initial condition of the robot to G ₃, as the removal of the liveness condition removes the need to use that dangerous corridor at all, unless the robot were to start in region G ₃.

Computation. For this paper, the authors used a Python implementation of the algorithms described in Sections 4 and 5, running on a Windows desktop PC. The computer has a 3.5 GHz, Intel Core i7 processor, with 16 GB of RAM. The “ModelCheck” step in Algorithms 1 –6 was conducted with a command-line call to the PRISM probabilistic model check, running version 4.2 of PRISM. Table 1 shows a comparison of the number of states (in the automaton and in the composed probabilistic model) and the computation times for the example problem, as well as for instances of the same problem where the number of adversary-accessible regions (the centrally located regions in Figure 3, R ₁–R ₅) is reduced to three regions, and increased to eight regions. The state sizes and computations time for the nominal example, discussed previously, are shown in bold.

Table 1.

Comparison of model sizes and computation times of Algorithm 3. The supplied example is compared with identical problems where the number of adversary-accessible regions (in the center of the map in Figure 3) has been increased and decreased.

Number of adversary regions	Number of states in the automaton	Number of states in the DTMC	Computation time (seconds)
3	37	85	23
5	75	196	475
8	153	422	3526

As can be seen in this table, variations in the number of adversary-accessible regions has a significant effect on the problem size. More importantly, changes in the size of the synthesized controller have a dramatic effect on the size of the composed model (which adds states to the model, in order to account for errors in the robot’s sensing and actuation), and, in turn, the computation time required. By increasing the number of adversary-accessible regions in the example problem from five to eight, the computation time required to find a safety revision increased from 475 seconds to 3526 seconds.

Owing to the offline nature of the algorithms, such computation times are not prohibitive, though they are noteworthy. The authors have successfully analyzed problems that have over 4000 states in the automaton and nearly 25,000 states in the probabilistic model; for such a model, model checking a formula for an initial state of the system required 28 seconds. When creating revisions, this constitutes the “ModelCheck” step of Algorithms 3 –6 and must be applied to most of the states in the model. This process could be parallelized to reduce the computational burden.

7. Conclusion

This paper presents a method for accounting for errors in the sensing and actuation of mobile robots, when controlled by a correct-by-construction automaton that is synthesized from a set of high-level task specifications. The paper discusses the composition of a DTMC model of the system, which includes the probabilistic errors in sensing and actuation, and the analysis of that model with respect to a set of LTL formulas.

Furthermore, four complementary methods are given for providing feedback to the user in a semi-automated fashion. By adding safety specifications, restricting the initial state of the robot, improving the performance of a particular low-level component, or removing a particularly troublesome liveness condition, the user may be able to improve the overall performance of the robot when operating with the modeled error.

The presented approach seeks to advance the field of synthesized robot controllers by relaxing the standard assumption of perfect sensing and actuation. Future work by the authors will focus on improving the revision process, and on incorporating the system uncertainty in the synthesis process to yield a correct-by-construction controller that is more robust to errors in sensing and actuation.

The current implementation of this work is computationally intensive for realistically large problems; this problem is somewhat alleviated by the offline nature of the algorithms, as the computation time is less of a concern than for online algorithms. Future implementations of this work may partially alleviate the computational issues in several different ways. One such method would be to parallelize the “ModelCheck” step in the revision algorithms; this process could be easily parallelized, since each call to the model checker is completed independently of the others, and would save computation time for large problems. Another way to improve the computational efficiency of the algorithms might be through additional reduction of the set of model states that must be checked. Because the “ModelCheck” step is, by far, the most expensive part of the algorithms, a reduction in the number of states to check would have a significant impact on the overall computation time required by the algorithm.

Footnotes

Funding

This work was supported by NSF (grant number CNS-0931686) and DARPA (grant number N66001-12-1-4250).

References

Bhatia

Kavraki

Vardi

(2010) Sampling-based motion planning with temporal goals. In: IEEE international conference on robotics and automation (ICRA). IEEE, pp. 2689–2696

Cizelj

Belta

(2013) Negotiating the probabilistic satisfaction of temporal logic motion specifications. In: IEEE international conference on intelligent robots and systems (IROS).

Conner

Kress-Gazit

Choset

Rizzi

(2007) Valet parking without a valet. In: Proceedings of IEEE/RSJ, pp. 572–577.

Courcoubetis

Yannakakis

(1995) The complexity of probabilistic verification. Journal of ACM 42(4): 587–907.

Ding

Smith

Belta

Rus

(2011) LTL control in uncertain environments with probabilistic satisfaction guarantees. In: 18th IFAC world congress.

Ding

Wang

Lahijanian

Paschalidis

Belta

(2012) Temporal logic motion control using actor–critic methods. In: 2012 IEEE international conference on robotics and automation. IEEE, pp. 4687–4692.

Emerson

(1990) Temporal and Modal Logic (Handbook of Theoretical Computer Science, vol. B). Cambridge, MA: MIT Press, pp. 995–1072.

Fainekos

(2011) Revising temporal logic specifications for motion planning. In: 2011 IEEE international conference on robotics and automation (ICRA). IEEE, pp. 40–45.

Fainekos

Girard

Pappas

(2007) Hierarchical synthesis of hybrid controllers from temporal logic specifications. In: Hybrid Systems: Computation and Control. New York: Springer, pp. 203–216.

10.

Fainekos

Kress-Gazit

Pappas

(2006) Hybrid controllers for path planning: a temporal logic approach. In: Proceedings of the 44th IEEE conference on decision and control, pp. 4885–4890.

11.

Johnson

Havlak

Campbell

Kress-Gazit

(2012) Execution and analysis of high-level tasks with dynamic obstacle anticipation. In: IEEE international conference on robotics and automation (ICRA).

12.

Johnson

Kress-Gazit

(2011) Probabilistic analysis of correctness of high-level robot behavior with sensor error. In: Proceedings of robotics: science and systems, Los Angeles, CA, USA.

13.

Johnson

Kress-Gazit

(2012) Probabilistic guarantees for high-level robot behavior in the presence of sensor error. Autonomous Robots 33: 309–321.

14.

Johnson

Kress-Gazit

(2013) Analyzing and revising high-level robot behaviors under actuator uncertainty. In: IEEE International conference on intelligent robots and systems (IROS).

15.

Karaman

Frazzoli

(2009) Sampling-based motion planning with deterministic μ -calculus specifications. In: IEEE conference on decision and control, pp. 2222–2229.

16.

Kim

Fainekos

Sankaranarayanan

(2012) On the revision problem of specification automata. In: Proceedings of the IEEE conference on robotics and automation.

17.

Kloetzer

Belta

(2006) A fully automated framework for control of linear systems from LTL specifications. Hybrid Systems: computation and control 3927: 333–347.

18.

Kress-Gazit

Fainekos

Pappas

(2007a) From structured English to robot motion. In: IEEE/RSJ international conference on intelligent robots and systems, 2007 (IROS 2007), pp. 2717–2722.

19.

Kress-Gazit

Fainekos

Pappas

(2007b) Where’s Waldo? Sensor-based temporal logic motion planning. In: 2007 IEEE international conference on robotics and automation, pp. 3116–3121.

20.

Kress-Gazit

Fainekos

Pappas

(2009) Temporal-logic-based reactive mission and motion planning. IEEE Transactions on robotics 25(6): 1370–1381.

21.

Kwiatkowska

Norman

Parker

(2011) PRISM 4.0: verification of probabilistic real-time systems. In: Proceedings of the 23rd international conference on computer aided verification (CAV’11) (Lecture notes in computer science, vol. 6806). New York: Springer, pp. 585–591.

22.

Kwiatkowska

Parker

(2012) Advances in probabilistic model checking. Software Safety and Security - Tools for Analysis and Verification 33: 126–151.

23.

Lahijanian

Andersson

Belta

(2009) A probabilistic approach for control of a stochastic system from LTL specifications. In: IEEE conference on decision and control, Shanghai, P.R. China, pp. 2236–2241.

24.

Lahijanian

Wasniewski

Andersson

Belta

(2010) Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees. In: 2010 IEEE international conference on robotics and automation (ICRA), Anchorage, AK, pp. 3227–3232.

25.

Loizou

Kyriakopoulos

(2004) Automatic synthesis of multi-agent motion tasks based on LTL specifications. In: IEEE conference on decision and control, Vol. 1. IEEE, pp. 153–158.

26.

Lyons

Arkin

Nirmal

Jiang

Liu

Deeb

(2013) Getting it right the first time: robot mission guarantees in the presence of uncertainty. In: IEEE international conference on intelligent robots and systems (IROS).

27.

Medina Ayala

Andersson

Belta

(2012) Probabilistic control from time-bounded temporal logic specifications in dynamic environments. In: 2012 IEEE international conference on robotics and automation. IEEE, pp. 4705–4710.

28.

Piterman

Pnueli

Sa’ar

(2006) Synthesis of reactive(1) designs. In: Verification, Model Checking, and Abstract Interpretation (Lecture Notes in Computer Science, Vol. 3855). New York: 2006, pp. 364–380.

29.

Raman

Kress-Gazit

(2013) Towards minimal explanations of unsynthesizability for high-level robot behaviors. In: IEEE international conference on intelligent robots and systems (IROS).

30.

Tabuada

Pappas

(2006) Linear time logic control of discrete-time linear systems. IEEE Transactions on Automatic Control 51(12): 1862–1877.

31.

Wongpiromsarn

Topcu

Murray

(2009) Receding horizon temporal logic planning. In: IEEE conference on decision and control (CDC). IEEE, pp. 5997–6004.

32.

Wongpiromsarn

Topcu

Murray

(2010) Automatic synthesis of robust embedded control software. In: AAAI spring symposium on embedded reasoning: intelligence in embedded systems.