Revisiting Underapproximate Reachability for Multipushdown Systems
401
Name
Locations Transitions Stacks Holes Time Empty (mili sec) Time Witness (mili sec) Memory(KB)
Bluetooth
45
89
2
0
149.3
0.241
6934
Bluetooth v2
47
134
2
0
92.2
0.176
5632
MultiProdCons(3,2)
7
11
2
2
126.529
0.281
5632
MultiProdCons(24,7)
32
34
2
2
1879.33
10.63
21836
Binary Search Tree
29
78
2
2
60.8
5.1
5143
untimed-L
crit
6
10
2
2
14.9
0.7
4692
untimed-Maze
9
12
2
0
8.25
0.07
5558
L
bh (from Sec. 2.1)
7
13
2
2
22.2
0.6
4404
Table 1. Experimental results: Time Empty and Time Witness column represents no.
of milliseconds needed for emptiness checking and to generate witness respectively.
and consumption of the ‘A’s and ‘B’s are modeled using push and pop in the
respective stack. For a given M and N , the language accepted by the system
is non-empty iff there is a run where all the produced ‘A’s and ‘B’s are consumed. The language accepted by the two-stack pushdown system is given by
L M,N = ((a
M + b
N )
+ (¯ a ¯ b)
+ )
+ , where a, b represent respectively, the push on
stack 1, 2 and ¯
a, ¯ b represent the pop on stack 1, 2 and hence must happen equal
number of times.
For any M, N > 0, any accepting run of the two stack pushdown system
cannot be well-nested. Further, in an accepting run, the minimum number of
items produced (and hence its length) must be a multiple of LCM (M, N ). As
the consumption of ‘A’s and ‘B’s happen in an order one by one i.e., in a sequence
where consumption of ‘A’ and ‘B’ alternate, the minimum number of context
changes (and the scope bound) required in an accepting run depends on M and
N (in fact it is O(2 × LCM (M, N )). On the other hand, the shortest accepting
run is 2-hole bounded: at any position of the word, the open holes come from
the unmatched sequences of a and b seen so far. Thus for any M, N >0, BHIM
was able to check for non-emptiness of L M,N with a witness of hole bound 2.
• Critical time constraints [9]. This is one of the timed examples, where
we consider the language L
crit = {a
y b
z c
y d
z
| y, z ≥ 1} with time constraints
between occurrences of symbols. The first c must appear after 1 time-unit of the
last a, the first d must appear within 3 time-units of the last b, and the last b
must appear within 2 time units from the start, and the last d must appear at
4 time units. L
crit is accepted by a TMPDA with two timed stacks. L
crit has no
well-nested word, is 4-context bounded, but only 2 hole-bounded.
• Concurrent Insertions in Binary Search Trees. Concurrent insertions
in binary search trees is a very important problem in database management
systems. [17,11] proposes an algorithm to solve this problem for concurrent
implementations. However, incorrect implementation of locks allows a thread
to overwrite others. We modified the algorithm [17] to capture this bug, and
modeled it as MPDA. BHIM found the bug with a witness of hole-bound 2.
• Maze Example. Finally we consider a robot navigating a maze, picking items;
an extended (from single to multiple stack) version of the example from [6]. In
the untimed setting, a witness for non-emptiness was obtained with hole-bound
0, while in the extension with time, the witness had a hole-bound 2.
401
Name
Locations Transitions Stacks Holes Time Empty (mili sec) Time Witness (mili sec) Memory(KB)
Bluetooth
45
89
2
0
149.3
0.241
6934
Bluetooth v2
47
134
2
0
92.2
0.176
5632
MultiProdCons(3,2)
7
11
2
2
126.529
0.281
5632
MultiProdCons(24,7)
32
34
2
2
1879.33
10.63
21836
Binary Search Tree
29
78
2
2
60.8
5.1
5143
untimed-L
crit
6
10
2
2
14.9
0.7
4692
untimed-Maze
9
12
2
0
8.25
0.07
5558
L
bh (from Sec. 2.1)
7
13
2
2
22.2
0.6
4404
Table 1. Experimental results: Time Empty and Time Witness column represents no.
of milliseconds needed for emptiness checking and to generate witness respectively.
and consumption of the ‘A’s and ‘B’s are modeled using push and pop in the
respective stack. For a given M and N , the language accepted by the system
is non-empty iff there is a run where all the produced ‘A’s and ‘B’s are consumed. The language accepted by the two-stack pushdown system is given by
L M,N = ((a
M + b
N )
+ (¯ a ¯ b)
+ )
+ , where a, b represent respectively, the push on
stack 1, 2 and ¯
a, ¯ b represent the pop on stack 1, 2 and hence must happen equal
number of times.
For any M, N > 0, any accepting run of the two stack pushdown system
cannot be well-nested. Further, in an accepting run, the minimum number of
items produced (and hence its length) must be a multiple of LCM (M, N ). As
the consumption of ‘A’s and ‘B’s happen in an order one by one i.e., in a sequence
where consumption of ‘A’ and ‘B’ alternate, the minimum number of context
changes (and the scope bound) required in an accepting run depends on M and
N (in fact it is O(2 × LCM (M, N )). On the other hand, the shortest accepting
run is 2-hole bounded: at any position of the word, the open holes come from
the unmatched sequences of a and b seen so far. Thus for any M, N >0, BHIM
was able to check for non-emptiness of L M,N with a witness of hole bound 2.
• Critical time constraints [9]. This is one of the timed examples, where
we consider the language L
crit = {a
y b
z c
y d
z
| y, z ≥ 1} with time constraints
between occurrences of symbols. The first c must appear after 1 time-unit of the
last a, the first d must appear within 3 time-units of the last b, and the last b
must appear within 2 time units from the start, and the last d must appear at
4 time units. L
crit is accepted by a TMPDA with two timed stacks. L
crit has no
well-nested word, is 4-context bounded, but only 2 hole-bounded.
• Concurrent Insertions in Binary Search Trees. Concurrent insertions
in binary search trees is a very important problem in database management
systems. [17,11] proposes an algorithm to solve this problem for concurrent
implementations. However, incorrect implementation of locks allows a thread
to overwrite others. We modified the algorithm [17] to capture this bug, and
modeled it as MPDA. BHIM found the bug with a witness of hole-bound 2.
• Maze Example. Finally we consider a robot navigating a maze, picking items;
an extended (from single to multiple stack) version of the example from [6]. In
the untimed setting, a witness for non-emptiness was obtained with hole-bound
0, while in the extension with time, the witness had a hole-bound 2.