SE PhD Final Defense: Ahmad Ahmad

SE PhD Final Defense: Ahmad Ahmad

TITLE: Quantitative Temporal Logic for Safe and Robust Planning, Learning, and Control

ADVISOR: Calin Belta (SE, ME), Roberto Tron (SE, ME)

CHAIR: Andrew Sabelhaus (SE, ME)

COMMITTEE: Wenchao Li (SE, ECE) Alyssa Pierson (SE, ME) Gioele Zardini, MIT

ABSTRACT: Temporal logics enable formal specification of robotic tasks with explicit timing constraints. While Signal Temporal Logic (STL) has established quantitative robustness measures, Time Window Temporal Logic (TWTL) previously lacked quantitative semantics. Traditional min-max robustness for STL focuses on critical time points, creating non-smooth optimization landscapes. This dissertation introduces the first quantitative semantics for TWTL, developing both traditional min-max and Arithmetic-Geometric Mean (AGM) robustness. AGM evaluates satisfaction holistically across all time points while maintaining soundness guarantees. We make three main contributions. First, we develop AGM robustness semantics for TWTL using arithmetic means for mixed-sign values and geometric means for uniform-sign values. We prove soundness, introduce interval semantics for partial trajectories, and present efficient incremental monitoring algorithms. Second, we present RRT$^\eta$, integrating AGM robustness into sampling-based motion planning for STL with interval semantics, Direction of Increasing AGM Satisfaction vectors, and Fulfillment Priority Logic composition. We prove probabilistic completeness and asymptotic optimality. Experiments show AGM-based methods discover feasible solutions where traditional approaches fail. Third, we develop Accelerated Proximal Policy Optimization (APPO) combining hybrid policy architecture with TWTL-based reward shaping. We prove monotonic improvement with bounded gap $(2\varsigma\gamma\alpha^2)/(1-\gamma)^2$ and optimal policy preservation. Experiments demonstrate successful learning for tasks with delayed rewards. AGM robustness provides a unifying framework across temporal logic formalisms and application domains, with smooth optimization landscapes, formal guarantees, and demonstrated benefits on diverse robotic systems.