Prism Importance Sampling Extension

Using Importance Sampling to Enlarge the Bullseye

Introduction

Hello, I am Tom Prouty and I am a Senior ECE Undergraduate Student in the Honors Research Fellowship Program. I have been working as a part of the USU contingent of the Fluent Verification Group. As a member of this group, My focus is on the development of CTMC (Continuous Time Markov Chain) models for verification.

I have also assisted in the development of possible methods of verifying these types of models to make them faster and more efficient. This project is about making the bullseye bigger, so data errors are found even more quickly.

Special Thanks:
Dr. Chris Winstead
UG Research Mentor

Project

• The background of this project was to develop and implement an Importance Sampling method that improved the efficiency of Stochastic Simulation for CTMC’s
• The solution to the problem of inefficient SSA by finding the probability of extremely unlikely events in CTMC models
• The objective was to use Importance Sampling to solve this verification problem. The result is less resources needed to explore and evaluate models like Biological Circuits and Reaction Networks.

System

Methods

• This project used PRISM model checker. Since its functions use Java code, the Importance Sampling method under investigation is written in Java as well.
• The implementation method chosen uses the “modulo” scheme developed by my Fellowship Research Professor, Dr. Winstead
• This scheme works by taking advantage of how exponential variables are time independent and how their probability distribution can be “compressed” by use of the modulo

Conclusion

• The results of the Modulo Importance Sampling Scheme showed that the amount of time needed for SSA to reach the variance bounds was marginally reduced.
• This anticipated result proves that Importance Sampling methods can be effective in CTMC verification . This was not intended to be the silver bullet for solving rare event simulation.

Honors Capstone

• A key part of the design and implementation process for digital models, is how a developer will test the effectiveness of their own design in comparison to other tools that are currently in use by the broader community.
• My Honors Capstone conducts a model comparison using the results of my Senior Project. This evaluates SSA and altered methods of SSA , by analyzing and comparing the model checker tools PRISM, Alt PRISM, STORM, and STAMINA.
• All three of these tools are in active development and use methods of SSA to analyze properties of Markov Chain Models.

Findings:

More work in this area will improve the speed of error detection.

This chart shows a comparison of my model and existing models with times narrowing down to hit the bullseye faster.

Special Thanks:
Dr. Todd Moon
Honors Capstone Advisor