# Pushdown Module Checking with Perfect and Imperfect Information

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 talk, we first recall the basic concepts and the main results regarding module checking.

Then, we focus on open pushdown systems and consider the related model-checking problem (pushdown module checking, for short) with respect to properties expressed by CTL, CTL*, and µ-calculus formulas, both in the perfect and imperfect information settings.

First we show that, in the perfect information setting, pushdown module checking against CTL and µ-calculus formulas is 2Exptime-complete, while it is 3Exptime-complete with respect to CTL* formulas. In particular, we show that, for a fixed formula, the problem is Exptime-complete.

Then, we consider the previous problems in the imperfect information setting, i.e., in the case where the environment has only a partial view of system's control states and pushdown store content.

We show that pushdown module checking becomes undecidable when the environment has imperfect information about the pushdown store, while having only imperfect information about the control states,

but a visible pushdown store, makes the problem decidable and 2Exptime-complete for CTL and the propositional µ-calculus formulas, and 3Exptime-complete in the case of CTL* formulas.

We conclude the talk by considering restricted open pushdown models in which it is possible, for fixed formulas, to solve the pushdown module checking problem in polynomial time.