Generalized Robust MTL Semantics for Problems in Cardiac Electrophysiology

Robustness-Guided Falsification (RGF) is an efficient testing technique that tries to find a system execution that violates some formal specification, by minimizing the robustness of the specification over the set of initial conditions of the system. Robustness uses an underlying distance function on the space of system executions. As RGF is applied to new fields like medicine, it is essential to determine whether our distances still capture the domain expert's intuition of which executions are similar and which are not. Motivated by the problem of testing the algorithms of cardiac defibrillators implanted in millions of patients worldwide, this work develops a (pseudo-)distance function, called conformance, over the space of cardiac signals. By using it to distinguish between fatal and non-fatal arrhythmias obtained from real patients, it is demonstrated that conformance measures the meaningful distance between cardiac signals much better than distances used in medical devices today. Next, conformance is used to re-define the robustness degrees of Metric Temporal Logic (MTL), and it is shown that conformance-based robust semantics of MTL can bound the (conformance-based) robustness degree, thus enabling a principled application of RGF to problems in the cardiac domain, using the appropriate distance notion. Using existing robust semantics based on sup norm can yield incorrect conclusions, with potentially severe consequences to patients.