UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)
For researchers and practitioners in probabilistic model checking, UMB provides a standardized, efficient low-level model representation that enables cross-tool interoperability and new use cases.
This paper introduces the Unified Markov Binary (UMB) format, an efficient and extensible file format for probabilistic model checking that improves interoperability and reduces file I/O overhead. The format achieves up to 10x smaller file sizes and faster read/write times compared to text-based formats.
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.