398
S. Akshay et al.
• Assume that the current pop operation is closing a hole
of kind
i as in Figure 2. This hole consists of the atomic holes
,
and
. The
atomic hole
consists of the push and the well-nested sequence
(same
for the other two atomic holes). Searching among possible push transitions, we
identify the matching push associated with the current pop, resulting in closing
the hole. On backtracking, this leads to a parent node with the atomic hole
having as left end point, the push , and the right end point as the target of
the ws
. We push onto the witness stack i, a barrier (a delimiter symbol #)
followed by the matching push transition and then the ws,
. The barrier
segregates the contents of the witness stack when we have two pop transitions
of the same stack in the reverse run, closing/shrinking two different holes.
Figure 2. Backtracking to spit
out the hole
in reverse.
The transitions of the atomic hole
are first written in the reverse
order, followed by those of
in
reverse, and then of
in reverse.
• Assume that the current pop operation is
shrinking a hole of kind i. The list at the
present node has this hole, and its parent will
have a larger hole (see Figure 2, where the parent node of
has
). As in the
case above, we first identify the matching push
transition, and check if it agrees with the push
in the last atomic hole segment in the parent.
If so, we populate the witness stack i with the
rightmost atomic hole segment of the parent
node (see Figure 2,
is populated in the
stack). Each time we find a pop on backtracking the exploration tree, we find the rightmost
atomic hole segment of the parent node, and
keep pushing it on the stack, until we reach the
node which is obtained as a result of a hole creation. Now we have completely recovered the
entire hole information by backtracking, and
fill the witness stack with the reversed atomic
hole segments which constituted this hole. Notice that when we finish processing
a hole of kind i, then the witness stack i has the hole reversed inside it, followed
by a barrier. The next hole of the same kind i will be treated in the same manner.
• If the current node of the BFS tree is obtained by creating a hole of kind i
in the fix-point algorithm, then we pop the contents of witness stack i till we
reach a barrier. This spits out the atomic hole segments of the hole from the
right to the left, giving us a sequence of push transitions, and the respective ws
in between. The transitions constituting the ws are retrieved and added. Notice
that popping the witness stack i till a barrier spits out the sequence of transitions
in the correct reverse order while backtracking.
5 Adding Time to Multi-pushdown systems
In this section, we briefly describe how the algorithms described in section 3
can be extended to work in the timed setting. Due to lack of space, we focus on
S. Akshay et al.
• Assume that the current pop operation is closing a hole
of kind
i as in Figure 2. This hole consists of the atomic holes
,
and
. The
atomic hole
consists of the push and the well-nested sequence
(same
for the other two atomic holes). Searching among possible push transitions, we
identify the matching push associated with the current pop, resulting in closing
the hole. On backtracking, this leads to a parent node with the atomic hole
having as left end point, the push , and the right end point as the target of
the ws
. We push onto the witness stack i, a barrier (a delimiter symbol #)
followed by the matching push transition and then the ws,
. The barrier
segregates the contents of the witness stack when we have two pop transitions
of the same stack in the reverse run, closing/shrinking two different holes.
Figure 2. Backtracking to spit
out the hole
in reverse.
The transitions of the atomic hole
are first written in the reverse
order, followed by those of
in
reverse, and then of
in reverse.
• Assume that the current pop operation is
shrinking a hole of kind i. The list at the
present node has this hole, and its parent will
have a larger hole (see Figure 2, where the parent node of
has
). As in the
case above, we first identify the matching push
transition, and check if it agrees with the push
in the last atomic hole segment in the parent.
If so, we populate the witness stack i with the
rightmost atomic hole segment of the parent
node (see Figure 2,
is populated in the
stack). Each time we find a pop on backtracking the exploration tree, we find the rightmost
atomic hole segment of the parent node, and
keep pushing it on the stack, until we reach the
node which is obtained as a result of a hole creation. Now we have completely recovered the
entire hole information by backtracking, and
fill the witness stack with the reversed atomic
hole segments which constituted this hole. Notice that when we finish processing
a hole of kind i, then the witness stack i has the hole reversed inside it, followed
by a barrier. The next hole of the same kind i will be treated in the same manner.
• If the current node of the BFS tree is obtained by creating a hole of kind i
in the fix-point algorithm, then we pop the contents of witness stack i till we
reach a barrier. This spits out the atomic hole segments of the hole from the
right to the left, giving us a sequence of push transitions, and the respective ws
in between. The transitions constituting the ws are retrieved and added. Notice
that popping the witness stack i till a barrier spits out the sequence of transitions
in the correct reverse order while backtracking.
5 Adding Time to Multi-pushdown systems
In this section, we briefly describe how the algorithms described in section 3
can be extended to work in the timed setting. Due to lack of space, we focus on