Computational Methods in Systems Biology

Quantitative Regular Expressions for Arrhythmia Detection Algorithms 27

andw 2 , and QREsf,g,split−op(f,g) mapswto the cost valueop(f(w 1 ),g(w 2 )),
whereopis some operator (e.g., averaging). So let QREfourBeatsmatch four
consecutive beats in the boolean signalwand let it compute the average cycle
length of these 4 beats. Letinc(x, y) be an operation that returns True whenever
0. 8 x≥y. Then QREsuddenOnsetdoes the job:

suddenOnset:= split−inc(fourBeats,fourBeats)

fourBeats:= iter 4 −avg(intervalLength)

intervalLength:= split−left(countzeros,1) // l e f t(a, b) returnsa

The third discriminator takes in a three-vaued signalw:N→{ 0 ,A,V}
where a 0 indicates no beat, anAindicates an atrial beat, and aV indicates
a ventricular beat. Onesimplifiedversion of this discriminator detects whether
this pattern occurs in the current window:V 0 a:bA 0 c:dV 0 e:fA 0 g:hV. Here,aand
bare integers, and 0a:bindicates betweenaandbrepetitions of 0. This can be
expressed in discrete-time Metric Temporal Logic [ 15 ]. E.g. the prefixV 0 a:bA
can be written asw=V =⇒ X((w=0)Ua+1,b). And so on. This
quickly becomes unwieldy as the pattern itself becomes lengthier and with more
restrictions on the timing of the repetitions. On the other hand, this is trivially
expressed as a (quantitative) regular expression.
Our final example comes from Peak Detection (PD), which takes in a real-
valued signalv:N→R≥ 0 .Forone componentof this PD, the objective is to
detect whenv(t) exceeds a threshold valueh>0 which is reset as a function of
the previous peak value. Thus the logic must remember the value of that peak.
This necessitatesfreeze quantificationof state variables, as used in Constraint
LTL with Freeze Quantification CLTL↓[ 10 ](↓z=vmeans that we freeze the
variablezto the value ofv):

(v>h=⇒↓BL=1♦(φlocal-max=⇒ h=0. 8 z 2 ))

φlocal-max:=↓z 1 =vX(↓z 2 =vX(z 2 >z 1 ∧z 2 >v))

The nesting of freeze quantifiers increases the chances of making errors when
writing the specification and decreases its legibility. More generally, monitoring
of nested freeze quantifiers complicates the monitors significantly and increases
their runtimes. E.g., in [ 6 ] the authors show that the monitoring algorithm for
STL with nested freeze quantifiers is exponential in the number of the nested
freeze operators in the formula. This becomes more significant when dealing
with thefullPD, of which the above is one piece. On the other hand, we have
implemented an even more complex PD as a QRE (Sect.5.1).
The reader will recognize that the operations performed in these tasks are
quite common, like averaging, variability, and state-dependent resetting of val-
ues, and can conceivably be used in numerous other applications.
This variety of logics required for these tasks, all of which are fundamental
building blocks of ICD operation, means that a temporal logic-based approach to
the problem is unlikely to yield a unifying view, whereas QREs clearly do. In the
rest of the paper, the focus is placed on peak detection, as it is more complicated