Information Technology Reference
In-Depth Information
A
to have a deterministic transition function
δ
since
A
Further, we can assume
is basically a compact representation of a set of finite automata.
3 Four-Valued Semantics of CaRet
+
on Finite Traces and
Impartial Monitoring
In this section, we consider the logic CaRet as a specification formalism for
nesting structures. For its future fragment CaRet
+
, we provide a four-valued,
impartial semantics on finite words. We show how to construct a push-down
Mealy machine as monitor that incrementally reads input symbols and outputs
the semantics of the observed trace. Our aim is to give an easily implementable
monitor construction for properties expressing nesting structures.
3.1 Four-Valued CaRet
+
The syntax of CaRet
+
formulae is defined by the following grammar.
X
a
ϕ
ϕ
U
a
ϕ
ϕ
::=
p
|
ϕ
∧
ϕ
|
X
ϕ
|
|
ϕ
U
ϕ
|
|
¬
p
|
ϕ
∨
ϕ
|
X
ϕ
|
X
a
ϕ
|
ϕ
R
ϕ
|
ϕ
R
a
ϕ
The idea of how CaRet extends the operators known form LTL is as follows:
Consider for example a program procedure. While the direct successor of a line
might be the first line in a called procedure, the abstract successor jumps directly
to the next line in the current procedure and omits to enter any called procedures.
Moreover, the last line in the procedure has a direct successor, namely the return
position in its caller, but no abstract successor. CaRet uses the abstract next
modality X
a
to specify a property at the next abstract position. Further, in
general, it contains the abstract past modality X
a
−
for specifying a property at
the call position of the current procedure. Intuitively, consecutive application
of X
a
−
walks up the call stack. Also, CaRet provides abstract versions of the
common until and since operators. However, for sake of simplicity, we do not
support the past operators in this section. It shall be noted, that in contrast to
LTL, past modalities add expressiveness to the logic.
For a formula
Φ
,wedenote
sub
(
Φ
) the set of sub-formulae including unfold-
ings, e.g.
ψ
∨
ϕ
∧
X(
ϕ
U
ψ
) for a sub-formula
ϕ
U
ψ
of
Φ
.
Semantics on Finite Traces.
The semantics of CaRet is defined on infinite traces.
Since monitoring inherently deals with finite traces we provide the impartial
finitary semantics FCaRet
4
. It is intended to intuitively resemble the infinite
trace semantics, similar to finitary semantics for LTL formulae, e.g. FLTL and
FLTL
4
[4].
As the latter, FCaRet
4
uses the four truth values
true
(
),
false
(
⊥
),
presum-
p
)and
presumably false
(
p
), allowing for impartiality.
ably true
(
⊥
