Information Technology Reference
In-Depth Information
Algorithm 1
Checking right-universality incrementally
function
Incremental-right-universality(
A
)
u ←
while
trace
w
is not completely read
do
a ←
next letter of
w
u ← ua
if
A
is right-universal w.r.t.
u
then
return
True
end if
end while
return
False
end function
in Algorithm 1. By incremental, we mean that some information is propagated
from one event (reading a letter in
w
) to the next one (reading the next letter in
w
), avoiding repeated identical computations. Note that our algorithm will not
store
u
, but enough information for asserting right-universality of
w.r.t.
u
.
For
safety properties
, right-universality allows to know at the earliest time
point, whether the execution is sure, and thus whether controls can be stopped.
This is typically the case for properties looking for a pattern (potentially com-
plicated) that must occur during the execution. For
properties to be avoided
,
this permits to stop the program before it enters an unsafe configuration, hence
avoiding potential attacks [BJLW08].
These questions started to be addressed in the context of XML through
earli-
est query answering
of XPath expressions [BYFJ05, GNT09]. Indeed, XML doc-
uments also entail a nesting structure, similarly to program traces, and properties
(or queries) over these documents can be expressed using VPAs. An algorithm
asserting at the earliest time point, whether an XML document is accepted by
a deterministic VPA has been proposed in [GNT09]. This algorithm runs in
polynomial time at each incoming event. For non-deterministic VPAs, however,
the decision problem associated with right-universality (i.e. given
A
and
u
,is
A
right-universal w.r.t.
u
?) is known to be ExpTime-complete [GNT09].
Algorithms that incrementally check right-universality of
non-deterministic
VPAs are challenging in several aspects. First, VPAs are usually an intermediate
object, resulting from the translation of a property expressed in some logics, like
XPath for XML documents. Such translations rely on non-determinism, as for in-
stance when referring to any call inside a given procedure call (which corresponds
to the descendant axis in XPath). Any VPA can be determinized, but the proce-
dure yields VPAs of exponential size [AM09]. Second, right-universality w.r.t.
u
can be considered as a variant of universality, parameterized by
u
. Recent tech-
niques have been proposed to check universality of non-deterministic VPAs e-
ciently [TO12, FKL13, BDG13]. Among them,
antichains
have been successfully
applied to decision problems related to non-deterministic automata: universal-
ity and inclusion for finite word automata [DDHR06], and for non-deterministic
bottom-up tree automata [BHH
+
08]. Whether these techniques also apply to
A
