{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:11:59Z","timestamp":1748751119315,"version":"3.41.0"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319254227"},{"type":"electronic","value":"9783319254234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25423-4_22","type":"book-chapter","created":{"date-parts":[[2015,11,30]],"date-time":"2015-11-30T17:10:46Z","timestamp":1448903446000},"page":"336-348","source":"Crossref","is-referenced-by-count":1,"title":["A Recursive Probabilistic Temporal Logic"],"prefix":"10.1007","author":[{"given":"Pablo F.","family":"Castro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cecilia","family":"Kilmurray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,1]]},"reference":[{"key":"22_CR1","volume-title":"Model Checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"22_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C.: LiQuor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, pp. 131\u2013132. IEEE Computer Society (2006)","DOI":"10.1109\/QEST.2006.25"},{"key":"22_CR5","volume-title":"A Practical Introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, New York (2006)"},{"key":"22_CR6","unstructured":"Cohen, B., Venkataramanan, S., Kumari, A., Piper, L.: System Verilog Assertions Handbook. VhdlCohen Publishing (2010)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Armoni","year":"2002","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., et al.: The ForSpec temporal logic: a new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 296. Springer, Heidelberg (2002)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1007\/3-540-45061-0_67","volume-title":"Automata, Languages and Programming","author":"C Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., McIsaac, A., Campenhout, D.V.: The definition of a temporal clock operator. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 857\u2013870. Springer, Heidelberg (2003)"},{"key":"22_CR9","unstructured":"Mio, M.: Game Semantics for Probabilistic $$\\mu $$ \u03bc -Calculi. Ph.D. thesis, University of Edinburgh (2012)"},{"key":"22_CR10","unstructured":"Castro, P.F., Kilmurray, C., Piterman, N.: Tractable probabilistic $$\\mu $$ \u03bc -calculus that expresses probabilistic temporal logics. In: 32nd International Symposium on Theoretical Aspects of Computer Science. LIPIcs, Garching, Germany, pp. 211\u2013223 (2015)"},{"key":"22_CR11","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1016\/j.peva.2012.05.005","volume":"69","author":"M Huth","year":"2012","unstructured":"Huth, M., Piterman, N., Wagner, D.: p-automata: new foundations for discrete-time probabilistic verification. Perform. Eval. 69, 356\u2013378 (2012)","journal-title":"Perform. Eval."},{"key":"22_CR12","first-page":"1015","volume":"19","author":"A Arora","year":"1993","unstructured":"Arora, A., Gouda, M.: Closure and convergence: a foundation of fault-tolerant computing. TOSEM 19, 1015\u20131027 (1993)","journal-title":"TOSEM"},{"key":"22_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1145\/963778.963782","volume":"26","author":"P Attie","year":"2004","unstructured":"Attie, P., Arora, A., Emerson, A.: Synthesis of fault-tolerant concurrent programs. TOPLAS 26, 125\u2013185 (2004)","journal-title":"TOPLAS"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: 12th IEEE Symposium on Logic in Computer Science, pp. 111\u2013122. IEEE Computer Society (1997)","DOI":"10.1109\/LICS.1997.614940"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Results on the quantitative qm $$\\mu $$ \u03bc . ACM Trans. Comput. Log. 8 (2007)","DOI":"10.1145\/1182613.1182616"},{"key":"22_CR16","unstructured":"Mio, M., Simpson, A.: \u0141ukasiewicz $$\\mu $$ \u03bc -calculus. In: FICS (2013)"},{"key":"22_CR17","unstructured":"Liu, W., Song, L., Wang, J., Zhang, L.: A simple probabilistic extension of model $$\\mu $$ \u03bc -calculus. In: 23rd International Joint Conference on Artificial Intelligence, Buenos Aires, Argentina. AAAI Press, pp. 882\u2013888 (2015)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25423-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T16:15:40Z","timestamp":1748708140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25423-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319254227","9783319254234"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25423-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}