Dear colleagues, (apology for multiple copies)
Let us advertise the next ERATO MMSD project colloquium talk by Sean Sedwards. Please find the title and abstract of the talk below. You are all cordially invited. Remote attendance is also welcome (Polycom is available in the room). Please let us know beforehand if you would like to join remotely.
Sincerely, Akira Yoshimizu Technical Assistant at ERATO MMSD project
---------- https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpX... https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpXDeA/edit
Fri 28 April 2017, 15:15–17:00 NII meeting room 2010 https://www.nii.ac.jp/en/about/access/ https://www.nii.ac.jp/en/about/access/ Sean Sedwards (ERATO MMSD), Rare Event Simulation for Statistical Model Checking 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.