Information Technology Reference
In-Depth Information
tation would be as
regular expressions
. For each pair of states in the original automaton,
one would derive regular expressions that encompass all paths that lead from one state
to the other. Several algorithms for deriving regular expressions from automata exist,
such as the one described by Brzozowski [7]. Given any two states
q
and
q
in an au-
tomaton, regex
D
q
) will return a regular expression for the set of strings which,
starting from
q
, lead to
q
,or
(
q
,
if there are no paths between the two states.
To evaluate a compressed trace against a regular expression constraint, one would
check whether the expression matches at least one legal permutation of the elements in
the compressed trace. However, this procedure is computationally expensive, making
regular expressions inadequate for representing constraints in a monitoring context.
⊥
3.4
Constraints and Constraint Expressions
Given the inadequacy of regular expressions for representing constraints, the remain-
der of this section details
constraint expressions
, which are more amenable to direct
comparisons with compressed traces. Section 4 then describes a rewriting system for
converting regular expressions into such constraint expressions.
is a tuple of the form
2
N
N·Σ
con-
Definition 3 (Basic Constraint).
A
basic constraint
C
sisting of a set of
moduli
, a numerical
o
ff
set
, and the
symbol
being constrained.
Example 1.
The constraint on entering state
S
1
from
S
2
in the automaton illustrated in
Figure 4 would be expressed as the following basic constraint:
{
2
}
1
·
a
For an observed aggregate input
v
, this constraint would be true when at least one
a
symbol has been observed (denoted by the subscript), and when #
a
−
1 is a multiple of
2. The precise evaluation procedure will be described in Section 3.5.
Definition 4 (Well-formed Constraint Vector).
A
constraint vector
C
is a set of basic
constraints. For a constraint vector to be
well-formed
with respect to an automaton
with alphabet
Σ
, it must contain exactly one basic constraint for each element of
Σ
.
def
= {
Example 2.
A
well-formed constraint vector
for an automaton with
Σ
a
,
b
}
.
{{
2
}
1
·
a
,∅
3
·
b
}
Definition 5 (Constraint Expression).
A
constraint expression
ˆ
C
is a logical formula
of the form
=
C |
ˆ
ˆ
ˆ
ˆ
ˆ
ˆ
ˆ
n
C
∗
|⊥
C
:
C ∨
C |
C ·
C |
C
|
,and
ˆ
ˆ
ˆ
The empty constraint expression is represented by
⊥
C ∨ ⊥≡⊥∨
C ≡
C · ⊥≡
ˆ
ˆ
⊥·
C ≡
C
⊥
∗
≡⊥
n
≡⊥
, whereas
Definition 6 (Disjunctive Constraint Expression).
A
Disjunctive Constraint Expres-
sion
(DCE) is a constraint expression consisting solely of well-formed constraint vec-
tors and
∨
operators.
