Pushdown Module Checking with Imperfect Information

Abstract : 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., to the case where the environment has only a partial view of the system's control states and push-down store content. We study the complexity of this problem with respect to the branching-time temporal logics CTL, CTL * and the propositional µ-calculus. We 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 2Exptime-complete for CTL and the propositional µ-calculus, and 3Exptime-complete for CTL * .
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2013, 223, pp.18. <10.1016/j.ic.2012.11.005>
Liste complète des métadonnées

Contributeur : Olivier Serre <>
Soumis le : vendredi 22 janvier 2016 - 14:41:48
Dernière modification le : vendredi 13 janvier 2017 - 14:21:37
Document(s) archivé(s) le : samedi 23 avril 2016 - 10:42:18


Fichiers produits par l'(les) auteur(s)




Benjamin Aminof, Axel Legay, Aniello Murano, Olivier Serre, Moshe Vardi. Pushdown Module Checking with Imperfect Information. Information and Computation, Elsevier, 2013, 223, pp.18. <10.1016/j.ic.2012.11.005>. <hal-01260664>



Consultations de
la notice


Téléchargements du document