Abstract
The model checking problem for open systems (module checking) has recently been the subject of extensive study. The problem 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 setting, 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 TWOEXPTIME-complete when the imperfect information only concerns control 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 TWOEXPTIME-complete for the propositional and the graded μ-calculus, and THREEEXPTIME-complete for CTL*.
Chapter PDF
Similar content being viewed by others
References
B. Aminof, A. Murano, and M.Y. Vardi. Pushdown module checking with imperfect information. In it CONCUR ’07, LNCS 4703, pages 461–476. Springer-Verlag, 2007.
P.A. Bonatti, C. Lutz, A. Murano, and M.Y. Vardi. The complexity of enriched μ-calculi. In it ICALP’06, LNCS 4052, pages 540–-551, 2006.
Laura Bozzelli, Aniello Murano, and Adriano Peron. Pushdown module checking. In it LPAR’05, LNCS 3835, pages 504–518. Springer-Verlag, 2005.
E.M. Clarke and E.A. Emerson. Design and verification of synchronization skeletons using branching time temporal logic. In it Proceedings of Workshop on Logic of Programs, LNCS 131, pages 52–71. Springer-Verlag, 1981.
E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. it J. of the ACM, 33(1):151–178, 1986.
A. Ferrante and A. Murano. Enriched μ–calculus module checking. In it FOSSACS’07, volume 4423 of it LNCS, pages 183–-197, 2007.
A. Ferrante, A. Murano, and M. Parente. Enriched μ–calculus pushdown module checking. In it LPAR’07, volume 4790 of it LNAI, pages 438–453, 2007.
C.A.R. Hoare. it Communicating Sequential Processes. Prentice-Hall, 1985.
D. Harel and A. Pnueli. On the development of reactive systems. In it Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 477–498. Springer-Verlag, 1985.
J. E. Hopcroft and J. D. Ullman. it Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.
D. Kozen. Results on the propositional mu–calculus. it Theoretical Computer Science, 27:333–354, 1983.
O. Kupferman, N. Piterman, and M.Y. Vardi. Pushdown specifications. In it LPAR’02, LNCS 2514, pages 262–277. Springer-Verlag, 2002.
O. Kupferman, U. Sattler, and M.Y. Vardi. The complexity of the graded μ-calculus. In it CADE’02, LNAI 2392, pages 423–-437, 2002.
O. Kupferman and M.Y. Vardi. Module checking. In it CAV’96, LNCS 1102, pages 75–86. Springer-Verlag, 1996.
O. Kupferman and M. Y. Vardi. Module checking revisited. In it Proc. 9th International Computer Aided Verification Conference, LNCS 1254, pages 36–47. Springer-Verlag, 1997.
O. Kupferman, M.Y. Vardi, and P. Wolper. An Automata-Theoretic Approach to Branching-Time Model Checking. it J. of the ACM, 47(2):312–360, 2000.
O. Kupferman, M.Y. Vardi, and P. Wolper. Module Checking. it Information and Computation, 164(2):322–344, 2001.
D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. it Theoretical Computer Science, 54:267–276, 1987.
J.P. Queille and J. Sifakis. Specification and verification of concurrent programs in Cesar. In it Proceedings of the Fifth International Symposium on Programming, LNCS 137, pages 337–351. Springer-Verlag, 1981.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Aminof, B., Legay, A., Murano, A., Serre, O. (2008). μ-calculus Pushdown Module Checking with Imperfect State Information. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds) Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008. IFIP International Federation for Information Processing, vol 273. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-09680-3_23
Download citation
DOI: https://doi.org/10.1007/978-0-387-09680-3_23
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-09679-7
Online ISBN: 978-0-387-09680-3
eBook Packages: Computer ScienceComputer Science (R0)