{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:00:29Z","timestamp":1725890429814},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540851134"},{"type":"electronic","value":"9783540851141"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85114-1_7","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T23:22:48Z","timestamp":1218583368000},"page":"60-76","source":"Crossref","is-referenced-by-count":5,"title":["Generating Compact MTBDD-Representations from Probmela Specifications"],"prefix":"10.1007","author":[{"given":"Frank","family":"Ciesinski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christel","family":"Baier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"Gr\u00f6\u00dfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"7_CR1","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design: An International Journal\u00a015(1), 7\u201348 (1999)","journal-title":"Formal Methods in System Design: An International Journal"},{"key":"7_CR2","unstructured":"Baier, C., Ciesinski, F., Gr\u00f6\u00dfer, M.: Probmela: a modeling language for communicating probabilistic systems. In: Proceeding MEMOCODE (2004)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/3-540-45139-0_11","volume-title":"Model Checking Software","author":"M. Baldamus","year":"2001","unstructured":"Baldamus, M., Schr\u00f6der-Babo, J.: p2b: a translation utility for linking promela and symbolic model checking (tool paper). In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 183\u2013191. Springer, Heidelberg (2001)"},{"key":"7_CR4","first-page":"131","volume-title":"Proc. QEST","author":"F. Ciesinski","year":"2007","unstructured":"Ciesinski, F., Baier, C.: LiQuor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. QEST, pp. 131\u2013132. IEEE CS Press, Los Alamitos (2007)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C., Groesser, M., Klein, J.: Reduction techniques for model checking markov decision processes (submitted for publication, 2008)","DOI":"10.1109\/QEST.2008.45"},{"key":"7_CR6","unstructured":"Clarke, E., Fujita, M., McGeer, P., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. In: International Workshop on Logic Synthesis, Tahoe City (1993)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/11944836_29","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"M. Gr\u00f6\u00dfer","year":"2006","unstructured":"Gr\u00f6\u00dfer, M., Norman, G., Baier, C., Ciesinski, F., Kwiatkoswka, M., Parker, D.: On reduction criteria for probabilistic reward models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol.\u00a04337, pp. 309\u2013320. Springer, Heidelberg (2006)"},{"issue":"1-2","key":"7_CR8","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/S1567-8326(02)00066-8","volume":"56","author":"H. Hermanns","year":"2003","unstructured":"Hermanns, H., Kwiatkowska, M., Norman, G., Parker, D., Siegle, M.: On the use of MTBDDs for performability analysis and verification of stochastic systems. Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems\u00a056(1-2), 23\u201367 (2003)","journal-title":"Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems"},{"key":"7_CR9","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.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"7_CR10","volume-title":"The Spin Model Checker, Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/123186.123225","volume-title":"DAC 1990: Proceedings of the 27th ACM\/IEEE conference on Design automation","author":"S.i. Minato","year":"1990","unstructured":"Minato, S.i., Ishiura, N., Yajima, S.: Shared binary decision diagram with attributed edges for efficient boolean function manipulation. In: DAC 1990: Proceedings of the 27th ACM\/IEEE conference on Design automation, pp. 52\u201357. ACM Press, New York (1990)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Information and Computation\u00a088(1) (1990)","DOI":"10.1016\/0890-5401(90)90004-2"},{"key":"#cr-split#-7_CR13.1","doi-asserted-by":"crossref","unstructured":"Lehmann, D., Rabin, M.O.: On the advantage of free choice: A symmetric and fully distributed solution to the Dining Philosophers problem (extended abstract). In: Proc. Eighth Ann. ACM Symp. on Principles of Programming Languages, pp. 133???138 (1981);","DOI":"10.1145\/567532.567547"},{"key":"#cr-split#-7_CR13.2","unstructured":"A classic paper in the area of randomized distributed algorithms. They show there is no deterministic, deadlock-free, truly distributed and symmetric solution to the Dining Philosophers problem, and describe a simple probabilistic alternative."},{"key":"7_CR14","first-page":"6","volume-title":"ICCAD 1988: Digest of technical papers","author":"S. Malik","year":"1988","unstructured":"Malik, S., Wang, A.R., Brayton, R.K.: Logic verification using binary decision diagrams in a logic synthesis environment. In: ICCAD 1988: Digest of technical papers, pp. 6\u20139. IEEE Press, Los Alamitos (1988)"},{"key":"7_CR15","unstructured":"McMillan, K.L.: The SMV system, symbolic model checking - an approach. Technical Report CMU-CS-92-131, Carnegie Mellon University (1992)"},{"key":"7_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-58940-9","volume-title":"Algorithms and Data Structures in VLSI Design: OBDD-Foundations and Applications","author":"C. Meinel","year":"1998","unstructured":"Meinel, C., Theobald, T.: Algorithms and Data Structures in VLSI Design: OBDD-Foundations and Applications. Springer, Heidelberg (1998)"},{"key":"7_CR17","unstructured":"Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham (2002)"},{"key":"7_CR18","unstructured":"PRISM web site, http:\/\/www.prismmodelchecker.org"},{"key":"7_CR19","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M.L. Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York (1994)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic Decision Diagrams and Their Applications. In: IEEE \/ACM International Conference on CAD, Santa Clara, California, November 1993, pp. 188\u2013191. ACM\/IEEE, IEEE Computer Society Press (1993)","DOI":"10.1109\/ICCAD.1993.580054"},{"issue":"2","key":"7_CR21","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 (1995)","journal-title":"Nordic Journal of Computing"},{"key":"7_CR22","unstructured":"Beaudenon, V., Encrenaz, E., Taktak, S.: Data decision diagrams for promela systems analysis. In: Software Tools and Technology Transfert (accepted for publication, 2008)"},{"key":"7_CR23","series-title":"Monographs on Discrete Mathematics and Applications","volume-title":"Monographs on Discrete Mathematics and Applications","author":"I. Wegener","year":"2000","unstructured":"Wegener, I.: Branching Programs and Binary Decision Diagrams: Theory and Applications. In: Monographs on Discrete Mathematics and Applications. Monographs on Discrete Mathematics and Applications. SIAM, Philadelphia (2000)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85114-1_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:22:12Z","timestamp":1606166532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85114-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851134","9783540851141"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85114-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}