Doctoral Research · Space Robotics Inspection with a Free-Flying Space Manipulator
A Doctoral Research Journal Aerospace Engineering

Start Here

This site is the working journal of a doctoral research project — risk-aware planning and control for a free-flying space manipulator. Everything on it is generated from one analysis pipeline and version-controlled sources: every number traces to a logged simulation run, every figure to a committed specification, every derivation to a machine-checked proof or a step-by-step write-up. This page is the front door: what the project is, where to start reading, and how each phase connects.

The thesis

Risk-Aware Active Inspection Planning and Control for Free-Flying Space Manipulators under State, Actuation, and Camera-Pose Uncertainty

Central question: how can a free-flying robotic inspection system make better inspection decisions under uncertainty? Two supporting questions follow: can risk-aware planning and control produce a more robust controller, and how must the guidance and control algorithms change to achieve it?

The problem, in one paragraph

A free-flying space manipulator — a fully-actuated spacecraft base carrying a robotic arm with a camera in place of an end-effector — inspects a target satellite. The nominal guidance and control already fly the full inspection orbit. The thesis question is what happens when the system stops pretending it knows everything: when its own state estimate, its actuation, and its camera pose all carry uncertainty. The work formalizes that uncertainty explicitly, scores camera views by risk rather than by expectation alone, and makes the planner and controller behave more cautiously exactly when confidence is poor — then measures what that caution costs and buys.

Where to begin

  1. One worked example, end to end: the mission-clock investigation — question, pre-registered prediction, measurement, conclusion; two candidate mechanisms eliminated by exact-zero tests before the surviving explanation was accepted.
  2. The pre-risk milestone: the architectural close-out of the error-floor investigation — six candidate channels excluded on frozen pre-registrations, the ~0.14 m along-track cruise floor shown to be architectural, and the re-scoping decision it tees.
  3. The phase timeline just below — what is finished, active, and upcoming, and what gates each step; the full interactive timeline lays out the risk-aware roadmap.
  4. The progress reports archive: /reports — every report, searchable.
  5. The research wiki: /research/ — the literature layer: sources, topics, and named results with their equations. Its counterpart, the code wiki, documents the software the same way.
  6. The formally verified proofs: the stability mathematics is being sealed in Lean 4 — each proof compiles against the community mathematics library with no unverified assumptions, and ships with a step-by-step human derivation that can be checked on paper, independent of any software. Sealed so far: the determinant identity, the Lyapunov comparison theorem, LaSalle’s invariance principle, and the passivity identity. The full proof library lists every sealed module.

The phase timeline

Phase Question it answers Status (July 2026)
Nominal lockdown Is the deterministic baseline trustworthy enough to perturb? active — the mission-clock case is closed; the along-track velocity bias is the sharpened open question
Phase 0 — foundation What breaks first, and how do we measure “worse”? active — three of four risk metrics implemented and verified
Phase A — CVaR view scoring Does risk-aware view scoring beat nominal and expected-value scoring under camera-pose uncertainty? derivation drafted, under review
Phase B — state uncertainty How should guidance behave when the state estimate itself is uncertain? upcoming, detailed after Phase A’s gate
Phase C — actuation uncertainty Can the controller derate itself risk-awarely? upcoming, after Phase B’s gate
Phase D/E — objective extensions Reconstruction confidence and probabilistic margins as objectives upcoming, research-first

Two tracks run in parallel and never gate the main line: the seven-degree-of-freedom extension, and the Lean 4 formalization of the stability mathematics.

How results are verified

Every phase is pre-registered before it runs: the question, the prediction, and the pass/fail criteria are written down first, and the measurement follows. Every simulation result comes from one pinned pipeline — a run specification in version control, executed by one orchestrator, measured by one analysis module. Every derivation is machine-checked symbolically before it is trusted, and the stability layer carries a second, stricter seal: proofs compiled by the Lean 4 kernel, each accompanied by its human derivation. Where a result disagrees with a prediction, the disagreement is reported as the finding.