{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:37:25Z","timestamp":1725550645889},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291077"},{"type":"electronic","value":"9783540320722"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560647_29","type":"book-chapter","created":{"date-parts":[[2005,10,20]],"date-time":"2005-10-20T14:04:06Z","timestamp":1129817046000},"page":"439-453","source":"Crossref","is-referenced-by-count":2,"title":["Quantitative Temporal Logic Mechanized in HOL"],"prefix":"10.1007","author":[{"given":"Orieta","family":"Celiku","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica\u00a020, 207\u2013226 (1983)","journal-title":"Acta Informatica"},{"issue":"2","key":"29_CR2","first-page":"102","volume":"11","author":"O. Celiku","year":"2004","unstructured":"Celiku, O., McIver, A.: Cost-based analysis of probabilistic programs mechanised in HOL. Nordic Journal of Computing\u00a011(2), 102\u2013128 (2004)","journal-title":"Nordic Journal of Computing"},{"key":"29_CR3","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"29_CR4","unstructured":"Erlangen-Twente Markov Chain Checker, http:\/\/www.informatik.uni-erlangen.de\/etmcc\/"},{"key":"29_CR5","volume-title":"Introduction to HOL (A theorem-proving environment for higher order logic)","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, Cambridge (1993)"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-48778-6_6","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"V. Hartonas-Garmhausen","year":"1999","unstructured":"Hartonas-Garmhausen, V., Campos, S.V.A., Clarke, E.M.: Probverus: Probabilistic symbolic model checking. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 96\u2013110. Springer, Heidelberg (1999)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-44880-2_16","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"T.S. Hoang","year":"2003","unstructured":"Hoang, T.S., Jin, Z., Robinson, K., McIver, A., Morgan, C.: Probabilistic invariants for probabilistic machines. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 240\u2013259. Springer, Heidelberg (2003)"},{"key":"29_CR8","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. In: Proc. of QAPL 2004 (March 2004)","DOI":"10.1016\/j.entcs.2004.01.021"},{"key":"29_CR10","unstructured":"Jeannet, B., D\u2019Argenio, P., Larsen, K.: Rapture: A tool for verifying Markov Decision Processes. In: Cerna, I. (ed.) Tools Day 2002, Brno, Czech Republic, Technical Report. Faculty of Informatics, Masaryk University Brno (2002)"},{"key":"29_CR11","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"issue":"3","key":"29_CR13","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1016\/S0304-3975(02)00612-6","volume":"293","author":"A. McIver","year":"2003","unstructured":"McIver, A., Morgan, C.: Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL. Theoretical Computer Science\u00a0293(3), 507\u2013534 (2003)","journal-title":"Theoretical Computer Science"},{"key":"29_CR14","volume-title":"Abstraction, refinement and proof for probabilistic systems","author":"A. McIver","year":"2004","unstructured":"McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Springer, Heidelberg (2004)"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-44880-2_15","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"A. McIver","year":"2003","unstructured":"McIver, A., Morgan, C., Hoang, T.S.: Probabilistic termination in B. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 216\u2013239. Springer, Heidelberg (2003)"},{"key":"29_CR16","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/S0304-3975(01)00049-4","volume":"282","author":"A.K. McIver","year":"2002","unstructured":"McIver, A.K.: Quantitative program logic and expected time bounds in probabilistic distributed algorithms. Theoretical Computer Science\u00a0282, 191\u2013219 (2002)","journal-title":"Theoretical Computer Science"},{"key":"29_CR17","unstructured":"Morgan, C.: Probabilistic temporal logic: qTL. Lectures on Probabilistic Formal Methods for the 2004 RSISE Logic Summer School, Slides available at http:\/\/www.cse.unsw.edu.au\/~carrollm\/canberra04\/"},{"issue":"6","key":"29_CR18","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1093\/jigpal\/7.6.779","volume":"7","author":"C. Morgan","year":"1999","unstructured":"Morgan, C., McIver, A.: An expectation-transformer model for probabilistic temporal logic. Logic Journal of the IGPL\u00a07(6), 779\u2013804 (1999)","journal-title":"Logic Journal of the IGPL"},{"key":"29_CR19","first-page":"14","volume":"22","author":"C. Morgan","year":"1999","unstructured":"Morgan, C., McIver, A.: pGCL: Formal reasoning for random algorithms. South African Computer Journal\u00a022, 14\u201327 (1999)","journal-title":"South African Computer Journal"},{"key":"29_CR20","volume-title":"Programming from Specifications","author":"C.C. Morgan","year":"1990","unstructured":"Morgan, C.C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1990)"},{"issue":"3","key":"29_CR21","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C.C. Morgan","year":"1996","unstructured":"Morgan, C.C., McIver, A.K., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems\u00a018(3), 325\u2013353 (1996)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-24611-4_11","volume-title":"Validation of Stochastic Systems","author":"G. Norman","year":"2004","unstructured":"Norman, G.: Analysing randomized distributed algorithms. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 384\u2013418. Springer, Heidelberg (2004)"},{"key":"29_CR23","unstructured":"Probabilistic Symbolic Model Checker, http:\/\/www.cs.bham.ac.uk\/dxp\/prism\/"},{"key":"29_CR24","unstructured":"Ymer, http:\/\/www.cs.cmu.edu\/~lorens\/ymer.html"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2005"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560647_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T11:08:06Z","timestamp":1586516886000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560647_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291077","9783540320722"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11560647_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}