Sequential Safety for Controlled Stochastic Diffusions:Reach--Avoid Automata with Deadlines and Hamilton--Jacobi--Bellman Characterisation

Mazumdar, Bujorianu and Wisniewski recently introduced \emph{probabilistic sequential safety} for It\^o diffusions: the probability that a trajectory visits a tuple of closed target regions, either in a prescribed order or in any order, before a horizon $T$.They characterise it through chains of coupled backward Kolmogorov equations obtained from a mode-augmented strong Markov process.We extend that framework in two directions.\emph{First}, we replace the chain and the subset lattice by a general finite directed acyclic graph of modes with per-mode \emph{avoid sets} and absolute \emph{stage deadlines}, and prove that the success probability is characterised by one parabolic Dirichlet problem per mode, solved backward along a topological order.\emph{Second}, we add control.For nondegenerate diffusions with controlled drift, the maximal (adversarial) and minimal (defensive) success probabilities solve the same recursive system with a Hamilton--Jacobi--Bellman nonlinearity.We prove a verification theorem that identifies the value functions and yields optimal \emph{mode-dependent} feedback laws, and a saddle-point result for a zero-sum attacker--defender version.We state precisely which analytic ingredients are imported from classical theory and which restrictions (diffusion control, overlapping targets, cyclic automata) remain open.