{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T00:57:11Z","timestamp":1743123431905,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48778-6_6","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T10:18:07Z","timestamp":1178014687000},"page":"96-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["ProbVerus: Probabilistic Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Vicky","family":"Hartonas-Garmhausen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Campos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ed","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D. Dill. Model Checking for Probabilistic Real-time Systems. Automata, Languages, and Programming 18th International Colloquium Proceedings; Madrid, Spain; 8\u201312 July 1991.","DOI":"10.1007\/3-540-54233-7_128"},{"key":"6_CR2","unstructured":"A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, A.L. Sangiovanni-Vincentelli. It usually works: the temporal logic of stochastic systems. In Proceedings of CAV\u201995."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"S. Campos, E. Clarke, W. Marrero, M. Minea and H. Hiraishi, Computing quantitative characteristics of finite-state real-time systems. In IEEE Real-Time Systems Symposium, 1994.","DOI":"10.1109\/REAL.1994.342709"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"S. Campos and E. Clarke, Real-time symbolic model checking for discrete time models. In AMAST Series in Computing: Theories and Experiences for Real-Time System Development. T. Rus, C. Rattray, editors. World Scientific Publishing Company, 1995.","DOI":"10.1142\/9789812831583_0005"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"S. V. Campos. A Quantitative Approach to the Formal Verification of Real-Time Systems. Ph.D. Thesis, School of Computer Science, Carnegie Mellon University, 1996.","DOI":"10.1007\/3-540-63166-6_46"},{"key":"6_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Logic of Programs: Workshop","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke, E. A. Emerson. Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer Verlag, 1981."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, M. Fujita, P.C. McGeer, K. McMillan, J. C.-Y. Yang, X. Zhao. Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation. IWLS\u2019 93: International Workshop on Logic Synthesis. Tahoe City, May 1993.","DOI":"10.1007\/978-1-4613-1385-4_4"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis, M. Yannakakis. The Complexity of Probabilistic Verification. Journal of the Association for Computing Machinery, Vol. 42, No. 4, July 1995.","DOI":"10.1145\/210332.210339"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"G. Hachtel, E. Macii, A. Pardo, F. Somenzi. Markovian Analysis of Large Finite State Machines. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 15. No. 12, December 1996.","DOI":"10.1109\/43.552081"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"H. Hansson and B. Jonsson. A Framework for Reasoning about Time and Reliability. In Proceedings of 10th IEEE Real Time System Symposium, pp. 102\u2013111, 1989.","DOI":"10.1109\/REAL.1989.63561"},{"key":"6_CR12","unstructured":"H. Hansson. Time and Probability in Formal Design of Distributed Systems. Elsevier, 1994."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"S. Hart and M. Sharir. Probabilistic Temporal Logics for Finite and Bounded Models. In Proceedings of the ACM Symposium on the Theory of Computing, pp. 1\u201313, 1984.","DOI":"10.1145\/800057.808660"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"V. Hartonas-Garmhausen, S. Campos, A. Cimatti, E. Clarke, F. Giunchiglia. Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints. In Proceedings of FTCS-28 The Twenty-Eighth Annual International Symposium on Fault-Tolerant Computing, pages 458\u2013463, June, 1998.","DOI":"10.1109\/FTCS.1998.689498"},{"key":"6_CR15","unstructured":"V. Hartonas-Garmhausen. Probabilistic Symbolic Model Checking with Engineering Models and Applications. Ph.D. Thesis. Carnegie Institute of Technology, Carnegie Mellon University, 1998."},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"D. Lehmann","year":"1982","unstructured":"D. Lehmann and S. Shelah. Reasoning with time and chance. Information and Control 53, pp. 165\u2013198, 1982.","journal-title":"Information and Control"},{"key":"6_CR17","first-page":"327","volume-title":"Proceedings of the 26th IEEE Symposium on Foundations of Computer Science","author":"M. Vardi","year":"1985","unstructured":"M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of the 26th IEEE Symposium on Foundations of Computer Science. IEEE, New York, pp. 327\u2013338, 1985."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:07:41Z","timestamp":1736986061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"30 April 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}