{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T15:10:33Z","timestamp":1787497833051,"version":"build-2736575974"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540657194","type":"print"},{"value":"9783540490197","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49019-1_20","type":"book-chapter","created":{"date-parts":[[2007,8,7]],"date-time":"2007-08-07T01:47:45Z","timestamp":1186451265000},"page":"288-305","source":"Crossref","is-referenced-by-count":9,"title":["Probabilistic Temporal Logics via the Modal Mu-Calculus"],"prefix":"10.1007","author":[{"given":"Murali","family":"Narasimha","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Purush","family":"Iyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. It usually works: The temporal logic of stochastic systems. In Proc of Computer Aided Verification\u2019 95. Springer-Verlag, July 1995.","DOI":"10.1007\/3-540-60045-0_48"},{"key":"20_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Proc. Foundations of software technology and theoretical computer science","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model-checking of probabilistic and non-deterministic systems. In Proc. Foundations of software technology and theoretical computer science, Lecture notes in Computer science, vol 1026, pages 499\u2013513. Springer-Verlag, December 1995."},{"issue":"5","key":"20_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/277652.277653","volume":"33","author":"R. Bodik","year":"1998","unstructured":"Rastislav Bodik, Rajiv Gupta, and Mary Lou Soffa. Complete removal of redundant computations. ACM SIGPLAN Notices, 33(5):1\u201314, May 1998.","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Thomas Ball and James R. Larus. Optimally profiling and tracing progranis. In Ravi Sethi, editor, Proceedings of the 19th Annual Symposium on Principles of Programming Languages, pages 59\u201370, Albuquerque, NM, January 1992. ACM Press.","DOI":"10.1145\/143165.143180"},{"issue":"2","key":"20_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"8","key":"20_CR6","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"Rance Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27(8):725\u2013747, 1990.","journal-title":"Acta Informatica"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Proc. 1988 IEEE Symp. on the Foundations of Comp. Sci., 1988.","DOI":"10.1109\/SFCS.1988.21950"},{"issue":"1","key":"20_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. A. Emerson","year":"1986","unstructured":"E. A. Emerson and J. Y. Halpern. \u201csometimes\u201d and \u201cnot never\u201d revisited: On branching time versus linear time temporal logic. JACM, 33(1):151\u2013178, 1986.","journal-title":"JACM"},{"key":"20_CR9","first-page":"267","volume-title":"Proceedings 1st Annual IEEE Symp. on Logic in Computer Science, LICS\u201986, Cambridge, MA, USA, 16-18 June 1986","author":"E.A. Emerson","year":"1986","unstructured":"E. Allen Emerson and Chin-Laung Lei. Efficient model-checking in fragments of the propositional mu-calculus. In Proceedings 1st Annual IEEE Symp. on Logic in Computer Science, LICS\u201986, Cambridge, MA, USA, 16-18 June 1986, pages 267\u2013278. IEEE Computer Society Press, Los Alamitos, CA, 1986."},{"key":"20_CR10","unstructured":"H. Hansson. Time and Probability in Formal Design of Distributed Systems. Elsevier, 1994."},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Michael Huth and Marta Kwiatkowska. Quantitative analysis and model checking. In Proceedings, Twelth Annual IEEE Symposium on Logic in Computer Science, pages 111\u2013122, Warsaw, Poland, 29 June-2 July 1997. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1997.614940"},{"issue":"1","key":"20_CR12","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association of Computing Machinery, 32(1):137\u2013161, 1985.","journal-title":"Journal of the Association of Computing Machinery"},{"issue":"1","key":"20_CR13","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoretical Computer Science, 27(1):333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"20_CR14","unstructured":"J. G. Kemeny, J. L. Snell, and A. W. Knapp. Denumerable Markov Chains. Van Nostrand, New Jersey, 1966."},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94, 1991.","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"20_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"McMillan, K. L. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993."},{"key":"20_CR17","volume-title":"Introduction to Probablistic Automata","author":"A. Paz","year":"1971","unstructured":"Azaria Paz. Introduction to Probablistic Automata. Academic Press, New York, 1971."},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"A. Philippou, O. Sokolksy, R. Cleaveland, I. Lee, and S. Smolka. Probabilistic resource failure in real-time process algebra. 1998. To appear in Proceedings of CONCUR.","DOI":"10.1007\/BFb0055637"},{"issue":"1","key":"20_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"Amir Pnueli and Lenore D. Zuck. Probabilistic verification. Information and Computation, 103(1):1\u201329, March 1993.","journal-title":"Information and Computation"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"G. Ramalingam. Data flow frequency analysis. In Proceedings of the ACM SIGPLAN\u2019 96 Conference on Programming Language Design and Implementation, pages 267\u2013277, Philadelphia, Pennsylvania, 21-24 May 1996.","DOI":"10.1145\/231379.231433"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"David A. Schmidt. Data flow analysis is model checking of abstract interpretation. In Conference Record of POPL\u2019 98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 38\u201348, San Diego, California, 19-21 January 1998.","DOI":"10.1145\/268946.268950"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"R. Segala. A compositional trace-based semantics for probabilistic automata. In CONCUR95, pages 324\u2013338, 1995.","DOI":"10.1007\/3-540-60218-6_17"},{"key":"20_CR23","series-title":"Lect Notes Comput Sci","first-page":"385","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"A. P. Sistla","year":"1993","unstructured":"A. P. Sistla, A. Emerson, and C. Jutla. Model checking in fragments of the mu-calculus. In Proceedings of the International Conference on Computer Aided Verification, volume Vol 697 of LNCS, pages 385\u2013396. Springer-Verlag, June 1993."},{"key":"20_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Data flow analysis as model checking","author":"B. Steffen","year":"1991","unstructured":"Bernhard Steffen. Data flow analysis as model checking. Lecture Notes in Computer Science, vol. 526, 1991."},{"key":"20_CR25","first-page":"478","volume":"2","author":"C. Stirling","year":"1992","unstructured":"C. Stirling. Modal and Temporal Logics, volume 2 of Handbook of Logic in Computer Science, pages 478\u2013551. Oxford Science Press, 1992.","journal-title":"Handbook of Logic in Computer Science"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"M. Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In IEEE Symposium on Foundations of Computer Science, pages 327\u2013338, 1985.","DOI":"10.1109\/SFCS.1985.12"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Rob van Glabbeek, Scott A. Smolka, Bernhard Steffen, and Chris M. N. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proc. of Fifth Annual IEEE Symposium on Logic in Computer Science, pages 130\u2013141. IEEE Computer Society Press, June 1990.","DOI":"10.1109\/LICS.1990.113740"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49019-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T16:06:23Z","timestamp":1556726783000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49019-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657194","9783540490197"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-49019-1_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}