Pushdown Module Checking

Model checking is a useful method to verify automatically the correctness of a system with respect to a desired behavior, by checking whether a mathematical model of the system satisfies a formal specifi- cation of this behavior. Many systems of interest are open, in the sense that their behavior depends on the interaction with their environment. The model checking problem for finite-state open systems (called module checking) has been intensively studied in the literature. In this paper, we focus on open pushdown systems and we study the related model- checking problem (pushdown module checking, for short) with respect to properties expressed by CTL and CTL formulas. We show that push- down module checking against CTL (resp., CTL ) is 2Exptime-complete (resp., 3Exptime-complete). Moreover, we prove that for a fixed CTL formula, the problem is Exptime-complete.