International Symposium On Leveraging Applications of Formal Methods, Verification and Validation • Crete, Greece
Time: Sunday, 3.11
Room: Room 1
Authors:
Abstract: Robust autonomy and interaction of robots with their environment, even in rare or new situations, is an ultimate goal of robotics research. We settle on Statistical Model Checking (SMC) for the benefit of robustness of robot deliberation and base our implementation on STORM, one of the most performant and comprehensive open-source model checkers, so far lacking an SMC extension. The SMC extension introduced in this paper offers various statistical methods, from which the user can choose to find the best trade-off between accuracy of the result and runtime. We demonstrate the effciency of our SMC implementation by comparing it to other state-of-the-art SMC tools on well-established benchmarks and on a robotics-related example. The results indicate that our implementation, which will be continuously extended in the future to improve support for robotics use cases, is performant enough to bridge the gap between robotic systems and model checking in industry.
Paper: Download