New results on pushdown module checking with imperfect information

Details New results on pushdown module checking with imperfect information New results on pushdown module checking with imperfect information

2011-06-07

arxiv.org/abs/1106.1239v1

EPTCS 54, 2011, pp. 162-177

Computer Science

Logic in Computer Science

In Proceedings GandALF 2011, arXiv:1106.0814

Scientific paper

10.4204/EPTCS.54.12

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).

Affiliated with

Also associated with

No associations

Rating

New results on pushdown module checking with imperfect information does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with New results on pushdown module checking with imperfect information, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and New results on pushdown module checking with imperfect information will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-26168