{'fraction_non_alphanumeric': 0.03528378140924266, 'fraction_numerical': 0.005939202249165349, 'mean_word_length': 4.72209933641665, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Cautious Planning with Incremental Symbolic Perception: Designing Verified Reactive Driving Maneuvers

This work presents a step towards utilizing incrementally-improving symbolic perception knowledge of the robot's surroundings for provably correct reactive control synthesis applied to an autonomous driving problem. Combining abstract models of motion control and information gathering, we show that assume-guarantee specifications (a subclass of Linear Temporal Logic) can be used to define and resolve traffic rules for cautious planning. We propose a novel representation called symbolic refinement tree for perception that captures the incremental knowledge about the environment and embodies the relationships between various symbolic perception inputs. The incremental knowledge is leveraged for synthesizing verified reactive plans for the robot. The case studies demonstrate the efficacy of the proposed approach in synthesizing control inputs even in case of partially occluded environments.


I. INTRODUCTION
Autonomous robots performing highly complex tasks such as urban driving may lead to serious repercussions when malfunctioning. Thus, having an autonomous system that not only adapts to the changing environment by utilizing the information gathered at runtime (reactive) but also guarantees safe behavior becomes crucial [1].
This broad problem is usually addressed using modular perception-planning frameworks (e.g., [2], [3]). Within the perception module, it is often assumed that the targets (objects of interest) can be fully identified assuming, inter alia, perfect sensing, fully observable environment, accurate detection and recognition frameworks, etc., [3]- [9]. However, pertaining to hardware limitations, occlusions, weather conditions, etc., the perception is often limited. Thus, the environment information may not be gathered all at once but may instead incrementally improve as the distance to target decreases. This renders the classical perceptionplanning architectures unable to react in a timely manner in cases where the robot may only have sparse perception information at a given instant. For instance, the autonomous car traveling downhill (Fig. 1) may detect a yellow board implying a warning sign a few instances before recognizing the exact sign. If the control module only acts based on the exact knowledge of upcoming environment states (e.g., [5]- [9]), it may lead to an overly conservative or unnecessarily risky behavior. Such challenging situations give rise to the question: how can partial knowledge be utilized to ensure safe planning? The overarching goal of this work is to address the problem of symbolic perception-aware planning where the perception improves as the robot physically progresses towards a target object. To achieve the verifiable usage of perception in control, we use abstractions to encapsulate the detection and estimation techniques (e.g., learning-based approaches, filtering) and subsequently assume symbolic information as input which is a commonly followed approach e.g., [10]- [17]. We propose an incremental-resolution representation for perception as a directed tree where each level corresponds to a symbolic feature identified at a given instant. To the authors' best knowledge, this is the first work that utilizes the evolution of perception knowledge in the form of incremental symbolic updates while providing guarantees on the system behavior for possibly adversarial environments.

A. Symbolic Perception:
Our approach for symbolic refinement tree representation is inspired by the way in which the human brain abstracts varying levels of details in the surroundings to guide learning and decision-making e.g., [18], [19]. With representation learning as the primary objective, [20] proposes learning hierarchies for obtaining semantically similar regions whereas [21] explores learning abstract representations for perception coupled with agent's skills. Instead, our work prescribes symbolic representation and utilizes it for safe control synthesis; learning the relationships among symbolic perception updates is a topic for future research.
Some existing sensor fusion approaches for perception of autonomous vehicles consider varying levels of detection and processing of individual sensor information [4]. Specific to traffic signs, [22], [23] propose the use of feature pyramids for neural networks that capture the low and high-level semantic information from a given image. Although the notion of capturing varying levels of detail (scale) is a common thread, they address the problem of accurately detecting varying-sized features from a given image, whereas we capture the evolution in symbolic knowledge about the environment.
B. Temporal Logic-Based Reactive Control Synthesis: Many existing approaches for reactive control given temporal logic specifications assume accurate symbolic perception input [10]- [14]. [10] and [11] present sampling-based and automata-based reactive planning approaches, respectively, using potential functions to react to local requests while ensuring infinite-time satisfaction of LTL tasks. In [24], the authors propose abstraction-refinement approach for planning with incomplete sensor information given LTL specifications. On the contrary, we consider the problem of reactive planning where the symbolic sensing resolution incrementally improves (refines). Assume-guarantee specifications reduce the otherwise computationally intensive, exponentialtime synthesis problem as with LTL to a polynomial-time synthesis problem. [12]- [14] solve a game between sensor propositions (environment) and robot propositions (control actions) for synthesizing reactive control in abstract dynamic environments. Our work leverages this specification formalism for control synthesis.
Another line of research investigates safe decision-making under uncertainty [25], [26]. Generally, the problem results in a Partially Observable Markov Decision Process solved using approximate methods [17], [27]- [29]. [30] considers probabilistic semantic maps for generating optimal control plans. [31] proposes a sampling-based planning approach over an environment with semantic, metric uncertainties. Although these works are closely related, they are not reactive. Using Probabilistic STL, [32] proposes a counter-example-guided approach under probabilistic perception uncertainty.
The key difference is that we incorporate the refinement in symbolic perception information into control synthesis. Our implementation considers symbolic perception input that is deterministic or is governed by a known probability distribution. However, the synthesis framework does not rely on quantification of environment uncertainty and is thus, independent of prior belief about the environment; investigating the incremental-resolution approach for a more general problem of reactive control synthesis in belief space is a topic for future research.

C. Contributions:
This work is the first step in the direction of verified reactive planning with incremental perception. The main contributions of this work are as follows: 1. We propose the problem of safe, high-level reactive control with incremental symbolic perception for an autonomous car. 2. We abstract the perception module and establish a novel incrementalresolution representation for the available symbolic perception information which facilitates the timely execution of the necessary behavior that the system must perform in order to satisfy rules of the road. 3. Additionally, we demonstrate with the help of case studies that this proposed approach helps synthesizing control inputs even in case of partial information about the environment.

II. PRELIMINARIES: MODELS AND SPECIFICATIONS
The terms ego and system interchangeably refer to an autonomous robot car that performs the assigned temporal logic tasks in a planar environment and operates using given control inputs. An environment refers to everything external to the ego that can be sensed and cannot be controlled by the ego. For formal definitions, refer to Sec. III.
, where X is a finite set of states; x T 0 ∈ X is the initial state; δ T ⊆ X × X is a set of transitions; AP is a set of properties (atomic propositions); h : X → 2 AP is a labeling function; and w T : δ T → R + is a positive weight function.
We also denote a transition ( where |x| is the length of x. We denote by x → * T x the path in T between x and x with minimum weight. The weight function ω may capture travel duration between states, distance, control effort, etc. Linear Temporal Logic (LTL) and Generalized Reactivity: Using LTL [33], specifications are expressed over a finite set of atomic propositions p i ∈ AP , i = 1, . . . , |AP |. Any LTL formula ψ is built recursively via the syntax (1) where, true, false are Boolean constants; negation (¬), conjunction (∧) are Boolean operators; and next ( ) and until (U) denote the temporal operators. Additional operators allowed by LTL such as disjunction (∨), eventually (♦), implication ( =⇒ ), always ( ), etc. can be derived using the operators defined in Eq. 1. For a detailed exposition to syntax and semantics of LTL, we refer the reader to [33].
In this work, we consider a special class of LTL formulas known as assume-guarantee specifications or GR(1) [34]. Let X denote the set of variables controlled by the environment and Y denote the set of variables controlled by the system. The synthesis problem is a dynamic game between the uncontrollable environment and the to-be-synthesized system. At each step of the game, the environment can choose the (Boolean) valuation of its variables in X before the system can choose the Boolean valuation of the variables in Y.
The general form of GR(1) formulae is Θ e ,Θ s , ψ e,safe , ψ s,safe , ψ e k for k ∈ K e and ψ s k for k ∈ K s are sub-formulae. Precisely, starting from atomic propositions based on the valuations of X and Y, the formulae Θ e and Θ s are composed via only Boolean operations (∧,∨, ¬). As such, they restrict the allowed initial states for the environment and system, respectively. The safety formulae define the allowed transitions. ψ e,safe is a Boolean formula over X ∪ Y ∪ X restricting the transitions of the environment, whereas ψ s,safe is a Boolean formula over X ∪ Y ∪ X ∪ Y. Progress or liveness are captured by the property ♦ψ which indicates that ψ should happen infinitely often. The progress goals for the environment ψ e k and for the system ψ s k are Boolean formulae over X ∪ Y.

A. Perception Model
The signs and markings in the environment are detected by the ego which is assumed to be equipped with the necessary sensors, possibly with limited range and resolution.
In addition to the traditional detection of elements of the environment (e.g., stop sign, traffic light), we assume that the perception module is capable of inferring multiple levels of detail of the given element (e.g., sign color, sign type), see Fig. 2. Thus, X = {x 1 , . . . , x n } consists of variables corresponding to varying levels of detail about the environment. These environment variables are atomic propositions and a particular variable is set to true when the event associated with it is detected in the environment. In this work, we limit the environment variables to traffic signs, intersections and traffic lights. However, the proposed approach can be used in other scenarios wherein utilizing the partial knowledge about the environment may lead to safer control strategies e.g., search and rescue, exploration missions.

B. Robot Model
Consider an ego car deployed in a planar workspace E ⊆ R 2 . We assume its dynamics to be governed byẋ = f (x, u), where x ∈ X is the state space and u ∈ U represents the control space. The state of the ego may capture its location, orientation as well as velocity. We abstract ego's motion in the workspace as a deterministic transition system T .
The control space of ego is abstracted via a finite set of system variables Y = {y 1 , y 2 , . . . , y n } denoting actions such as stop, move slowly, etc. These system variables are atomic propositions. A system variable is set to true when the corresponding action is being executed by the robot. The constraints between actions are captured in the system guarantees LTL property, e.g., come to stop =⇒ ¬move.
We consider a receding horizon approach for navigating the environment where a nominal route is assumed to be available to the ego. The ego follows a time-varying goal with respect to an abstract symbolic reference frame centered at the ego. Here, the goal refers to the next way-point to be reached while making progress on the given nominal route as expressed by the GR(1) formulae.

C. Rules
Intuitively, a rule associated with a specific environment configuration can be defined as the expected behavior by the ego upon encountering that configuration. Formally, a set of rules φ is a set of GR(1) formulae of the form (2) that establish the relation between the perceived environment state and the expected robot behavior, e.g., ¬sign ⇒ ♦max speed . Example: Consider an ego approaching a work zone. Let X = {work zone} and Y = {move slow}. The rule to be satisfied is "When work zone is encountered, slow down to the posted speed limit; If no work zone, move with maximum allowed speed".

Conditions
Environment System Initial Θ e = ¬work zone, Θ s = ¬move slow Safety ψ e,safe = T rue (environments with / without work zones are admissible) Remark: Multiple environment and system variables can be true at the same time. Furthermore, if two or more system variables cannot be true simultaneously, it should be explicitly specified as a system safety condition.
Problem III.1 (Hierarchical Perception-based Verified Reactive Planning). Given robot model, set of environment variables X , system variables Y, and the rules of the road φ, synthesize a symbolic controller (if feasible) such that the generated behavior plan for the robot to follow the nominal route satisfies all rules φ for all valid valuations of the elements of X .
IV. SOLUTION This section presents a solution to Problem III.1. In order to synthesize a winning strategy for the controllable system and uncontrollable environment, we use a receding horizon control synthesis approach. The abstractions of perception and control are centered at the ego vehicle. Thus, these abstractions are updated at each time step as the ego exhibits different control actions. The abstract models along with the rules of the road are internally converted into a GR(1) specification and then into a GR(1) game by a control synthesis tool. With the help of GR(1) specifications, we capture boththe hierarchy in the environment variables and ego's motion. The control strategies for any valid environment states are obtained as a solution to the GR(1) game (if feasible). Addressing reactivity at the specification and control level [13], [35] we assume that robust low-level controllers are available that handle the implementation level uncertainties such as obstacle avoidance, interactions with pedestrians. The detailed solution is as follows:

A. Incremental Symbolic Model of Perception
The incremental symbolic knowledge about the environment is represented using a directed tree structure referred to as the symbolic refinement tree defined as follows: Definition 2 (Symbolic Refinement Tree for Perception). The semantic relationship between symbols is captured by a directed tree G = (X , ∆) where ∆ establishes how the nodes in X are related to each other. The root of the node corresponds to whether there is an object in the environment. Each subsequent layer of the tree adds more information, capturing a refinement of the object's meaning (semantics).

Definition 3 (Ground Variables).
The set X gr ⊆ X is a set of all environment variables that correspond to the terminal nodes of the perception tree. These variables correspond to the ground truth of perception, e.g., stop sign, crosswalk sign.

Definition 4 (Derived Variables).
The set X dr ⊆ X consists of all other environment variables that lead up to the ground variables. These variables correspond to the progress of robot's knowledge towards the ground truth of perception X gr thereby capturing the symbolic multi-resolution capabilities of the perception module, e.g., sign shape, mandatory sign, danger warning sign.
Naturally, we have X gr ∩ X dr = ∅ and X gr ∪ X dr = X . Detection results in setting one or multiple environmental variables X to true. In what follows, this occurrence of true environment variables is referred to as an event. Remark: We assume that detection is persistent, i.e., coupled detection and tracking methods within the perception module. Consequently, once a variable is set, it will remain set or set a refined version of it from its descendants in G.
With respect to the abstract symbolic reference of the robot, the subset of X c over which the ground and derived variables can be detected is referred to as perception horizon.
The refinement tree G is converted into GR(1) formulae in assume-guarantee form, and provided to Tulip [36] for synthesis. The formulae capture both the refinement and persistence of information, see Sec. V for examples.

B. Robot Motion Planning
A cell decomposition of X is a set C of subsets of X such that A∈C A = X, cl(A) = A for all A ∈ C, where int(A) and cl(A) denote the interior and closure of set A, respectively. A cell decomposition of X is an exact cover of X with closed cells that share only boundaries if int(A) ∩ int(A ) = ∅ for all A, A ∈ C. Finite state abstraction. Let T C be a transition system representing the robot model abstraction such that the state space X C corresponds to a cell decomposition of X. A transition between two cells c and c , c, c ∈ X c exists if there is ξ ∈ c, ξ ∈ c , and there exists a sequence of highlevel control actions (y a , . . . , y b ) such that their execution results in driving the system from ξ to ξ . Definition 5 (Target Cell). Given X c , the target cell c target is the cell in the perception horizon sensing range of the system where a base variable x gr ∈ X gr (see III-A) is present.
Finite movement abstraction. Consider the transition system T T that consists of a state space X T ⊂ X C × X C such that (c 1 , c 2 ) ∈ X T if there exists a transition in T C between the cells c 1 and c 2 . We can now label the states based on both the location of the car and the transition that the car is making. The latter allows us to associate propositions such as moving or stationary to the car. This also implies whether new information will enter the perception model.

C. Control Synthesis as a GR(1) Game
Both the incremental symbolic model of the perception and the symbolic model of the motion planning problem can now be captured together with the rules into one GR(1) game. For control synthesis, we use the Omega solver [37] in Tulip [36], [38], which is an abstraction-based control synthesis tool. Internally, it constructs an enumerated transducer based on the given GR(1) specification and solves a Streett game -here solving refers to finding a controller that ensures the satisfaction of GR(1) formula for any admissible behavior of the uncontrolled environment. It is important to note that GR(1) can only be reactive to "known" unknowns, i.e., if the environment variable takes a value other than the imposed assumptions, no guarantees can be provided on the system behavior. Moreover, due to the particular structure requirement of GR(1), some temporal formulae like ♦ ψ cannot be directly expressed as opposed to [39]. However, the GR(1) structure is sufficiently expressive for the problem being addressed [12], [34] while also avoiding the exponential time complexity as with LTL. A detailed description of GR(1) synthesis can be found in [34], [40].
The continuous execution of the discrete solution based on the abstract models can be achieved in a provably correct fashion if there exists a similarity relation for the abstractions of continuous models [41]. For each system variable y i , we associate a continuous controller Λ(y i ). Such low-level controllers can be computed using standard methods [42] and are assumed to be available. If the a system variable y i is set to True, the ego executes control Λ(y i ).

V. RESOLVING TRAFFIC REGULATIONS WITH TEMPORAL
LOGIC CONTROL: CASE STUDIES Given limited perception, this section demonstrates how the available information can be utilized by the ego to ensure continued conformance to traffic rules. In both cases, the ego is assumed to be equipped with necessary sensors as well as recognition and tracking algorithms that provide symbolic perception input with respect to the ego's frame. The ego follows a nominal route defined in ego's reference frame where at least the immediate way-point is always within the perception horizon. The presence or absence of signs as well as their exact location are not known a priori.

A. Case Study 1
We first consider a fully observable environment wherein the ego is moving on a straight road section with one traffic sign. The ego is provided with necessary way points. The upcoming road of the ego vehicle can be partitioned into cells as depicted in Fig. 3. Depending on the distance from c target = 1, we obtain refinement of the road sign information while the car is approaching the road sign. The levels of knowledge of the ego about the environment are {sign present, sign type, sign shape, exact sign}. These will serve as environment variables in the 2-player game as described in Section IV-C and form the nodes of G. Initially, no signs are present. The condition for environment progress is "infinitely often, no signs" and is formally given by ♦¬exact sign. }. The environment variables evolve as follows as the car travels from cell c 5 to c 1 -1) If no sign in cell c i : in the next step, no sign in the current cell c i−1 (eq. (3)-(4)), 2) if sign in c i : in the next step, we get more information about it in cell c i−1 , (eq. (5)-(7)), and, thus, we move to the next level of the perception refinement tree.  Fig. 3 shows the evolution of knowledge of the system and Fig. 4 depicts the interaction between perception and control abstraction for a 'STOP' sign. In this case, the environment variables are {sign present, sign red, sign hexagonal, stop sign} and the environment progress condition is ♦¬stop sign. The control inputs for the system are : {move, attention, slow down, prepare to stop, stop}. The system progress rule is given by ♦move. The system safety rule is ψ s,safe = (stop sign =⇒ stop ∧ (move)) . The control input for the system progresses towards making a complete stop as the knowledge about the environment increases (see Fig. 4). This points at the natural interrelation between perception and control abstraction.  Fig. 5. The ego car approaching a traffic signal in a reduced traction region followed by a partially visible yield sign. In both cases the car needs to react to partial information to satisfy the rules.
Extending the previous case study, we now consider the perception knowledge to be probabilistic pertaining to the uncertainties associated with partially occluded traffic lights and signs, sensor limitations, different weather and road conditions, inaccuracies associated with detection, tracking, etc. We compare our proposed framework with the classical perception-planning approach (baseline) that does not consider symbolic refinement in perception. Note that, we employ the same high-level reactive control synthesis module for both cases and the only difference lies in whether or not incremental symbolic perception information is utilized for control synthesis. Moreover, the probabilities are used only for simulating the environment. The control synthesis is independent of these beliefs. Fig. 5 shows the test scenario where the ego car first encounters a traffic light at an intersection in a reduced traction region followed by a partially visible yield sign.
The probabilistic perception refinement is obtained as follows: The probability distribution over the terminal nodes χ gr indicates the probability of encountering a particular sign in the environment and is obtained by the state-ofthe-art traffic sign detection algorithms e.g., [23], [43]. The probability of each derived variable x dr ∈ χ dr is then obtained using the total probability rule used recursively over the refinement tree. For simulating the baseline, we only have access to the probability distribution over the terminal nodes. For both cases, the identified environment variable is then used for control synthesis. We study the reactive control synthesis for following two events.
1) Event: Traffic light: Of particular interest are the cases where the traffic light is red and the ego car needs to decelerate from v max to 0 within the remaining distance to c target (the cell containing traffic light) while accounting for the reduced friction condition. As the stopping distance is higher in this case, a safe behavior would imply starting to slow down as early as possible and avoiding hard stops.
2) Event: Yield Sign: Since the yield sign is partially visible, the perception module may not be able to accurately identify the sign in time for the system to be able to react and, thus, may lead to a collision with oncoming traffic. The environment and system variables for both cases are given in Table I. The system variables are of the form: action in x where action refers to the control input to be executed and x is the number of cells within which to execute this input. e.g., stop in 4 implies come to a complete stop in 4 cells. hard stop and yield now indicate that the action needs to be executed within one cell and infeasible indicates that the system has already reached c target without detecting the event. Fig. 6 shows the comparison between the actions chosen by the system in response to the environment.
Performance. We consider a distance-based metric defined over the robot motion model to measure the goodness of an already synthesized plan as follows: Let c d ∈ X c be the cell where a derived variable x dr is first sensed in the given cell decomposition as defined in Sec. IV. The performance s yi corresponding to a chosen control action y i by the system is defined as: s yi = ω(c d → * T C c target ), where ω(c d → * T C c target ) represents the topological distance between c d and c target in T C . Thus, the higher the distance available to react, the better is the performance. Fig. 6. The comparison between control inputs obtained for a system with (blue) and without (hatched grey) incremental-resolution perception for interaction for 100 trials. Performance s increases from left to right as the available distance to react increases. Fig. 6 shows the comparison between the control inputs for a system with and without incremental-resolution perception for n=100 trials. The frequency indicates the number of times a particular control action is chosen by the ego. Furthermore, the performance values of the chosen control action are indicated. For simplicity, we assume cells of unit length, thus if c d = c 2 , naturally s yi = 2 and so on. Since the distance to execute the chosen maneuver in the discretized environment is higher, the performance increases from left to right in Fig. 6. Evidently, the ego consistently achieves higher performance when leveraging the symbolic relationship among input environment variables.

VI. CONCLUSION
This work is a step towards representing and utilizing incremental symbolic perception information for synthesizing verified reactive control plans for an autonomous robot car. We propose a novel incremental-resolution symbolic tree for perception -an abstraction that captures gradual improvements in the ego's knowledge about the environment as well as the symbolic relationships among various environment variables. Furthermore, we combine the abstractions of information gathering and motion control along with rules of the road to be satisfied in a single GR(1) game. The case studies demonstrate an improved performance when leveraging the proposed framework with respect to execution of high-level control actions. Future directions involve experimental validation and safe control synthesis under environment uncertainty with incremental-resolution perception.