Probabilistic model checking is an area within the formal methods community that supports the analysis of a variety of queries on Markov chains (MCs), Markov decision processes (MDPs), and variations of these formalisms. Since MCs and MDPs are popular in a variety of research communities, probabilistic model checking research and algorithms have been applied by researchers in reliability engineering, robotics, safety in AI, computational biology, and others.

We see two ingredients to this success story. First, the availability of the PRISM model checker, which has been developed over more than 20 years, has yielded a standard set of benchmarks, input language, and a de-facto standard to compare with. Second, a variety of modern tools have provided additional functionalities, and they de-facto adopted the PRISM interface. Consequently, users can easily run the tool that is most suited for their problem.

However, the success and broad applicability of these model checkers yields tools and interfaces that are increasingly diverging, based on the domains they specialize on. In addition, for queries that have been developed more recently, there is no de-facto standard and thus, tools do not necessarily agree on the interface. In this workshop, we aim to converge on some of these interfaces, in order to align the tools and make sure that they keep providing value for researchers in a variety of communities.

Creative Commons BY 4.0

Sebastian Junges and David Parker