UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)

arXiv (Cornell University)

Abstract

This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic systems. UMB addresses the problem that, while probabilistic model checking tools often support common high-level modelling languages, there is no effective mechanism for exchanging low-level model representations. In practice, textual, tool-specific formats are used, hampering interoperability and resulting in large overheads in writing and reading model files. UMB provides a clean, unified, and efficient solution, based on a general underlying mathematical model, and encoded using a small set of bit-level primitive data structures. The format has already been adopted by prominent tools and comes with a convenient Python library for reading, manipulating, creating, and validating models, plus infrastructure for cross-tool installation and continuous validation. We report on both the efficiency of the file format and the new practical use cases that it facilitates.

Authors 8

1. Roman Andriushchenko
2. Arnd Hartmanns

   University of Twente

   Affiliation as printed

   University of Twente , Enschede , The Netherlands

3. Joshua Jeppson
4. Sebastian Junges

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University , Nijmegen , The Netherlands

5. Tobias Meggendorfer

   Lancaster University

   Affiliation as printed

   Lancaster University Leipzig , Leipzig , Germany

6. David Parker
7. Tim Quatmann Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

8. Maximilian Weininger

   Ruhr University Bochum

   Affiliation as printed

   Ruhr-University Bochum , Bochum , Germany