Abstract
The model checking problem for propositional dynamic logic (PDL) over message sequence charts (MSCs) and communicating finite state machines (CFMs) asks, given a channel bound B, a PDL formula ϕ and a CFM \(\mathcal{C}\), whether every existentially B-bounded MSC M accepted by \(\mathcal{C}\) satisfies ϕ. Recently, it was shown that this problem is PSPACE-complete. In the present work, we consider CRPDL over MSCs which is PDL equipped with the operators converse and repeat. The former enables one to walk back and forth within an MSC using a single path expression whereas the latter allows to express that a path expression can be repeated infinitely often. To solve the model checking problem for this logic, we define global message sequence chart automata (gMSCAs) which are multi-way alternating parity automata walking on MSCs. By exploiting a new concept called concatenation states, we are able to inductively construct, for every CRPDL formula ϕ, a finite set of gMSCAs \(\mathfrak{G}\) such that the set of models of ϕ equals the union of the languages of the gMSCAs from \(\mathfrak{G}\). As a result, we obtain that the model checking problem for CRPDL and CFMs is still in PSPACE.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bollig, B., Kuske, D., Meinecke, I.: Propositional Dynamic Logic for Message-Passing Systems. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 303–315. Springer, Heidelberg (2007)
Dax, C., Klaedtke, F.: Alternation Elimination by Complementation (Extended Abstract). In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 214–229. Springer, Heidelberg (2008)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)
Gastin, P., Kuske, D.: Satisfiability and Model Checking for MSO-Definable Temporal Logics Are in PSPACE. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 222–236. Springer, Heidelberg (2003)
Gastin, P., Oddoux, D.: LTL with Past and Two-Way Very-Weak Alternating Automata. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 439–448. Springer, Heidelberg (2003)
Genest, B., Kuske, D., Muscholl, A.: A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput. 204(6), 920–956 (2006)
Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-State High-Level MSCs: Model-Checking and Realizability. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 657–668. Springer, Heidelberg (2002)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
Katz, S., Peled, D.: Interleaving set temporal logic. Theor. Comput. Sci. 75(3), 263–287 (1990)
Kesten, Y., Pnueli, A., Raviv, L.-o.: Algorithmic Verification of Linear Temporal Logic Specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 1–16. Springer, Heidelberg (1998)
Küsters, R.: Memoryless Determinacy of Parity Games. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 95–106. Springer, Heidelberg (2002)
Madhusudan, P., Meenakshi, B.: Beyond Message Sequence Graphs. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 256–267. Springer, Heidelberg (2001)
Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theor. Comput. Sci. 54, 267–276 (1987)
Peled, D.: Specification and verification of message sequence charts. In: FORTE. FIP Conference Proceedings, vol. 183, pp. 139–154. Kluwer (2000)
Pratt, V.R.: Semantical considerations on floyd-hoare logic. In: FOCS, pp. 109–121. IEEE (1976)
Streett, R.S.: Propositional dynamic logic of looping and converse. In: STOC, pp. 375–383. ACM (1981)
Vardi, M.Y.: Alternating Automata and Program Verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471–485. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mennicke, R. (2012). Propositional Dynamic Logic with Converse and Repeat for Message-Passing Systems. In: Koutny, M., Ulidowski, I. (eds) CONCUR 2012 – Concurrency Theory. CONCUR 2012. Lecture Notes in Computer Science, vol 7454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32940-1_37
Download citation
DOI: https://doi.org/10.1007/978-3-642-32940-1_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32939-5
Online ISBN: 978-3-642-32940-1
eBook Packages: Computer ScienceComputer Science (R0)