{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:25:50Z","timestamp":1777519550528,"version":"3.51.4"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661964","type":"print"},{"value":"9783319661971","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66197-1_22","type":"book-chapter","created":{"date-parts":[[2017,8,12]],"date-time":"2017-08-12T01:02:30Z","timestamp":1502499750000},"page":"349-366","source":"Crossref","is-referenced-by-count":4,"title":["Computing Conditional Probabilities: Implementation and Evaluation"],"prefix":"10.1007","author":[{"given":"Steffen","family":"M\u00e4rcker","sequence":"first","affiliation":[]},{"given":"Christel","family":"Baier","sequence":"additional","affiliation":[]},{"given":"Joachim","family":"Klein","sequence":"additional","affiliation":[]},{"given":"Sascha","family":"Kl\u00fcppelholz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"key":"22_CR1","unstructured":"Andr\u00e9s, M.: Quantitative analysis of information leakage in probabilistic and nondeterministic systems. Ph.D. thesis, UB Nijmegen (2011)"},{"issue":"28","key":"22_CR2","doi-asserted-by":"publisher","first-page":"3072","DOI":"10.1016\/j.tcs.2011.02.045","volume":"412","author":"ME Andr\u00e9s","year":"2011","unstructured":"Andr\u00e9s, M.E., Palamidessi, C., van Rossum, P., Sokolova, A.: Information hiding in probabilistic concurrent systems. Theor. Comput. Sci. 412(28), 3072\u20133089 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-78800-3_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"ME Andr\u00e9s","year":"2008","unstructured":"Andr\u00e9s, M.E., van Rossum, P.: Conditional probabilities over probabilistic and nondeterministic systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 157\u2013172. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_12"},{"issue":"3","key":"22_CR4","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"11","author":"J Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. J. Algorithms 11(3), 441\u2013461 (1990)","journal-title":"J. Algorithms"},{"issue":"1","key":"22_CR5","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model-checking continous-time Markov chains. ACM Trans. Comput. Logic 1(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Logic"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., K\u0159et\u00ednsk\u00fd, J., M\u00fcller, D., Parker, D., Strej\u010dek, J.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_31"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-06880-0_5","volume-title":"Horizons of the Mind. A Tribute to Prakash Panangaden","author":"C Baier","year":"2014","unstructured":"Baier, C., Dubslaff, C., Klein, J., Kl\u00fcppelholz, S., Wunderlich, S.: Probabilistic model checking for energy-utility analysis. In: Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden. LNCS, vol. 8464, pp. 96\u2013123. Springer, Cham (2014). doi: 10.1007\/978-3-319-06880-0_5"},{"issue":"6","key":"22_CR8","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"22_CR9","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-642-54862-8_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Baier","year":"2014","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., M\u00e4rcker, S.: Computing conditional probabilities in Markovian models efficiently. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 515\u2013530. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_43"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-662-54580-5_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., Wunderlich, S.: Maximizing the conditional expected reward for reaching the goal. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 269\u2013285. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54580-5_16"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-63387-9_8","volume-title":"Computer Aided Verification","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). doi: 10.1007\/978-3-319-63387-9_8"},{"issue":"3","key":"22_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.Z.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125\u2013155 (1998)","journal-title":"Distrib. Comput."},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-41528-4_3","volume-title":"Computer Aided Verification","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Espitau, T., Ferrer Fioriti, L.M., Hsu, J.: Synthesizing probabilistic invariants via Doop\u2019s decomposition. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 43\u201361. Springer, Cham (2016). doi: 10.1007\/978-3-319-41528-4_3"},{"key":"22_CR15","volume-title":"Object-Oriented Implementation of Numerical Methods: An Introduction with Java and Smalltalk","author":"DH Besset","year":"2000","unstructured":"Besset, D.H.: Object-Oriented Implementation of Numerical Methods: An Introduction with Java and Smalltalk. Morgan Kaufmann Publishers Inc., Burlington (2000)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499\u2013513. Springer, Heidelberg (1995). doi: 10.1007\/3-540-60692-0_70"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). doi: 10.1007\/978-3-319-41528-4_1"},{"issue":"4","key":"22_CR18","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. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., \u00c1brah\u00e1m, E.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_13"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). doi: 10.1007\/978-3-319-63390-9_31"},{"issue":"6","key":"22_CR21","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1145\/3812.3818","volume":"28","author":"S Even","year":"1985","unstructured":"Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Commun. ACM 28(6), 637\u2013647 (1985)","journal-title":"Commun. ACM"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53\u2013113. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21455-4_3"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-319-02444-8_36","volume-title":"Automated Technology for Verification and Analysis","author":"Y Gao","year":"2013","unstructured":"Gao, Y., Hahn, E.M., Zhan, N., Zhang, L.: CCMC: a conditional CSL model checker for continuous-time Markov chains. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 464\u2013468. Springer, Cham (2013). doi: 10.1007\/978-3-319-02444-8_36"},{"issue":"1\u20132","key":"22_CR24","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1016\/j.ipl.2012.09.009","volume":"113","author":"Y Gao","year":"2013","unstructured":"Gao, Y., Xu, M., Zhan, N., Zhang, L.: Model checking conditional CSL for continuous-time Markov chains. Inf. Process. Lett. 113(1\u20132), 44\u201350 (2013)","journal-title":"Inf. Process. Lett."},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002). doi: 10.1007\/3-540-36387-4"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-11439-2_10","volume-title":"Reachability Problems","author":"S Haddad","year":"2014","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 125\u2013137. Springer, Cham (2014). doi: 10.1007\/978-3-319-11439-2_10"},{"key":"22_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Cham (2014). doi: 10.1007\/978-3-319-06410-9_22"},{"key":"22_CR28","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 Comput. 6, 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"22_CR29","doi-asserted-by":"publisher","DOI":"10.1002\/0470841923","volume-title":"Performance of Computer Communication Systems: A Model-Based Approach","author":"BR Haverkort","year":"1998","unstructured":"Haverkort, B.R.: Performance of Computer Communication Systems: A Model-Based Approach. Wiley, Hoboken (1998)"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-38697-8_21","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"M Heiner","year":"2013","unstructured":"Heiner, M., Rohr, C., Schwarick, M.: MARCIE \u2013 model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389\u2013399. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38697-8_21"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Types for Proofs and Programs","author":"L Helmink","year":"1994","unstructured":"Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127\u2013165. Springer, Heidelberg (1994). doi: 10.1007\/3-540-58085-9_75"},{"key":"22_CR32","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.entcs.2015.12.013","volume":"319","author":"Nils Jansen","year":"2015","unstructured":"Jansen, N., Kaminski, B.L., Katoen, J., Olmedo, F., Gretz, F., McIver, A.: Conditioning in probabilistic programming. In: Mathematical Foundations of Programming Semantics (MFPS), ENTCS, vol. 319, pp. 199\u2013216 (2015)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"6","key":"22_CR33","first-page":"1329","volume":"8","author":"M Ji","year":"2013","unstructured":"Ji, M., Wu, D., Chen, Z.: Verification method of conditional probability based on automaton. J. Netw. 8(6), 1329\u20131335 (2013)","journal-title":"J. Netw."},{"issue":"2","key":"22_CR34","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J-P Katoen","year":"2011","unstructured":"Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"22_CR35","volume-title":"Modeling and Analysis of Stochastic Systems","author":"VG Kulkarni","year":"1995","unstructured":"Kulkarni, V.G.: Modeling and Analysis of Stochastic Systems. Chapman & Hall, Boca Raton (1995)"},{"key":"22_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM? In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 194\u2013206. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44585-4_17"},{"key":"22_CR37","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.) PAPM-PROBMIV 2002. LNCS, vol. 2399, pp. 169\u2013187. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45605-8_11"},{"issue":"2","key":"22_CR38","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"MZ Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. Int. J. Softw. Tools Technol. Transf. (STTT) 6(2), 128\u2013142 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"22_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"MZ Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_47"},{"key":"22_CR40","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: 9th International Conference on Quantitative Evaluation of SysTems (QEST), pp. 203\u2013204. IEEE Computer Society (2012)","DOI":"10.1109\/QEST.2012.14"},{"key":"22_CR41","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-319-66197-1_22","volume-title":"Software Engineering and Formal Methods","author":"Steffen M\u00e4rcker","year":"2017","unstructured":"M\u00e4rcker, S., Baier, C., Klein, J., Kl\u00fcppelholz, S.: Computing conditional probabilities: implementation and evaluation (extended version) (2017). http:\/\/wwwtcs.inf.tu-dresden.de\/ALGI\/PUB\/SEFM17\/"},{"key":"22_CR42","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-972-5","volume-title":"Programming Finite Elements in Java$$^{\\rm TM}$$","author":"GP Nikishkov","year":"2010","unstructured":"Nikishkov, G.P.: Programming Finite Elements in Java$$^{\\rm TM}$$, 1st edn. Springer, London (2010)","edition":"1"},{"key":"22_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-540-40981-6_9","volume-title":"Formal Aspects of Security","author":"G Norman","year":"2003","unstructured":"Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. In: Abdallah, A.E., Ryan, P., Schneider, S. (eds.) FASec 2002. LNCS, vol. 2629, pp. 81\u201396. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-40981-6_9"},{"key":"22_CR44","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L., Processes, M.D.: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (1994)"},{"issue":"1","key":"22_CR45","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"MK Reiter","year":"1998","unstructured":"Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. ACM Trans. Inf. Syst. Secur. (TISSEC) 1(1), 66\u201392 (1998)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"key":"22_CR46","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: 26th IEEE Symposium on Foundations of Computer Science (FOCS), pp. 327\u2013338. IEEE Computer Society (1985)","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T03:21:46Z","timestamp":1659324106000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}