Automatic Inference and Effective Application of Temporal Specifications - Mining Software Specifications: Methodologies and Applications - page 251

Alternating
(PS)*

MultiEffect
(PSS*)*

MultiCause
(PP*S)*

EffectFirst
S*(PS)*

OneCause
S*(PSS*)*

CauseFirst
(PP*SS*)*

OneEffect
S*(PP*S)*

Response
S*(PP*SS*)*

FIGURE 8.4: Partial order of property templates. Each box shows a prop-
erty template and its regular expression representation. A pattern A is stricter
than another pattern B if L(A) L(B), where L(A) means all the strings
accepted by A. The eight patterns form a partial order in terms of their strict-
ness. For example, Alternating is the strictest pattern among them. In addition,
these patterns have an internal logical relationship as illustrated by the logical
^ operators among them. For example, a string satises the MultiEffect pattern
if and only if it satisfies the OneCause and CauseFirst patterns.

events and L events total, we want to infer which pairs of events can satisfy
the Alternating pattern. For example, a hypothetical trace ABCACBDC has
four distinct events: A, B, C, and D. Hence, there are 12 ways to instantiate
the Alternating template: (AB) , (AC) , (AD) , (BA) , ::: , (DC) . Of these,
the only Alternating property that string satises is A ! B.
A brute force algorithm would check the string against all 12 instantiations
of the property one by one. However, this algorithm does not scale when the
number of distinct events becomes large. For N distinct events, there are
N(N1) instantiations of a pattern with two parameters. Checking the string
against each instantiation needs to traverse the string once. Hence, the na ve
algorithm has running time in (N 2 L).
Next, we introduce a more ecient inference algorithm with time com-
plexity in (NL) and space complexity in (N 2 ).
The algorithm encodes a property template as a table. Figure 8.5(a) shows
a finite state machine representation of the Alternating template. State 0 is
both the initial state and the accepting state. State 2 is the error state. We
can encode the transitions in this FSM as the table shown in Figure 8.5(b).
The column header is the current state of the FSM. The row header is the
current event in the trace. Given the current state and the current event, our