{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T17:43:23Z","timestamp":1770918203265,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540222651","type":"print"},{"value":"9783540246114","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24611-4_5","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T19:01:10Z","timestamp":1267124470000},"page":"147-188","source":"Crossref","is-referenced-by-count":81,"title":["On Probabilistic Computation Tree Logic"],"prefix":"10.1007","author":[{"given":"Frank","family":"Ciesinski","sequence":"first","affiliation":[]},{"given":"Marcus","family":"Gr\u00f6\u00dfer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Alur, Dill: A theory of timed automata. Theoretical Computer Science, 183\u2013235 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Automata, Languages and Programming, 18th International Colloquium","author":"R. Alur","year":"1991","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for probabilistic real-time systems (extended abstract). In: Albert, J.L., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) Automata, Languages and Programming, 18th International Colloquium. LNCS, vol.\u00a0510, pp. 115\u2013126. Springer, Heidelberg (1991)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R.K.: CAV 1995. LNCS, vol.\u00a0939, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"key":"5_CR4","unstructured":"Baier, C.: On algorithmic verification methods for probabilistic systems, Habilitation thesis (November 1998)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 146\u2013161. Springer, Heidelberg (1999)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Automata, Languages and Programming","author":"C. Baier","year":"1997","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M.Z., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, pp. 430\u2013440. Springer, Heidelberg (1997)"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/s002360050136","volume":"35","author":"Beauquier","year":"1998","unstructured":"Beauquier, Slissenko: Polytime model checking for timed probabilistic computation tree logic. Acta Informatica\u00a035, 645\u2013664 (1998)","journal-title":"Acta Informatica"},{"issue":"8","key":"5_CR8","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/s002360050136","volume":"35","author":"D. Beauquier","year":"1998","unstructured":"Beauquier, D., Slissenko, A.: Polytime model checking for timed probabilistic computation tree logic. Acta Informatica\u00a035(8), 645\u2013664 (1998)","journal-title":"Acta Informatica"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., De Alfaro, L.: FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11 (1998)","DOI":"10.1007\/s004460050046"},{"issue":"2","key":"5_CR11","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Allen Emerson, E., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR12","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"5_CR13","first-page":"338","volume-title":"29th Annual Symposium on Foundations of Computer Science","author":"C. Courcoubetis","year":"1988","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, October 24\u201326, pp. 338\u2013345. IEEE, Los Alamitos (1988)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/BFb0032043","volume-title":"Automata, Languages and Programming","author":"C. Courcoubetis","year":"1990","unstructured":"Courcoubetis, C., Yannakakis, M.: Markov decision processes and regular events (extended abstract). In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 336\u2013349. Springer, Heidelberg (1990)"},{"issue":"4","key":"5_CR15","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of Process Algebra and Probabilistic Methods. Performance Modeling and Verification. Joint International Workshop, PAPM-PROBMIV 2001","author":"P.R. D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) Proceedings of Process Algebra and Probabilistic Methods. Performance Modeling and Verification. Joint International Workshop, PAPM-PROBMIV 2001, Copenhagen, Denmark. LNCS, Springer, Heidelberg (2001)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/BFb0023457","volume-title":"STACS 97","author":"L. Alfaro De","year":"1997","unstructured":"De Alfaro, L.: Temporal logics for the specification of performance and reliability. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol.\u00a01200, pp. 165\u2013176. Springer, Heidelberg (1997)"},{"key":"5_CR18","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. Thesis CS-TR-98- 1601, Stanford University, Department of Computer Science, June 1998."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Emerson, Mok, Sistla, Srinivasan: Quantitative temporal reasoning. Journal of Real Time System, 331\u2013352 (1992)","DOI":"10.1007\/BF00355298"},{"issue":"1","key":"5_CR20","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u2018Sometimes\u2019 and \u2018not never\u2019 revisited: on branching time versus linear time temporal logic. Journal of the ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"Journal of the ACM"},{"key":"5_CR21","series-title":"Formal Models and Semantics","first-page":"995","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol.\u00a0B, pp. 995\u20131072. Elsevier Science Publishers, Amsterdam (1990)"},{"key":"5_CR22","volume-title":"An Intro. to Probability Theory and its application.","author":"W. Feller","year":"1968","unstructured":"Feller, W.: An Intro. to Probability Theory and its application. John Wiley and Sons, New York (1968)"},{"key":"5_CR23","volume-title":"Series in Real-Time Safety Critical Systems","author":"H. Hansson","year":"1994","unstructured":"Hansson, H.: Time and Probability in Formal Design of Distributed Systems. In: Series in Real-Time Safety Critical Systems. Elsevier, Amsterdam (1994)"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1109\/REAL.1990.128759","volume-title":"Proceedings of the Real- Time Systems Symposium - 1990","author":"H. Hansson","year":"1990","unstructured":"Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabitilies. In: IEEE Computer Society Press (ed.) Proceedings of the Real- Time Systems Symposium - 1990, Lake Buena Vista, Florida, USA, pp. 278\u2013287. IEEE Computer Society Press, Los Alamitos (1990)"},{"issue":"5","key":"5_CR25","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"5_CR26","unstructured":"Hansson, H.A.: Time and probability in formal design of distributed systems. SICS Dissertation Series 05, Swedish Institute of Computer Science, Box 1263, S-164 28 Kista, Sweden (1994)"},{"issue":"3","key":"5_CR27","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/2166.357214","volume":"5","author":"S. Hart","year":"1983","unstructured":"Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent programs. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a05(3), 356\u2013380 (1983)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/3-540-45694-5_24","volume-title":"CONCUR 2002 - Concurrency Theory","author":"R. Jagadeesan","year":"2002","unstructured":"Jagadeesan, R., Desharnais, J., Gupta, V., Panangaden, P.: Weak bisimulation is sound and complete for PCTL*. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 355\u2013370. Springer, Heidelberg (2002)"},{"key":"5_CR29","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1109\/LICS.1991.151651","volume-title":"Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science","author":"B. Jonsson","year":"1991","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, July15\u201318, pp. 266\u2013277. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/BFb0039071","volume-title":"CONCUR 1990: Theories of Concurrency: Unification and Extension","author":"C.-C. Jou","year":"1990","unstructured":"Jou, C.-C., Smolka, S.A.: Equivalences, congruences, and complete axiomatizations for probabilistic processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol.\u00a0458, pp. 367\u2013383. Springer, Heidelberg (1990)"},{"key":"5_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K. Larsen","year":"1991","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput.\u00a094, 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"5_CR32","volume-title":"Finite Markov Chains","author":"J.G. Kemeny","year":"1960","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Princeton University Press, Princeton (1960)"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 75\u201395. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48778-6_5"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. LNCS, vol.\u00a01877. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-44618-4_11"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-45605-8_11","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 169\u2013187. Springer, Heidelberg (2002)"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Computer Performance Evaluation \/ TOOLS, pp. 200\u2013204 (2002)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"5_CR37","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. PhD thesis, Carnegie Mellon University, Pittsburgh (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"5_CR39","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distributed Computing\u00a01, 53\u201372 (1986)","journal-title":"Distributed Computing"},{"key":"5_CR40","first-page":"322","volume-title":"Symposium on Logic in Computer Science","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Probabilistic verification by tableaux. In Proceedings. In: Symposium on Logic in Computer Science, Cambridge, Massachusetts, June 16\u201318, pp. 322\u2013331. IEEE Computer Society, Los Alamitos (1986)"},{"issue":"1","key":"5_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"Pnueli, A., Zuck, L.D.: Probabilistic verification. Information and Computation\u00a0103(1), 1\u201329 (1993)","journal-title":"Information and Computation"},{"key":"5_CR42","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes\u2014Discrete Stochastic Dynamic Programming","author":"M.L. Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes\u2014Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York (1994)"},{"key":"5_CR43","first-page":"319","volume-title":"29th Annual Symposium on Foundations of Computer Science","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, October 24\u201326 1988, pp. 319\u2013327. IEEE, Los Alamitos (1988)"},{"key":"#cr-split#-5_CR44.1","unstructured":"R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology (June 1995);"},{"key":"#cr-split#-5_CR44.2","unstructured":"Available as Technical Report MIT\/LCS\/TR-676"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. LNCS, vol.\u00a0836, pp. 481\u2013496. Springer, Heidelberg (1994)","DOI":"10.1007\/978-3-540-48654-1_35"},{"issue":"2","key":"5_CR46","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing\u00a02(2), 250\u2013273 (Summer 1995)","journal-title":"Nordic Journal of Computing"},{"key":"5_CR47","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a04, pp. 133\u2013191. Elsevier Science Publishers B.V., Amsterdam (1990)"},{"key":"5_CR48","doi-asserted-by":"crossref","unstructured":"Campos, S., Hartonas-Garmhausen, V., Clarke, E.: Probverus: Probabilistic symbolic model checking. LNCS, vol.\u00a01601, pp. 96\u2013110. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48778-6_6"},{"key":"5_CR49","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1109\/SFCS.1985.12","volume-title":"26th Annual Symposium on Foundations of Computer Science","author":"M.Y. Vardi","year":"1985","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: 26th Annual Symposium on Foundations of Computer Science, Los Angeles, Ca., USA, October 1985, pp. 327\u2013338. IEEE Computer Society Press, Los Alamitos (1985)"},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-48778-6_16","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"M.Y. Vardi","year":"1999","unstructured":"Vardi, M.Y.: Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 265\u2013276. Springer, Heidelberg (1999)"},{"key":"5_CR51","first-page":"332","volume-title":"Proceedings, Symposium on Logic in Computer Science","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings, Symposium on Logic in Computer Science, Cambridge, Massachusetts, June 16\u201318, pp. 332\u2013344. IEEE Computer Society, Los Alamitos (1986)"}],"container-title":["Lecture Notes in Computer Science","Validation of Stochastic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24611-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T16:51:51Z","timestamp":1685465511000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24611-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540222651","9783540246114"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24611-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}