Formal Robotics Specification – RadarMap and Sensor Event Correlation

1. System Overview

The system models a robotic perception stack that integrates LiDAR-based spatial mapping and proximity sensor event. The objective is to maintain a consistent representation of the environment and to correlate heterogeneous sensor events in time.

---

2. RadarMap Representation

The RadarMap is a discrete 2D occupancy structure defined as a grid of square cells.

Let

• $R$: set of LiDAR measurements (rays or returns)

Each cell stores the following state variables:

• t_last_LiDAR: timestamp of the last LiDAR event (obstacle-related)
• $\Delta {Occlusion} = \sum_{i\in R} I_{hit}(i) − \sum_{i \in R} I_{free}(i)$ where $I_{hit}$ is the occupancy indicator for valid obstacle returns
• t_last_contact: timestamp of the last detected proximity signal

Each cell encodes a local environmental occupancy estimate derived from LiDAR and contact observations.

The contact state is defined as a binary indicator function:

$$ C=1(t_{last_contact}>0) $$

Contact observations contribute a binary occupancy confirmation independent of LiDAR estimation.

---

3. LiDAR Event Processing Model

3.1 Input Definition

A LiDAR event is defined as:

$$ L_i = (t_i, r_i, d_i) $$

where:

• t is the timestamp
• r is the sensor direction
• d is the measured distance

---

3.2 Geometric Projection

For each grid cell, the system computes:

• P_near: closest point to sensor within the receptive field
• P_far: farthest point within the receptive field

Each point is evaluated in terms of:

• Euclidean distance d
• direction vector θ relative to sensor frame

Let:

• d_near be the distance to P_near
• d_max be the maximum sensor range

---

3.3 Update Function

Each grid cell is updated according to the following deterministic rule set:

Case 1 – Valid Occlusion Detection

If:

• P_near exists
• d_near ≤ d_max
• a valid occlusion is observed

Then:

• increment ΔOcclusion count
• update t_last_LiDAR ← t

---

Case 2 – Non-occlusion Consistent Return

If:

• P_near exists
• d_near ≤ d_max
• no occlusion is detected
• the measurement lies beyond P_near along the same ray

Then:

• decrement ΔOcclusion count
• update t_last_LiDAR ← t

---

Case 3 – No Update Condition

In all other cases:

• the cell state remains unchanged

---

4. Contact Event Processing Model

4.1 Input Definition

A contact event is defined as:

C = (t, f, r)

where:

• t is the timestamp
• f is the no front contacts flag
• r is the no rear contacts flag

Contact events can occur in the following regions:

• front only
• rear only
• both
• neither

---

4.2 Update Function

Let:

• $F$: the cells in the front half-plane of the robot and within a radius of contact influence.
• $R$: the cells in the rear half-plane of the robot and within a radius of contact influence.
• $\tau_C$: the contact expiration time

Each grid cell is updated according to the following rule:

• $f=0⇒∀c∈F,C(c)←1$
• $r=0⇒∀c∈R,C(c)←1$
• $t- t_{last_contact}> \tau_C ⇒ ∀c∈R,C(c)←0$

Contact state is write-1, decay-to-0 system.

---

5. System Assumptions

• Sensor timestamps are globally ordered or synchronized
• LiDAR and contact events are processed in discrete time steps
• Geometric projections assume a calibrated and fixed sensor frame relationship
• Grid resolution is uniform and static

---

6. Version

Release: 0.26.0

---