A Statistical Model Checker for Situation Calculus Based Multi-Agent Models

In this paper we introduce a new approach for multi-agent simulation and statistical model checking that combines the well-established situation calculus with a first order version of bounded linear time logic (BLTL). This creates a fully integrated solution for specifying system behavior and requirements within the same logical framework. We realized the approach in an extensible tool that combines the benefits of constraint logic programming with the versatility of Python and its ecosystem. First experiments show that the approach is applicable to a wide range of problems and that altogether a more flexible modeling-verification workflow is achieved than in most existing solutions.