Hole Bounded Reachability in Multi-Stack Pushdown Systems – with and without Time!

Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in analyzing a restricted class that still captures useful behaviors. In this talk, we present a new class of underapproximations for multi-stack pushdown automata called hole-bounded behaviors. We compare the expressiveness of the hole-bounded underapproximation with the existing underapproximations. Then we solve the hole-bounded reachability problem of multi-stack pushdown automata, i. e. , checking if there exists a hole-bounded behavior that is accepted by the MPDA, by developing an algorithm that uses efficient fix-point computations. We also propose an algorithm that produces witness of reachability, i. e. , when the reachability algorithm returns true, the witness algorithm produces the sequence of transitions as a witness of reachability. We further extend this work to the timed setting. Timed multi-stack pushdown automata are extensions of multi-stack pushdown automata with real-valued variables called clocks. The stacks of timed multi-stack pushdown automata are also aged in the sense that they can track the amount of time an element spent inside them. We show that hole bounded reachability of timed multi-stack pushdown automata with closed guards can be solved by extending our earlier algorithm. All these algorithms are implemented in a tool named BHIM (Bounded Hole reachability In Multi-stack pushdown systems). We illustrate its applicability by generating a set of relevant benchmarks and examining its performance. As an additional takeaway, BHIM solves the binary reachability problem in pushdown automata. Part of this work is published under the name “Revisiting Underapproximate Reachability for Multipushdown Systems” in TACAS’20 (https: //doi. org/10. 1007/978-3-030-45190-5_21)This work is done in collaboration with, Prof. Akshay S (IIT Bombay, India), Prof. Paul Gastin (ENS Paris-Sacley, France), and Prof. Krishna S (IIT Bombay, India).

Authors

• Sparsa Roychowdhury

Keywords

No keywords are indexed for this paper.