Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Research Meeting 24134

Towards A Unified Interface For Modern Probabilistic Model Checking Tools

( Mar 24 – Mar 27, 2024 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:




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.

Copyright Sebastian Junges and David Parker