Forward-Invariant STL Hidden-State Tubes

1. Integration point: use a GRU, structured state-space model, or neural ODE with latent state $h$. Add a residual input channel $u$ and parameterize $G_\theta$ as a small learned matrix, an identity map on selected latent coordinates, or a bounded linear head. Define STL predicates on decoded outputs $\hat y=D_\theta(h)$; for a linear decoder, pull output half-spaces back into latent half-spaces, while for a nonlinear decoder use its local Jacobian. 2. Pseudocode: at time $t$, compute $f_\theta$, evaluate the active polytope faces, estimate $\dot A$ and $\dot b$ by analytic differentiation or finite differences, construct the displayed inequalities, solve the minimum-norm QP, and integrate $h_{k+1}=h_k+\Delta t(f_\theta+G_\theta u^*)$. Initially stop gradients through the QP; later use an implicit differentiable QP layer. 3. Taken from the paper's mechanism are time-indexed convex STL sets and forward-invariance constraints. Estimated quantities are the learned dynamics, control map, moving-set derivatives, and actual robustness margin. 4. First experiment: train a two-layer GRU on Lorenz-63 or pendulum next-state prediction with the requirement that position remain in a safe interval during $[2,4]$ and enter a target interval during $[6,8]$. Compare unconstrained rollout, penalty-only training, and QP correction. Sweep $\kappa$, input bounds, and integration step. The prediction is a feasibility boundary: when available control authority exceeds the maximum outward boundary velocity, violations should vanish; below it, QP infeasibility or persistent violation should occur. In feasible runs, plot $\log V_i(t)$ and test whether its slope is approximately $-\kappa$ within 20 percent. Also test whether the robust STL violation rate approaches zero and whether long-horizon prediction error is lower than for the unconstrained model.