Information Technology Reference
In-Depth Information
incrementally check right-universality is an interesting issue. Third, the algo-
rithm proposed in the deterministic case [GNT09] does not directly generalize
to the non-deterministic case.
Our contributions are the following. We propose an ecient incremental algo-
rithm checking right-universality of a non-deterministic VPA
. This algorithm
relies on the progressive computation of
safe sets of configurations
, the configu-
ration of a VPA being a state together with a stack content. It avoids to enterily
determinize the given VPA. This algorithm uses antichains in order to get a
compact representation of safe sets of configurations. We also propose ecient
operators and data structures for saving useless computation. We report on some
experiments, performed on randomly generated VPAs, and also on VPAs result-
ing from a translation from XPath expressions. These results exhibit the benefits
of our optimizations.
Verification of traces with a nesting structure has already been addressed,
through different aspects. Let us mention some of them. In [AEM04], the logic
CaRet over words with a nesting structure is introduced, and a model check-
ing algorithm is proposed. An extension is presented in [RCB08], with a cor-
responding monitor synthesis algorithm. VPAs are also sometimes used as an
intermediate model to express properties on program traces [CA07, FJJ
+
12].
The paper is structured as follows. In Section 2 we introduce VPAs and right-
universality. Safe sets of configurations are defined in Section 3. Our antichain-
based algorithm is described in Section 4, and further optimizations in Section 5.
Experiments are reported in Section 6.
A
2 Visibly Pushdown Automata and Right-Universality
Visibly pushdown automata (VPAs) are pushdown automata working on a par-
titioned alphabet where only call symbols can push, return symbols can pop,
and internal symbols can fire transitions without considering the stack [AM04,
AM09].
In this paper, we consider trees, instead of words with a nesting structure
(i.e. their linearization). Such a mapping is illustrated in Figure 1. Each call and
its matching return are mapped to a node, and the calls and returns directly
nested under this call correspond to the children of this node. These trees are
unranked, as the number of children of a node is not determined by its label. We
use VPAs as
unranked tree acceptors
, operating on their linearization [GNR08].
In particular these VPAs do not use internal symbols.
2.1 Unranked Trees
We here recall the standard definition of unranked trees, as provided for instance
in [CDG
+
07]. Let
Σ
be a finite
alphabet
,and
Σ
∗
(resp.
Σ
+
)bethesetofall
words (resp. non empty words) over
Σ
. The empty word is denoted by
.Given
two words
v,w
Σ
∗
over
Σ
,
v
is a
prefix
(resp.
proper prefix
)of
w
if there exists
∈
aword
v
∈
Σ
∗
(resp.
v
∈
Σ
+
) such that
vv
=
w
.
