Information Technology Reference
In-Depth Information
This common concept of nesting is reflected in the class of visibly context-
free languages. Alur et al. proposed in [13] visibly pushdown automata as an
automaton characterization of visibly context-free languages. The nature of this
automaton model is that the stack action is determined by the input symbol.
This is analogous to calls and returns in recursive programs. In contrast, a push-
down property that is not visibly, is the language
a
n
ba
n
where a stack is needed
rather for counting than for recognizing a nesting structure.
In the context of temporal specifications, the logic CaRet is a natural exten-
sion of LTL with the ability to express nesting [14,15]. The concept of a direct
temporal successor is extended to the concept of a so-called abstract successor.
That is, the successor on the same level between a call and its matching return.
CaRet, however does not cover the full class of visibly context-free properties.
Logics with full expressiveness regarding visibly context-free languages are, for
example VP-
μ
TL [16] and MSO
μ
[13].
Monitor synthesis for CaRet was first considered in [17]. More specifically, a
monitoring approach for a version of CaRet is provided that allows for checking
globally a past-time property, i.e. safety properties [18]. According to our tax-
onomy, the approach is rewriting-based. Due to the additional stack that has to
be kept in this setting, a translation to an impartial automaton approach is not
straightforward. Note that for CaRet the general scheme developed in [12] is not
applicable.
In this paper, we study monitoring of visibly context-free properties. The
future fragment of CaRet allows, similar to LTL a direct unfolding-based au-
tomaton construction. We provide a four-valued, impartial semantics on finite
words in Section 3 which is particularly suitable for monitoring. It allows us to
synthesize monitors in terms of deterministic push-down Mealy machines.
Additionally, we study an anticipatory approach to monitoring of visibly
context-free properties in Section 4. We achieve to construct anticipatory mon-
itors from visibly push-down
ω
-automata by utilizing a decision procedure for
emptiness. Thus, this allows us to monitor properties expressed e.g. in full CaRet
or VP-
μ
TL. As such, we provide a complete picture of monitoring context-free
properties in the taxonomy introduced in [4] and explained at the beginning of
this paper.
2 Preliminaries
Alphabets and Words.
Let AP be a finite set of atomic propositions and
Σ
=
2
AP
a finite alphabet. We assume
Σ
to be the disjoint union of
call
symbols
Σ
c
,
return
symbols
Σ
r
and
internal
symbols
Σ
int
.Furthermore,
call
,
int
and
ret
denote propositional formulae characterizing exactly the call, internal and
return symbols, respectively. A word over
Σ
is a possibly infinite sequence
w
=
w
0
w
1
w
2
...
s.t.
w
i
∈
Σ
.Wedenoteby
w
(
i
)
=
w
i
w
i
+1
...
the sux starting at
=
n
its length. Let
Σ
∗
and
Σ
ω
denote the sets
finite and infinite words over
Σ
, respectively, and
Σ
∞
=
Σ
∗
∪
Σ
n
,by
position
i
and, if
w
∈
|
w
|
Σ
ω
,
Σ
+
:=
Σ
∗
\{
}
.
p
,
p
,
We denote
B
4
=
{
,
⊥
⊥}
the four-valued De-Morgan lattice with linear
p
p
p
=
p
.Note,
order, i.e. the lattice with
⊥
⊥
,
=
¬⊥
and
¬⊥
