Information Technology Reference
In-Depth Information
as follows:
=
i∈
[1
,n
]
j∈
[1
,m
]
˜
˜
{
K
1
,...,K
n
}
{
H
1
,...,H
m
}
{
K
i
}
{
H
j
}
˜
{
(
K, b,
(
A,u,g
1
)(
G,g
1
,g
2
))
}
{
(
H, c,
(
B,v,g
1
)(
G,g
1
,g
2
))
}
=
{
(
K∪H, bc,
(
A∪B,uvg
1
,g
1
)(
G,g
1
,g
2
))
}
Σ
∗
.Then
Theorem 1.
Let
Φ
be a CaRet formula and
w
∈
M
Φ
(
w
)=
Φ
4
(
w
)
.
Corollary 1.
Given a CaRet formula
ϕ
,wecanconstructin2-
ExpTime
a
push-down Mealy machine
M
implementing the four-valued FCaRet
4
semantics
of
ϕ
.
4 Anticipatory Monitoring of Visibly Context-Free
Properties
In this section we describe an anticipatory monitor construction for visibly
context-free
ω
-languages. By basing the construction on properties given by
ω
-Vpa we provide support for complete CaRet including past operators and
more expressive logics like VP-
μ
TL and MSO
μ
which are complete for the visi-
bly context-free
ω
-languages. Furthermore, integrating an emptiness check into
the monitor construction allows for the synthesis of
anticipatory
monitors, i.e.
monitors that yield a definite verdict as early as possible.
Given a property
L
Σ
ω
we define a three-valued, anticipatory
monitor
func-
⊆
tion
M
3
thereby lifting the concept of [10] from LTL to arbitrary
ω
-languages.
M
3
:2
Σ
ω
(
Σ
∗
→
B
3
)isgivenas
→
⎧
⎨
if
∀
u∈Σ
ω
:
wu
∈
L
M
3
(
L
)(
w
)=
⊥
∀
u∈Σ
ω
:
wu
∈
L
if
⎩
? rwi .
The monitor function yields
for a good prefix
w
i.e. if any continuation of
w
is in
L
, it yields
for a bad prefix
w
i.e. if any continuation of
w
is not in
L
and it yields ? otherwise.
⊥
4.1 Emptiness Per Configuration
Let
=(
Q,Σ,Γ,δ,Q
0
,F
)bean
ω
-Vpa. In the following, we show how to
construct a deterministic Vpa that accepts exactly the good and inconclusive
prefixes of
P
Σ
∗
|∃
u∈Σ
ω
:
wu
.
As Bouajjani et al. describe in [19], we can, in polynomial time, construct a
multi-automaton
L
(
P
), i.e.
{
w
∈
∈L
(
P
)
}
Q,Γ,Q,δ
A
,A
) accepting exactly the set of configu-
rations from which there is an accepting run of
A
=(
S
∪
P
.Thatis,
P
can still accept
