{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T19:46:02Z","timestamp":1769975162621,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540600459","type":"print"},{"value":"9783540494133","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_48","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:36:26Z","timestamp":1330277786000},"page":"155-165","source":"Crossref","is-referenced-by-count":109,"title":["It usually works: The temporal logic of stochastic systems"],"prefix":"10.1007","author":[{"given":"Adnan","family":"Aziz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vigyan","family":"Singhal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felice","family":"Balarin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert K.","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model Checking for Probabilistic Real Time Systems. In Proc. of the Colloquium on Automata, Languages, and Programming, pages 115\u2013126, 1991.","DOI":"10.1007\/3-540-54233-7_128"},{"key":"14_CR2","unstructured":"A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, and A. Sangiovanni-Vincentelli. It Usually Works: The Temporal Logic of Stochastic Systems. http:\/\/www-cad.eecs.berkeley.edu:80\/\u00e3dnan\/cav95.1."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Equivalences for Fair Kripke Structures. In International Colloquium on Automata, Languages and Programming. Springer Verlag, July 1994.","DOI":"10.1007\/3-540-58201-0_82"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"R. I. Bahar, E. A. Frohm, C. M. Gaona, G. D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic Decision Diagrams and their Applications. In Proc. Intl. Conf. on Computer-Aided Design, pages 188\u2013192, 1993.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"M. Ben-Or, D. Kozen, and J. Reif. The Complexity of Elementary Algebra and Geometry. In Proc. ACM Symposium on the Theory of Computing, pages 457\u2013464, 1984.","DOI":"10.1145\/800057.808712"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"M. C. Browne, E. M. Clarke, and O. Gr\u00fcmberg. Characterizing Kripke Structures in Temporal Logic. Technical Report CMU-CS-87-104, Department of Computer Science, Carnegie Mellon University, 1987.","DOI":"10.21236\/ADA188620"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"R. Cleavland, S. A. Smolka, and A. Zwarico. Testing Preorders for Probabilistic Processes. In Proc. of the Colloquium on Automata, Languages, and Programming, pages 708\u2013719, 1992.","DOI":"10.1007\/3-540-55719-9_116"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis and M. Yannakakis. Verifying Temporal Properties of Finite State Probabilistic Programs. In Proc. IEEE Symposium on the Foundations of Computer Science, pages 338\u2013345, 1988.","DOI":"10.1109\/SFCS.1988.21950"},{"key":"14_CR9","unstructured":"C. Courcoubetis and M. Yannakakis. Automatic Verification of Finite State Programs. In Proc. of the Colloquium on Automata, Languages, and Programming, pages 326\u2013347, 1990."},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, pages 996\u20131072. Elsevier Science, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"14_CR11","volume-title":"PhD thesis","author":"I. Emiris","year":"1994","unstructured":"Ioannis Emiris. Sparse Elimination and Applications in Kinematics. PhD thesis, University of California at Berkeley, Berkeley, CA, December 1994."},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing, 6:512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"S. Hart and M. Shamir. Probabilistic Temporal Logics for Finite and Bounded Models. In Proc. ACM Symposium on the Theory of Computing, pages 1\u201313, 1984.","DOI":"10.1145\/800057.808660"},{"key":"14_CR14","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1137\/0213021","volume":"13","author":"S. Hart","year":"1984","unstructured":"S. Hart, M. Sharir, and A. Pneuli. Verification of Probabilistic Programs. SIAM Journal of Computation, 13:292\u2013314, 1984.","journal-title":"SIAM Journal of Computation"},{"key":"14_CR15","unstructured":"A. Paz. Introduction to Probabilistic Automata. Academic-Press, 1971."},{"issue":"1","key":"14_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1001","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"A. Pnueli and L. Zuck. Probabilistic verification. Information and Computation, 103(1):1\u201329, 1993.","journal-title":"Information and Computation"},{"key":"14_CR17","volume-title":"PhD thesis","author":"A. Rege","year":"1995","unstructured":"Ashutosh Rege. Efficient Decision Procedures for Fragments of R.C.F. (in preparation). PhD thesis, University of California at Berkeley, Berkeley, CA, June 1995."},{"key":"14_CR18","unstructured":"D. Revuz. Markov Chains. North-Holland, 1975."},{"key":"14_CR19","unstructured":"H. L. Royden. Real Analysis. Macmillan Publishing, 1889."},{"key":"14_CR20","unstructured":"M. Y. Vardi and P. L. Wolper. An Automata-Theoretic Approach to Program Verification. In Proc. IEEE Symposium on Logic in Computer Science, pages 332\u2013334, 1986."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_48.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:51:52Z","timestamp":1742597512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}