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

Mazumdar, Bujorianu and Wisniewski recently introduced 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.First, we replace the chain and the subset lattice by a general finite directed acyclic graph of modes with per-mode avoid sets and absolute stage deadlines, and prove that the success probability is characterised by one parabolic Dirichlet problem per mode, solved backward along a topological order.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 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.