{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T01:18:52Z","timestamp":1725671932665},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288906"},{"type":"electronic","value":"9783642288913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_19","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"181-194","source":"Crossref","is-referenced-by-count":0,"title":["Specification in PDL with Recursion"],"prefix":"10.1007","author":[{"given":"Xinxin","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bingtian","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic Verification Methods for Finite State Systems","author":"K. Larsen","year":"1990","unstructured":"Larsen, K.: Modal Specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 232\u2013246. Springer, Heidelberg (1990)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/BFb0012782","volume-title":"Automata, Languages, and Programming","author":"D. Kozen","year":"1982","unstructured":"Kozen, D.: Results on the propositional mu\u2013calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol.\u00a0140, pp. 348\u2013359. Springer, Heidelberg (1982)"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. System Sci.\u00a018(2) (1979)","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Lange, M.: Model checking propositional dynamic logic with all extras. Journal of Applied Logic\u00a04 (2006)","DOI":"10.1016\/j.jal.2005.08.002"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-540-87873-5_5","volume-title":"Verified Software: Theories, Tools, Experiments","author":"D. Leivant","year":"2008","unstructured":"Leivant, D.: Propositional Dynamic Logic for Recursive Procedures. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 6\u201314. Springer, Heidelberg (2008)"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"L\u00f6ding, C., Lutz, C., Serre, O.: Propositional dynamic logic with recursive programs. Journal Logic and Algebraic Programming\u00a073 (2007)","DOI":"10.1016\/j.jlap.2006.11.003"},{"key":"19_CR8","unstructured":"Clarke, E., Grumberg Jr., O., Peled, D.: Model checking. MIT Press (1999)"},{"key":"19_CR9","unstructured":"Liu, X., Xue, B.: Recursive pdl with nesting (in preparing)"},{"key":"19_CR10","unstructured":"Liu, X., Xue, B.: Decomposition of pdl and its extension. Submitted to International Conference on Computer Science, Hongkong (2012)"},{"key":"19_CR11","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","volume":"81","author":"R.S. Streett","year":"1989","unstructured":"Streett, R.S., Emerson, E.A.: An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation\u00a081, 249\u2013264 (1989)","journal-title":"Information and Computation"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/3-540-12896-4_370","volume-title":"Logics of Programs","author":"D. Kozen","year":"1984","unstructured":"Kozen, D., Parikh, R.: A decision procedure for the propositional mu\u2013calculus. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol.\u00a0164, pp. 313\u2013325. Springer, Heidelberg (1984)"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/3-540-53982-4_21","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"B. Jonsson","year":"1991","unstructured":"Jonsson, B., Larsen, K.: On the Complexity of Equation Solving in Process Algebra. In: Abramsky, S. (ed.) TAPSOFT 1991. LNCS, vol.\u00a0493, pp. 381\u2013396. Springer, Heidelberg (1991)"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/BFb0032056","volume-title":"Automata, Languages and Programming","author":"K. Larsen","year":"1990","unstructured":"Larsen, K., Liu, X.: Compositionality Through an Operational Semantics of Contexts. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 526\u2013539. Springer, Heidelberg (1990)"},{"key":"19_CR15","unstructured":"Milner, R.: Communication and Concurrency. Prentice\u2013Hall (1989)"},{"key":"19_CR16","unstructured":"Walukiewicz, I.: Notes on the propositional \u03bc-calculus: completeness and related results, brics nots series, Tech. Rep. NS-95-1 (1995)"},{"key":"19_CR17","unstructured":"Larsen, K., Liu, X.: Equation solving using modal transition systems. In: Proceedings on Logic in Computer Science (1990)"},{"key":"19_CR18","unstructured":"Liu, X.: Specification and decomposition in concurrency, Ph.D. dissertation, University of Aalborg, Fredrik Bajers Vej 7, DK 9220 Aalborg \u00f8, Denmark (1992)"},{"key":"19_CR19","unstructured":"Larsen, K., Xinxin, L.: On equation solving. In: Larsen, K., Skou, A. (eds.) 2nd NOrdic Workshop on Program Correctness (1990)"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1007\/3-540-52559-9_76","volume-title":"Stepwise Refinement of Distributed Systems","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G.: Compositional Theories based on an Operational Semantics of Contexts. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol.\u00a0430, pp. 487\u2013518. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:14:16Z","timestamp":1620126856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}