<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">Dear colleagues, (apology for multiple copies)</div><div class=""><br class=""></div><div class="">Let us advertise the next ERATO MMSD project colloquium talk by Sean Sedwards.</div><div class="">Please find the title and abstract of the talk below. You are all cordially invited.</div><div class="">Remote attendance is also welcome (Polycom is available in the room). Please let us know beforehand if you would like to join remotely.</div><div class=""><br class=""></div><div class="">Sincerely,</div><div class="">Akira Yoshimizu</div><div class="">Technical Assistant at ERATO MMSD project</div><div class=""><br class=""></div><div class="">----------</div><div class=""><a href="https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpXDeA/edit" class="">https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpXDeA/edit</a> </div><div class=""><br class=""></div><div class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-family: Arial; font-size: 14pt; font-weight: 700; background-color: rgb(255, 255, 255);" class="">Fri 28 April 2017, 15:15–17:00</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 8pt; font-family: Arial; background-color: rgb(255, 255, 255); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline;" class="">NII meeting room 2010</span><span style="font-size: 8pt; font-family: Arial; background-color: rgb(255, 255, 255); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline;" class=""><br class="kix-line-break"></span><a href="https://www.nii.ac.jp/en/about/access/" style="text-decoration:none;" class=""><span style="font-size: 8pt; font-family: Arial; color: rgb(17, 85, 204); background-color: rgb(255, 255, 255); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; text-decoration: underline; vertical-align: baseline;" class="">https://www.nii.ac.jp/en/about/access/</span></a><span style="font-size: 8pt; font-family: Arial; background-color: rgb(255, 255, 255); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline;" class=""> </span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; background-color: rgb(255, 255, 255); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline;" class="">Sean Sedwards (ERATO MMSD), </span><span style="font-size: 11pt; font-family: Arial; background-color: rgb(255, 255, 255); font-weight: 700; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline;" class="">Rare Event Simulation for Statistical Model Checking</span></div><span style="font-size: 9pt; font-family: Arial; color: rgb(102, 102, 102); background-color: rgb(255, 255, 255); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline;" class="">Statistical model checking (SMC) avoids the intractable number of states associated with numerical model checking by estimating the probability of a property from a number of execution traces (simulations). Rare events nevertheless pose an important challenge to SMC because interesting properties, such as bugs and optima, are often very rare and occur infrequently in simulations. A key objective for SMC is thus to reduce the number and length of simulations necessary to produce an estimate with a given level of statistical confidence. In this talk I will describe two variance reduction approaches that address this problem: importance sampling and importance splitting. Importance sampling weights the probabilities of a system to make a rare property occur more frequently in simulations, then compensates the results by the weights. Importance splitting decomposes a rare property into the product of sub-properties that are less rare and easier to simulate. I will outline the challenges of using these techniques in SMC and highlight some practical solutions, including the recent successful application of importance sampling to stochastic timed automata.</span></div><div class=""><br class=""></div></body></html>