Risk-Certified Compositional Abstractions of Stochastic Networks under Imperfect Input Execution, with an Application to Mood Dynamics Fitted to Public EMA Data

Approximate (alternating) bisimulation lets one synthesize controllers on a finite abstraction and refine them to a concrete system with a quantified error. For stochastic interconnected systems, recent compositional results certify closeness only through $q$-th moments, and they assume that the input prescribed on the abstraction is executed exactly. Both assumptions are limiting in computational psychiatry, where the events that matter (relapse, mood-episode onset) are \emph{tail} events, and where the ``actuator'' is a patient who may skip, delay, or mis-dose an intervention.We combine two extensions of the moment-based framework. First, we convert $q$-th-moment bounds into \emph{explicit risk bounds} via conditional Markov inequalities, which yields approximate alternating simulation relations with a genuine failure probability $\varrho>0$. Second, we treat imperfect input execution as a \emph{universally quantified} perturbation of the prescribed input, constrained only by a conditional $q$-th-moment budget; this differs from the existentially quantified input slack in the standard definition. For a class of networked linear-affine stochastic systems with finite prescribed input sets, we prove that a quantized abstraction satisfies the resulting relation, that locally verified assume--guarantee contracts compose into a global risk certificate with $\varrho_{\mathrm{glob}}=\sum_i\varrho_i$, and that the certified first-exit time is stochastically bounded below by a geometric random variable. We derive closed-form \emph{adherence tolerances}, namely the largest skip probability compatible with a prescribed per-step risk. We also give a measurement-free regime in which accumulated error is bounded through the spectral radius of an $N\times N$ comparison matrix, a small-gain-type condition that replaces incremental stability of the full state space.As an application we fit a three-node mood--sleep--activity network to a public single-participant EMA data set (239 days, major depressive disorder, tapered antidepressant) and evaluate the certificates on the fitted model. The certificates are consistent with simulation but conservative: on this data, process noise is comparable to the series' own variability, so informative per-day risk bounds require wide safe bands, adherence barely moves the bound at the fitted dose strength, and worst-case parameter-uncertainty margins from 79--142 day-pairs make certification infeasible. The paper makes no clinical claims, and the data are not from bipolar disorder.