{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T06:48:14Z","timestamp":1764053294358,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314230"},{"type":"electronic","value":"9783642314247"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_26","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"327-342","source":"Crossref","is-referenced-by-count":27,"title":["Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking"],"prefix":"10.1007","author":[{"given":"Cyrille","family":"Jegourel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sean","family":"Sedwards","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-28756-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Barbot","year":"2012","unstructured":"Barbot, B., Haddad, S., Picaronny, C.: Coupling and Importance Sampling for Statistical Model Checking. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 331\u2013346. Springer, Heidelberg (2012)"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-13464-7_4","volume-title":"Formal Techniques for Distributed Systems","author":"A. Basu","year":"2010","unstructured":"Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical Abstraction and Model-Checking of Large Heterogeneous Systems. In: Hatcliff, J., Zucca, E. (eds.) FMOODS 2010. LNCS, vol.\u00a06117, pp. 32\u201346. Springer, Heidelberg (2010)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J. Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Uppaal \u2014 a Tool Suite for Automatic Verification of Real-Time Systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 232\u2013243. Springer, Heidelberg (1996)"},{"issue":"4","key":"26_CR4","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1214\/aoms\/1177729330","volume":"23","author":"H. Chernoff","year":"1952","unstructured":"Chernoff, H.: A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the sum of Observations. Ann. Math. Statist.\u00a023(4), 493\u2013507 (1952)","journal-title":"Ann. Math. Statist."},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24372-1_1","volume-title":"Automated Technology for Verification and Analysis","author":"E.M. Clarke","year":"2011","unstructured":"Clarke, E.M., Zuliani, P.: Statistical Model Checking for Cyber-Physical Systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 1\u201312. Springer, Heidelberg (2011)"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"De Boer, P.-T., Nicola, V.F., Rubinstein, R.Y.: Adaptive importance sampling simulation of queueing networks. In: Winter Simulation Conference, vol.\u00a01, pp. 646\u2013655 (2000)","DOI":"10.1109\/WSC.2000.899776"},{"key":"26_CR7","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM\u00a018, 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"D.T. Gillespie","year":"1977","unstructured":"Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry\u00a081, 2340\u20132361 (1977)","journal-title":"Journal of Physical Chemistry"},{"key":"26_CR9","unstructured":"Godefroid, P., Levin, M., Molnar, D.: Automated whitebox fuzz testing. In: NDSS (2008)"},{"key":"26_CR10","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1145\/203091.203094","volume":"5","author":"P. Heidelberger","year":"1995","unstructured":"Heidelberger, P.: Fast simulation of rare events in queueing and reliability models. ACM Trans. Model. Comput. Simul.\u00a05, 43\u201385 (1995)","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate Probabilistic Model Checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"issue":"301","key":"26_CR12","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W. Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability Inequalities for Sums of Bounded Random Variables. Journal of the American Statistical Association\u00a058(301), 13\u201330 (1963)","journal-title":"Journal of the American Statistical Association"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/978-3-642-28756-5_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: A Platform for High Performance Statistical Model Checking \u2013 PLASMA. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 498\u2013503. Springer, Heidelberg (2012)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-03845-7_15","volume-title":"Computational Methods in Systems Biology","author":"S.K. Jha","year":"2009","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian Approach to Model Checking Biological Systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol.\u00a05688, pp. 218\u2013234. Springer, Heidelberg (2009)"},{"key":"26_CR15","unstructured":"Kahn, H.: Stochastic (Monte Carlo) Attenuation Analysis. Technical Report P-88, Rand Corporation (July 1949)"},{"key":"26_CR16","unstructured":"Kullback, S.: Information Theory and Statistics. Dover (1968)"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"issue":"247","key":"26_CR18","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1080\/01621459.1949.10483310","volume":"44","author":"N. Metropolis","year":"1949","unstructured":"Metropolis, N., Ulam, S.: The Monte Carlo Method. Journal of the American Statistical Association\u00a044(247), 335\u2013341 (1949)","journal-title":"Journal of the American Statistical Association"},{"key":"26_CR19","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/s10479-005-5727-9","volume":"134","author":"A. Ridder","year":"2005","unstructured":"Ridder, A.: Importance sampling simulations of markovian reliability systems using cross-entropy. Annals of Operations Research\u00a0134, 119\u2013136 (2005)","journal-title":"Annals of Operations Research"},{"issue":"1","key":"26_CR20","doi-asserted-by":"publisher","first-page":"1571","DOI":"10.1016\/j.procs.2010.04.176","volume":"1","author":"A. Ridder","year":"2010","unstructured":"Ridder, A.: Asymptotic optimality of the cross-entropy method for markov chain problems. Procedia Computer Science\u00a01(1), 1571\u20131578 (2010)","journal-title":"Procedia Computer Science"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Rubino, G., Tuffin, B. (eds.): Rare Event Simulation using Monte Carlo Methods. Wiley (2009)","DOI":"10.1002\/9780470745403"},{"key":"26_CR22","unstructured":"Rubinstein, R.: The Cross-Entropy Method for Combinatorial and Continuous Optimization 1, 127\u2013190 (1999)"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: QEST, pp. 251\u2013252. IEEE (September 2005)","DOI":"10.1109\/QEST.2005.42"},{"issue":"3","key":"26_CR24","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1287\/mnsc.40.3.333","volume":"40","author":"P. Shahabuddin","year":"1994","unstructured":"Shahabuddin, P.: Importance Sampling for the Simulation of Highly Reliable Markovian Systems. Management Science\u00a040(3), 333\u2013352 (1994)","journal-title":"Management Science"},{"issue":"1","key":"26_CR25","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/TIT.1980.1056144","volume":"26","author":"J. Shore","year":"1980","unstructured":"Shore, J., Johnson, R.: Axiomatic derivation of the principle of maximum entropy and the principle of minimum cross-entropy. IEEE Transactions on Information Theory\u00a026(1), 26\u201337 (1980)","journal-title":"IEEE Transactions on Information Theory"},{"key":"26_CR26","unstructured":"The PRISM website, http:\/\/www.prismmodelchecker.org"},{"key":"26_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 223\u2013235. Springer, Heidelberg (2002)"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2005","unstructured":"Younes, H.L.S.: Ymer: A Statistical Model Checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 429\u2013433. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T09:31:52Z","timestamp":1743586312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}