New results on pushdown module checking with imperfect information

TL;DR

This paper investigates the decidability and complexity of pushdown module checking with imperfect information, revealing undecidability in some cases and identifying a decidable subclass with high complexity.

Contribution

It establishes the undecidability of PMC with imperfect information under certain restrictions and identifies a specific subclass where the problem is decidable and has 2EXPTIME complexity.

Findings

PMC with imperfect information is undecidable when stack depth is visible.

A subclass with visible stack depth has decidable PMC against existential CTL.

Program complexity for this subclass is 2EXPTIME-complete.

Abstract

Model checking of open pushdown systems (OPD) w.r.t. standard branching temporal logics (pushdown module checking or PMC) has been recently investigated in the literature, both in the context of environments with perfect and imperfect information about the system (in the last case, the environment has only a partial view of the system's control states and stack content). For standard CTL, PMC with imperfect information is known to be undecidable. If the stack content is assumed to be visible, then the problem is decidable and 2EXPTIME-complete (matching the complexity of PMC with perfect information against CTL). The decidability status of PMC with imperfect information against CTL restricted to the case where the depth of the stack content is visible is open. In this paper, we show that with this restriction, PMC with imperfect information against CTL remains undecidable. On the other hand, we individuate an interesting subclass of OPDS with visible stack content depth such that PMC with imperfect information against the existential fragment of CTL is decidable and in 2EXPTIME. Moreover, we show that the program complexity of PMC with imperfect information and visible stack content against CTL is 2EXPTIME-complete (hence, exponentially harder than the program complexity of PMC with perfect information, which is known to be EXPTIME-complete).