Hardware implementation of BLTL property checkers for acceleration of statistical model checking

Statistical model checking is a method to analyze systems where values of variables may have some uncertainty or variations. It can be used to check whether some desired properties are satisfied with specified probability under such uncertainty. In statistical model checking, the system needs to be repeatedly simulated and checked for properties represented in Bounded Linear Temporal Logic (BLTL). The property checking takes a long time if a property includes many variables and/or if the analysis is performed for long sequences. In this paper, we propose a hardware implementation of BLTL property checkers to accelerate the property checking process in statistical model checking. Through the experimental results on Tsunami simulation with variations of earthquake parameters, we show that the total execution time of statistical model checking can be shorten by more than 30 times compared to a software implementation, by implementing our proposed BLTL property checkers on FPGA.