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 specification 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 pushdown module checking against CTL (resp., CTL∗) is 2EXPTIME-complete (resp., 3EXPTIME-complete). Moreover, we prove that for a fixed CTL or CTL∗ formula, the problem is EXPTIME-complete.