{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:28:51Z","timestamp":1742992131064,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402534"},{"type":"electronic","value":"9783540448808"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44880-2_15","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"216-239","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Probabilistic Termination in B"],"prefix":"10.1007","author":[{"given":"Annabelle","family":"McIver","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carroll","family":"Morgan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thai Son","family":"Hoang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial, D. Cansell, and D. Mery. A mechanically proved and incremental development of the IEEE 1394 Tree Identify Protocol. Formal Aspects of Computing, 14(3), 2002.","DOI":"10.1007\/s001650300002"},{"key":"15_CR3","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice Hall International, Englewood Cliffs, N.J., 1976."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"C. J. Fidge and C. Shankland. But what if I don\u2019t want to wait forever? Formal Aspects of Computing, 2002. To appear.","DOI":"10.1007\/s001650300006"},{"key":"15_CR5","unstructured":"G. Grimmett and D. Welsh. Probability: an Introduction. Oxford Science Publications, 1986."},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/2166.357214","volume":"5","author":"S. Hart","year":"1983","unstructured":"S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent programs. ACM Transactions on Programming Languages and Systems, 5:356\u2013380, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings 15th International Conference on Theorem Proving and Higher Order Logic, 20\u201323 August 2002. Hampton, Virginia","author":"J. Hurd","year":"2002","unstructured":"Joe Hurd. A formal approach to probabilistic termination. In Proceedings 15th International Conference on Theorem Proving and Higher Order Logic, 20\u201323 August 2002. Hampton, Virginia, volume 2410 of LNCS. Springer Verlag, 2002."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"D. Kozen. A probabilistic PDL. In Proceedings of the 15th ACM Symposium on Theory of Computing, New York, 1983. ACM.","DOI":"10.1145\/800061.808758"},{"key":"15_CR9","unstructured":"S. Maharaj, J.M.T. Romijn, and C. Shankland. An introduction to the IEEE 1394 FireWire. Formal Aspects of Computing, 2002. To appear."},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s002360000046","volume":"37","author":"A.K. McIver","year":"2001","unstructured":"A.K. McIver and C. Morgan. Demonic, angelic and unbounded probabilistic choices in sequential programs. Acta Informatica, 37:329\u2013354, 2001.","journal-title":"Acta Informatica"},{"key":"15_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 2nd International B Conference B\u201998","author":"C. Morgan","year":"1998","unstructured":"Carroll Morgan. The generalised substitution language extended to probabilistic programs. In Proc. 2nd International B Conference B\u201998, volume 1393 of LNCS, 1998. Also available at [22, B98]."},{"issue":"6","key":"15_CR12","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1093\/jigpal\/7.6.779","volume":"7","author":"C. Morgan","year":"1999","unstructured":"Carroll Morgan and Annabelle McIver. An expectation-based model for probabilistic temporal logic. Logic Journal of the IGPL, 7(6):779\u2013804, 1999. Also available at [22, MM97].","journal-title":"Logic Journal of the IGPL"},{"key":"15_CR13","unstructured":"Carroll Morgan and Annabelle McIver. pGCL: Formal reasoning for random algorithms. South African Computer Journal, 22, March 1999. Also available at [22, pGCL]."},{"key":"15_CR14","unstructured":"Carroll Morgan and Annabelle McIver. Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL. In Proceedings CATS\u2019 01. Elsevier, 2000. Also available at [22, PROB-1]; to appear in Theoretical Computer Science."},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"C.C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3), July 1988. Reprinted in [19].","DOI":"10.1145\/44501.44503"},{"key":"15_CR16","unstructured":"C.C. Morgan. Programming from Specifications. Prentice-Hall, second edition, 1994. At http:\/\/web.comlab.ox.ac.uk\/oucl\/publications\/books\/PfS."},{"key":"15_CR17","unstructured":"C.C. Morgan. Proof rules for probabilistic loops. In He Jifeng, John Cooke, and Peter Wallis, editors, Proceedings of the BCS-FACS 7th Refinement Workshop, Workshops in Computing. Springer Verlag, July 1996. At http:\/\/www.springer.co.uk\/ewic\/workshops\/7RW; also available at [22, M95]."},{"issue":"3","key":"15_CR18","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C.C. Morgan","year":"1996","unstructured":"C.C. Morgan, A.K. McIver, and K. Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325\u2013353, May 1996.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"C.C. Morgan and T.N. Vickers, editors. On the Refinement Calculus. FACIT Series in Computer Science. Springer Verlag, Berlin, 1994.","DOI":"10.1007\/978-1-4471-3273-8"},{"issue":"4","key":"15_CR20","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G. Nelson","year":"1989","unstructured":"G. Nelson. A generalization of Dijkstra\u2019s calculus. ACM Transactions on Programming Languages and Systems, 11(4):517\u2013561, October 1989.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR21","unstructured":"C. Paulin-Mohring. Randomized algorithms in type theory. Presentation at Daghstuhl Workshop, August 2001."},{"key":"15_CR22","unstructured":"PSG. Probabilistic Systems Group: Collected reports. At http:\/\/web.comlab.ox.ac.uk\/oucl\/research\/areas\/probs\/bibliography.html."},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"J.R. Rao. Reasoning about probabilistic parallel programs. ACM Transactions on Programming Languages and Systems, 16(3), May 1994.","DOI":"10.1145\/177492.177724"},{"key":"15_CR24","unstructured":"M.I.A. Stoelinga. Fun with FireWire: Experiments with verifying the IEEE 1394 Root Contention Protocol. In S. Maharaj, C. Shankland, and J.M.T. Romijn, editors, Formal Aspects of Computing, 2002. To appear."}],"container-title":["Lecture Notes in Computer Science","ZB 2003: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44880-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T01:57:43Z","timestamp":1676685463000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"27 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}