Statistical model checking: Challenges and perspectives

Statistical model checking (SMC) is a powerful and widely used approach that consists in estimating the probability for a system to satisfy a temporal property. This is done by monitoring a finite number of executions of the system, and then extrapolating the result using statistics. The answer is correct up to some confidence that can be parameterized by the user. It is known that SMC mitigates the state-space explosion problem and allows us to handle requirements that cannot be expressed in classical temporal logics. The approach has been implemented in several toolsets, and successfully applied in a wide range of diverse areas such as systems biology, robotic, or automotive. The objectives of this special issue are (1) to survey existing results on SMC, (2) to propose SMC algorithms for a larger class of systems, and (3) to show the applicability of SMC to new emerging applications.