The model checking problem for finite-state open systems (module checking) has been extensively studied in the literature, both in the context of environments with perfect and imperfect information about the system. Recently, the perfect information case has been extended to infinite-state systems (pushdown module checking). In this paper, we extend pushdown module checking to the imperfect information setting; i.e., the environment has only a partial view of the system's control states and pushdown store content. We study the complexity of this problem with respect to the branching-time temporal logic CTL, and show that pushdown module checking, which is by itself harder than pushdown model checking, becomes undecidable when the environment has imperfect information. We also show that undecidability relies on hiding information about the pushdown store. Indeed, we prove that with imperfect information about the control states, but a visible pushdown store, the problem is decidable and its complexity is the same as that of (perfect information) pushdown module checking. © Springer-Ver lag Berlin Heidelberg 2007.
CITATION STYLE
Aminof, B., Murano, A., & Vardi, M. Y. (2007). Pushdown module checking with imperfect information. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4703 LNCS, pp. 460–475). Springer Verlag. https://doi.org/10.1007/978-3-540-74407-8_31
Mendeley helps you to discover research relevant for your work.