Mu-calculus Pushdown Module Checking with Imperfect State Information. Aminof, B., Legay, A., Murano, A., & Serre, O. In Proceedings of the 5th IFIP International Conference on Theoretical Computer Science (IFIP TCS 2008), volume 273, of IFIP, pages 333-348, 2008. Springer-Verlag.
abstract   bibtex   
The model checking problem for open systems (module checking ) has recently been the sub ject of extensive study. The prob- lem was first studied by Kupferman, Vardi, and Wolper for finite-state systems and properties expressed in the branching time logics CTL and CTL∗ . Further study continued mainly in two directions: considering systems equipped with a pushdown store, and considering environments with imperfect information about the system. A recent paper combined the two directions and considered the CTL pushdown module checking problem in the imperfect information set- ting, i.e., in the case where the environment has only a partial view of the system control states and pushdown store content. It has been shown that this problem is undecidable when the environment has imperfect information about the pushdown store content, while it is decidable and 2Exptime-complete when the imperfect information only concerns con- trol states. It was left open whether the latter remains decidable also for more expressive logics. In this paper, we answer this question in the affirmative, showing that the pushdown module checking problem with imperfect information about the control states is decidable and 2Exptime-complete for the propositional and the graded µ-calculus, and 3Exptime-complete for CTL∗ .
@inproceedings{AminofLMS08,
  keywords = {perso,conf},
  author    = {Benjamin Aminof and
               Axel Legay and
               Aniello Murano and
               Olivier Serre},
  title     = {Mu-calculus Pushdown Module Checking with Imperfect State Information},
  year      = {2008},
  pages     = {333-348},
  booktitle = {Proceedings of the 5th IFIP International Conference on Theoretical Computer Science (IFIP TCS 2008)},
  publisher = "Springer-Verlag",
  series    = {IFIP},
  volume    = {273},
abstract = {The model checking problem for open systems (module checking ) has recently been the sub ject of extensive study. The prob- lem was first studied by Kupferman, Vardi, and Wolper for finite-state systems and properties expressed in the branching time logics CTL and CTL∗ . Further study continued mainly in two directions: considering systems equipped with a pushdown store, and considering environments with imperfect information about the system. A recent paper combined the two directions and considered the CTL pushdown module checking problem in the imperfect information set- ting, i.e., in the case where the environment has only a partial view of the system control states and pushdown store content. It has been shown that this problem is undecidable when the environment has imperfect information about the pushdown store content, while it is decidable and 2Exptime-complete when the imperfect information only concerns con- trol states. It was left open whether the latter remains decidable also for more expressive logics. In this paper, we answer this question in the affirmative, showing that the pushdown module checking problem with imperfect information about the control states is decidable and 2Exptime-complete for the propositional and the graded µ-calculus, and 3Exptime-complete for CTL∗ .},
fulltexturl = {http://hal.archives-ouvertes.fr/hal-00345948},
}

Downloads: 0