Distributed Finite-State Runtime Monitoring with Aggregated Events - Runtime Verification - page 97

The problem of computing the set of next states can be reformulated in terms of
reachability. Each state can be seen as having a set of associated conditions, or con-
straints , on the input. If a constraint evaluates to true, then the system can transition
into that state. To compute a complete set of next states, one has to check these condi-
tions for every reachable state.

State Constraint
S 0 # a = 0
S 1 # a = 1
S 2 # a = 2
Fig. 2. A linear automaton with constraints on a trace v received at S 0

a a

S 0 S 1 S 2

Figure 2 illustrates a very simple linear automaton, and the conditions required for
entering each other state when starting from S 0 . The function # a returns the frequency
with which symbol a appears in trace v . The constraints defined are strict and unam-
biguous, referring to specific frequencies. Thus, for example, if one a is observed at S 0 ,
then the system can only be in state S 1 .

a

State Constraint
S 0 # a = 0

1
S 2 # a ≥ 2
Fig. 3. Modified constraints on introducing a loop at S 1

S 1 # a ≥

a a

S 0 S 1 S 2

Precision becomes an issue once loops enter the equation. Figure 3 illustrates an au-
tomaton similar to that shown in Figure 2, yet the addition of a self-loop has weakened
the conditions, which can now only place a lower bound on the number of observed
events. However, as can be seen in the example illustrated in Figure 4, loops do not al-
ways introduce ambiguity; in this example, the automaton goes to a unique state under
any input despite the presence of loops.

a State Constraint

# a = 0 S 0

a

S 0

S 1 S 2

# a ≥ 1 ∧ (# a − 1) mod 2 = 0

S 1

a

# a ≥

∧

(# a −

=

S 2 2 2) mod 2 0

Fig. 4. A flip-flop automaton. Following a mandatory single input, the automaton oscillates be-
tween S 1 and S 2 , with the final state depending on whether an even or odd number of inputs has
been received

In general, fixed sequences of transitions precisely define the number of elements
that must be observed for the end state to be reached. Loops consume elements in
multiples of the number of elements along their path. For instance, the self-loop on S 1