{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T09:30:58Z","timestamp":1725701458338},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642329395"},{"type":"electronic","value":"9783642329401"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32940-1_37","type":"book-chapter","created":{"date-parts":[[2012,9,1]],"date-time":"2012-09-01T16:47:02Z","timestamp":1346518022000},"page":"531-546","source":"Crossref","is-referenced-by-count":0,"title":["Propositional Dynamic Logic with Converse and Repeat for Message-Passing Systems"],"prefix":"10.1007","author":[{"given":"Roy","family":"Mennicke","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"37_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-540-77050-3_25","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"B. Bollig","year":"2007","unstructured":"Bollig, B., Kuske, D., Meinecke, I.: Propositional Dynamic Logic for Message-Passing Systems. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855, pp. 303\u2013315. Springer, Heidelberg (2007)"},{"key":"37_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-89439-1_16","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Dax","year":"2008","unstructured":"Dax, C., Klaedtke, F.: Alternation Elimination by Complementation (Extended Abstract). In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 214\u2013229. Springer, Heidelberg (2008)"},{"issue":"2","key":"37_CR3","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci.\u00a018(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"37_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-540-45187-7_15","volume-title":"CONCUR 2003 - Concurrency Theory","author":"P. Gastin","year":"2003","unstructured":"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.\u00a02761, pp. 222\u2013236. Springer, Heidelberg (2003)"},{"key":"37_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-540-45138-9_38","volume-title":"Mathematical Foundations of Computer Science 2003","author":"P. Gastin","year":"2003","unstructured":"Gastin, P., Oddoux, D.: LTL with Past and Two-Way Very-Weak Alternating Automata. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 439\u2013448. Springer, Heidelberg (2003)"},{"issue":"6","key":"37_CR6","doi-asserted-by":"publisher","first-page":"920","DOI":"10.1016\/j.ic.2006.01.005","volume":"204","author":"B. Genest","year":"2006","unstructured":"Genest, B., Kuske, D., Muscholl, A.: A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput.\u00a0204(6), 920\u2013956 (2006)","journal-title":"Inf. Comput."},{"key":"37_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1007\/3-540-45465-9_56","volume-title":"Automata, Languages and Programming","author":"B. Genest","year":"2002","unstructured":"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.\u00a02380, pp. 657\u2013668. Springer, Heidelberg (2002)"},{"key":"37_CR8","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"issue":"3","key":"37_CR9","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0304-3975(90)90096-Z","volume":"75","author":"S. Katz","year":"1990","unstructured":"Katz, S., Peled, D.: Interleaving set temporal logic. Theor. Comput. Sci.\u00a075(3), 263\u2013287 (1990)","journal-title":"Theor. Comput. Sci."},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055036","volume-title":"Automata, Languages and Programming","author":"Y. Kesten","year":"1998","unstructured":"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.\u00a01443, pp. 1\u201316. Springer, Heidelberg (1998)"},{"key":"37_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-36387-4_6","volume-title":"Automata, Logics, and Infinite Games","author":"R. K\u00fcsters","year":"2002","unstructured":"K\u00fcsters, R.: Memoryless Determinacy of Parity Games. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500, pp. 95\u2013106. Springer, Heidelberg (2002)"},{"key":"37_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/3-540-45294-X_22","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"P. Madhusudan","year":"2001","unstructured":"Madhusudan, P., Meenakshi, B.: Beyond Message Sequence Graphs. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 256\u2013267. Springer, Heidelberg (2001)"},{"key":"37_CR13","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theor. Comput. Sci.\u00a054, 267\u2013276 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"37_CR14","doi-asserted-by":"crossref","unstructured":"Peled, D.: Specification and verification of message sequence charts. In: FORTE. FIP Conference Proceedings, vol.\u00a0183, pp. 139\u2013154. Kluwer (2000)","DOI":"10.1007\/978-0-387-35533-7_9"},{"key":"37_CR15","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Semantical considerations on floyd-hoare logic. In: FOCS, pp. 109\u2013121. IEEE (1976)","DOI":"10.1109\/SFCS.1976.27"},{"key":"37_CR16","doi-asserted-by":"crossref","unstructured":"Streett, R.S.: Propositional dynamic logic of looping and converse. In: STOC, pp. 375\u2013383. ACM (1981)","DOI":"10.1145\/800076.802492"},{"key":"37_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/BFb0015261","volume-title":"Computer Science Today","author":"M.Y. Vardi","year":"1995","unstructured":"Vardi, M.Y.: Alternating Automata and Program Verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 471\u2013485. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2012 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32940-1_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:49:41Z","timestamp":1620114581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32940-1_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642329395","9783642329401"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32940-1_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}