Databases Reference
In-Depth Information
rd
fin
3
rd
fin
cfg
cnc
cnc
fin
fin
0
1
2
5
6
fin
4
wrt
cfg
cnc
fin
cnc
0
1
2
3
4
wrt
(a)
(b)
FIGURE 6.8: (a) Past abstraction step; and (b) future abstraction step,
before quotient construction.
Definition 6.4.9. An automaton A has the (k
1
;k
2
)-past-future property if
for every q
1
6= q
2
2 Q, in
k
1
(q
1
); out
k
2
(q
1
) \ in
k
1
(q
2
); out
k
2
(q
2
) = ;. This
implies that every sequence of length k
1
+ k
2
is linked to a unique automaton
state.
Proposition 6.4.10 (Precision Guarantee). If
S
h
\
2H
\
C
Tr(h
\
) is accepted by
some automaton that has the (k
1
;k
2
)-past-future property, then the (k
1
;k
2
)-
past-future abstraction with exterior merge is precise.
When the precision precondition is not met, different choices of k
1
;k
2
in
the past-future abstraction can lead to different results:
Example 6.4.11. The first row of Figure 6.9 presents two histories produced
while using the 1-past abstraction to track an abstract object that uses the
Signature
API. The history on the left uses the
verify
feature of the API,
while the history on the right uses
sign
. The current states of these two his-
tories, states 2 and 2
0
, are compatible (in
1
(2) = in
1
(2
0
) = f
update
g), and
the histories are therefore merged into the history presented in Figure 6.9 on
the right. In particular, states 2 and 2
0
are merged. As a result, the relation
between an invocation of
initVerify
(resp.
initSign
) and a later invocation
of
verify
(resp.
sign
) is lost.
When using the 1-future abstraction, on the other hand, the corresponding
abstract histories, depicted in the second row of Figure 6.9, are not compat-
ible since their initial states are not compatible (out
1
(0) = f
initVerify
g,
past
up
up
past: after merge
initV
verify
initS
sign
up
up
initV
0
1
2
3
0
1'
2'
3'
up
initV
initS
initV
up
verify
1
3
0
2
up
future
up
3
sign
3'
up
1'
3'
initS
up
initV
up
initS
0
1
2
initS
up
0'
1'
2'
up
verify
sign
FIGURE 6.9: Past abstraction versus future abstraction.
Search WWH ::
Custom Search