Information Technology Reference
In-Depth Information
with N atoms of the form a k , P power operators, and C
concatenation operators, will produce an initial constraint expression ˆ
R
A regular expression
under
with
an equal number of P and C operators in the constraint expression domain, and each of
the N atoms will be replaced with a constraint vector. The number of disjunctions in the
expression is not directly relevant for the purposes of convergence.
The transformation
C
is defined for all constraint expression operators, only stop-
ping once a constraint expression is a DCE. In addition,
will itself produce a con-
straint expression, thus showing that the system will always progress while there are
operators left to be reduced. The next step is thus to demonstrate that repeated applica-
tions of
will reduce P and C to zero. This is done by case analysis on each constituent
definition of the operator, as follows:
- Concatenation of two vectors will reduce C by 1.
- Distributing
ect of increasing C by the number of
disjuncts, yet the composite expressions will subsequently undergo concatenation,
giving an overall reduction in C of 1.
- Bounded Repetition on constraint vectors will reduce P . Bounded repetition on a
disjunctions of constraint expressions will itself produce a disjunction of constraint
expressions. The index is transferred to the individual, simpler disjuncts. These dis-
juncts would either consist of constraint vectors, in which case P would be reduced,
or further disjunctions. Yet in the latter case, the nesting depth must be finite (due
to the expression being finite).
- Unbounded Repetition of a constraint vector leads to an immediate reduction of
1 from P . For a disjunction of constraint vector, the transformation will result in
each disjunct being raised to an unbounded power, and hence an initial increase in
P and C by the number of disjuncts. Yet if the sub-terms are constraint vectors,
then P and C will be reduced, as per the previous definitions. If, alternatively, the
terms are themselves disjunctions of expressions, then the terms would be further
expanded until concatenations of basic vectors are reached, at which point P and C
will be reduced.
·
over
has the immediate e
ff
Theorem 2 (Equal Aggregate Event Vectors). Given that Perms ( s ) returns the set of
permutations of a trace s, if s
# p
∈Σ ,then
.↓
Σ = ↓
# s
Σ
p
Perms ( s )
Proof. As the alphabet
Σ
is fixed for all the permutations of s , the function will always
return a set containing
Σ
maps, with one for each element of
Σ
. Since the permutation
operation only a
ff
ects the order of symbols within a trace, the symbol counts remain
ff
una
ected.
Theorem 3 (Equivalent Evaluations of Regex and Constraint Expressions). The
constraint automaton cannot produce false negatives, and is also maximally precise
given the reduced information it receives, i.e., won't produce more false warnings than
a solution based on the explicit automaton traversal using all string permutations. It
holds that
eval # s
Σ
) )
∈Σ .
C Σ (
R
(
.
,R
s
(
))
p
Perms ( s )
match( p
Each direction of the bi-implication is proven separately, and is presented as two
proofs. Prior to the proofs, we state the following lemmas:
Search WWH ::




Custom Search