Unsolved problem
Sepsis early-warning systems are point-in-time statistical models. No formal model of pre-clinical physiological trajectory exists. Alarm-threshold verification is ad hoc.
Vitacore angle
Probabilistic timed automaton model of pre-sepsis state transitions with formal verification of alarm timing guarantees. Reachability analysis answers: can the system provably alarm before critical state transition?