💻 computer science

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

Dit artikel introduceert het Unified Markov Binary (UMB) formaat, een efficiënte en uitbreidbare binaire bestandsstandaard die is ontworpen om interoperabiliteitsbarrières in probabilistisch model checken te overwinnen door een verenigde, laag-niveau representatie van probabilistische systemen te bieden die al is overgenomen door prominente tools en wordt ondersteund door een uitgebreide Python-bibliotheek.

Oorspronkelijke auteurs: Roman Andriushchenko, Arnd Hartmanns, Joshua Jeppson, Sebastian Junges, Tobias Meggendorfer, David Parker, Tim Quatmann, Maximilian Weininger

Gepubliceerd 2026-06-17

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Roman Andriushchenko, Arnd Hartmanns, Joshua Jeppson, Sebastian Junges, Tobias Meggendorfer, David Parker, Tim Quatmann, Maximilian Weininger

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een enorme, complexe machine probeert te bouwen (zoals een zelfrijdende auto of een weersvoorspellingssysteem) met behulp van verschillende teams van ingenieurs. Elk team spreekt een iets andere taal en gebruikt zijn eigen unieke set blauwdrukken.

Team A schrijft hun plannen in een lange, gedetailleerde brief (tekstgebaseerde code).
Team B tekent hun plannen op een whiteboard met een specifieke shorthand.
Team C gebruikt een digitaal 3D-model.

Het probleem is dat wanneer Team A hun werk naar Team B wil sturen, ze de hele brief moeten herschrijven naar de shorthand van Team B. Dit duurt eeuwen, creëert enorme stapels papier en leidt vaak tot fouten. In de wereld van de informatica is dit precies wat er gebeurt met Probabilistisch Model Checken. Dit zijn tools die worden gebruikt om systemen (zoals software of netwerken) wiskundig te bewijzen dat ze veilig en correct functioneren. Momenteel worstelen deze tools om met elkaar te communiceren omdat ze geen gemeenschappelijk "laag-niveau" bestandsformaat delen.

Dit artikel introduceert UMB (Unified Markov Binary Format), een nieuwe oplossing voor dit communicatieprobleem.

Het Kernidee: De "Universele Vertaler"-doos

Denk aan UMB niet als een taal, maar als een gestandaardiseerde zeecontainer.

Vóór UMB, als je een model van het ene naar het andere instrument wilde verplaatsen, moest je de hele machine uitpakken, hem in de taal van het nieuwe instrument vanaf nul weer opbouwen, en hem dan weer inpakken. Het was traag, slordig en inefficiënt.

UMB is een binair bestandsformaat (een compacte, door de computer leesbare code) dat fungeert als een universele container. Het stelt verschillende tools in staat om een model in de container te plaatsen, het direct naar een andere tool te verschepen, en die tool vervolgens de container te laten openen en het direct te laten gebruiken zonder het opnieuw op te bouwen.

Hoe het werkt: De "Gelaagde Taart" van Beslissingen

Het artikel legt uit dat UMB is gebouwd op een slim wiskundig idee dat een Annotated Transition System wordt genoemd. Om dit te begrijpen, stel je een "kies je eigen avontuur"-boek voor:

Toestanden (De Pagina's): Dit zijn de verschillende situaties waarin het systeem zich kan bevinden (bijv. "De auto rijdt," of "De auto staat stil").
Keuzes (De Beslissingen): Op sommige pagina's moet je een keuze maken (bijv. "Linksaf slaan" of "Rechtsaf slaan"). In de oude dagen gingen verschillende tools anders om met deze keuzes. UMB behandelt ze allemaal als een standaard "Keuze"-laag.
Vertakkingen (De Uitkomsten): Zodra een keuze is gemaakt, zijn er specifieke uitkomsten (bijv. "Linksaf slaan leidt 50% van de tijd tot een park, of 50% van de tijd tot een straat"). UMB behandelt dit als "Vertakkingen".

De Magie van "Annotaties":
Wat UMB bijzonder maakt, is dat het niet alleen het pad opslaat; het stelt je ook in staat om stickers (annotaties) op elk deel van het boek te plakken.

Je kunt een sticker op een pagina plakken met: "Dit is een veilige toestand."
Je kunt een sticker op een keuze plakken met: "Dit is een menselijke beslissing."
Je kunt een sticker op een uitkomst plakken met: "Er is een kans van 0,5 op regen."

Omdat deze "stickers" gescheiden zijn van de hoofdstructuur, kan UMB alle soorten complexe systemen aan—van eenvoudige willekeurige wandelingen tot complexe spellen met meerdere spelers—zonder dat er voor elk type een nieuw bestandsformaat nodig is.

Waarom is het beter? (Snelheid en Grootte)

De auteurs hebben UMB getest tegen bestaande formaten (zoals de .tra en .drn bestanden die door populaire tools worden gebruikt). Ze vonden drie belangrijke voordelen:

Het is Snel: Een model laden vanuit een UMB-bestand is alsof je een streepjescode leest. Het is aanzienlijk sneller dan het lezen van de lange, tekstgebaseerde brieven (zoals de PRISM-taal of JANI) die tools gewoonlijk gebruiken. Het artikel laat zien dat UMB modellen in seconden kan laden die met andere formaten veel langer duren.
Het is Compact: Omdat het binaire code (enen en nullen) gebruikt in plaats van menselijke tekst, zijn de bestanden kleiner. Het is alsof je een gecomprimeerd zip-bestand stuurt in plaats van een document van 500 pagina's.
Het is Flexibel: Als er morgen een nieuw type systeem wordt uitgevonden (één die nog niet eerder is gezien), kan UMB dit waarschijnlijk aan, simpelweg door nieuwe "stickers" (annotaties) toe te voegen zonder de kerncontainer te veranderen.

Het Ecosysteem: Een Teaminspanning

Dit is niet alleen een theoretisch idee; het wordt al gebruikt. Het artikel benadrukt dat grote tools zoals PRISM, Storm en mcsta al UMB hebben overgenomen. Ze hebben zelfs een "testlab" (de UMB Observatory genoemd) gebouwd om te garanderen dat wanneer de ene tool een bestand opslaat, een andere tool het perfect kan openen.

Ze hebben ook een Python-bibliotheek (een set vooraf geschreven codetools) gemaakt die het voor ontwikkelaars gemakkelijk maakt om deze bestanden te lezen, te schrijven en te repareren zonder dat ze expert hoeven te zijn in de details op laag niveau.

Winsten in de echte wereld (Volgens het artikel)

Het artikel geeft een paar voorbeelden van hoe dit onderzoekers nu helpt:

Het Beste van Beide Werelden: De ene tool is erg goed in het bouwen van complexe modellen, terwijl een andere tool erg goed is in het oplossen ervan met hoge snelheid. Met UMB kun je het model in de eerste tool bouwen, het opslaan in de UMB-container, en het direct aan de tweede tool overhandigen om het op te lossen. Je krijgt het beste van beide zonder de wachttijd.
Teamwerk: Je kunt nu hetzelfde model door verschillende tools tegelijkertijd laten lopen om te zien welke de beste uitkomst geeft, iets wat voorheen erg moeilijk was omdat de tools de ruwe data niet gemakkelijk konden delen.
Toekomstbestendigheid: Onderzoekers die werken aan gloednieuwe, experimentele soorten modellen kunnen UMB gebruiken om hun ideeën onmiddellijk te testen, zonder te hoeven wachten tot er een nieuw bestandsformaat is uitgevonden.

Samenvatting

Kortom, UMB is een nieuwe, super-efficiënte "universele zeecontainer" voor probabilistische modellen. Het vervangt het trage, slordige proces van het herschrijven van modellen tussen verschillende softwaretools door een snel, compact en flexibel binair formaat. Het stelt verschillende computerprogramma's in staat om naadloos met elkaar te communiceren, wat tijd bespaart en onderzoekers in staat stelt om hardere problemen sneller op te lossen.

Technische Samenvatting: UMB – Een Uniform Binair Markov-formaat voor Probabilistisch Modelverificatie

Probleemstelling

Tools voor probabilistische modelverificatie (PMC) zijn in decennia tijd volwassen geworden en ondersteunen een breed scala aan modellen, van Markov-ketens tot stochastische spellen. Hoewel hoogwaardige modellerings talen (bijv. PRISM, JANI) en formaten (bijv. op JSON gebaseerde JANI) de uitwisseling van hoogwaardige beschrijvingen vergemakkelijken, is er een kritiek gebrek aan effectieve mechanismen voor het uitwisselen van laagniveau, expliciete-toestand modelrepresentaties.

In de praktijk wordt interoperabiliteit tussen tools gehinderd door twee inefficiënte benaderingen:

Re-encoding: Het converteren van expliciete-toestand modellen terug naar hoogwaardige tekstuele formaten (zoals de PRISM-taal), wat enorme opslagoverhead en parseerkosten met zich meebrengt.
Tool-specifieke Tekstformaten: Het gebruik van ad-hoc, tekstuele formaten (bijv. .tra voor PRISM, .drn voor Storm) die vaak beperkt zijn tot specifieke modeltypen, geen metadata bevatten en inefficiënt zijn om te genereren en te parsen.

Deze fragmentatie verhindert de naadloze constructie van toolchains die de unieke sterktes van verschillende PMC-tools kunnen benutten.

Methodologie: Het Unified Markov Binary (UMB) Formaat

De auteurs stellen UMB voor, een uniform, uitbreidbaar en efficiënt binair bestandsformaat dat specifelt is ontworpen voor expliciete-toestand probabilistische systemen. De methodologie rust op drie pijlers:

1. Uniforme Wiskundige Representatie (Geannoteerde Transitiesystemen)

Het formaat is geworteld in een formeel wiskundig model genaamd het Annotated Transition System (ATS). Een ATS deelt transities op in drie gelaagde entiteiten:

States ( $S$ ): De systeemtoestanden.
Choices ( $C$ ): Nondeterministische keuzes beschikbaar in een toestand.
Branches ( $B$ ): Probabilistische uitkomsten voortvloeiend uit een keuze.

Deze structuur wordt uitgebreid met annotaties (mapping van entiteiten naar domeinen zoals waarschijnlijkheden, integers of strings). Deze formalisering is algemeen genoeg om natuurlijk het volgende te coderen:

Markov-ketens (DTMCs, CTMCs)
Markov Decision Processes (MDPs)
Partially Observable MDPs (POMDPs)
Stochastische spellen (turn-based en concurrent)
Modellen met interval-waarschijnlijkheden of onzekere transities
Niet-probabilistische Labelled Transition Systems (LTS)

2. Binaire Bestandsstructuur

Een .umb bestand is een (optioneel gecomprimeerd) tar-archief bevattende:

index.json: Een metadata-bestand dat het modeltype, statistieken en een kaart van de geïncludeerde annotaties definieert.
Binaire Databestanden: Drie specifieke typen binaire bestanden die worden gebruikt om gegevens efficiënt op te slaan:
- TO1: Vastgrootte, integer-geïndexeerde arrays (bijv. voor waarschijnlijkheden of integer ID's).
- SEQ: Lijsten van potentieel variabele grootte waarden (bijv. strings).
- CSR (Compressed Sparse Row): Indices naar andere bestanden, die de standaard sparse matrix opslagregelingen spiegelen om constant-tijd lookups van branches per state/choice mogelijk te maken.

Het formaat ondersteunt primitieve typen (Booleans, integers, doubles, rationals, intervallen) en staat arbitraire annotaties toe (bijv. beloningen, atomaire proposities, waarderingen) gekoppeld aan states, choices of branches.

3. Het UMB Ecosysteem

Om adoptie en consistentie te waarborgen, hebben de auteurs een ondersteunend ecosysteem ontwikkeld:

umbi Library: Een Python-bibliotheek die dient als een referentie-implementatie voor het lezen, creëren, manipuleren en valideren van UMB-bestanden. Het biedt een formaat-agnostische abstractielaag (ATS object model) om de details van de binaire lay-out te verbergen.
Tool Support: Belangrijke PMC-tools (PRISM, Storm, de Modest Toolset van mcsta, Paynt, Stamina, Stormvogel) hebben UMB import/export mogelijkheden geïntegreerd.
UMB Observatory: Een gedeelde testomgeving met continue integratie om de uitlijning tussen tools en de umbi bibliotheek te waarborgen en semantische inconsistenties vroegtijdig te detecteren.

Belangrijkste Bijdragen

Een Universeel Laagniveau Formaat: UMB biedt het eerste breed ondersteunde, efficiënte binaire formaat voor het uitwisselen van expliciete-toestand probabilistische modellen over verschillende toolchains heen.
Uitbreidbaarheid: Het annotatie-gebaseerde ontwerp stelt het formaat in staat om "exotische" of toekomstige modelvarianten (bijv. gedeeltelijk observeerbare stochastische spellen of interval continuous-time Markov chains) te ondersteunen zonder dat daarvoor een nieuw bestandsformaat-specificatie nodig is.
Efficiëntie: Door gebruik te maken van binaire primitieven en sparse storage schema's, vermijdt UMB de parsing-overhead van tekstuele formaten en de opgeblazen omvang van het re-encoderen van modellen naar hoogwaardige talen.
Praktische Tooling: Het paper levert niet alleen een specificatie, maar ook een werkend ecosysteem inclusief een Python-bibliotheek, Java/C++ bindings (via umbj) en een continuous integration framework.

Resultaten en Prestaties

De auteurs hebben UMB geëvalueerd tegenover 36 standaard benchmark-modellen (DTMC, CTMC, MDP) en vergeleken met hoogwaardige formaten (PRISM, JANI) en bestaande expliciete-toestand formaten (DRN).

Laadsnelheid: Het laden van een UMB-bestand om een expliciete-toestand representatie te verkrijgen is significant sneller dan het genereren van dergelijke representaties vanuit PRISM/JANI modellen of het laden vanaf DRN-bestanden.
Export Snelheid: Exporteren naar UMB is consequent en significant sneller dan exporteren naar ongecomprimeerde DRN. Hoewel compressie beide processen vertraagt, blijft UMB sneller.
Bestandsgrootte: UMB en DRN (ongecomprimeerd) hebben vergelijkbare groottes. Compressie (GZip, XZ) vermindert de grootte vergelijkbaar voor beide, waarbij XZ effectiever is maar langzamer.
Validatie van Use Cases: Het paper demonstreert praktische toolchains, zoals het gebruik van mcsta om complexe toestandsruimten te verkennen (met dynamische arrays) en het exporteren naar UMB voor Storm om snelle modelverificatie uit te voeren. In één casestudy (Bitcoin attack model) minimaliseerde Storm de toestandsruimte en exporteerde deze naar UMB in minder dan 3 seconden, waardoor mcsta eigenschappen kon verifiëren in 13 seconden—een taak die bij een directe poging in Storm een timeout veroorzaakte.

Betekenis en Claims

Het paper claimt dat UMB een fundamentele kloof in de probabilistische modelverificatie gemeenschap aanpakt: het onvermogen om laagniveau modellen efficiënt uit te wisselen. De betekenis ligt in:

Het Mogelijk Maken van Nieuwe Toolchains: Het stelt onderzoekers en praktijkgebruikers in staat om de modelleringssterktes van de ene tool (bijv. mcsta's ondersteuning voor recursieve datatypen) te combineren met de oplossnelheid van een andere (bijv. de algoritmen van Storm).
Snel Prototyping: Onderzoekers kunnen algoritmen voor nieuwe modelklassen (bijv. interval modellen) ontwikkelen en testen met umbi zonder dat zij een volledige parser en state-space explorer vanaf nul moeten implementeren.
Standaardisatie: Door een verenigde, binaire standaard te bieden, vermindert UMB de overhead van het schrijven en lezen van modelbestanden, wat het genereren van modellen en evaluatie-pipelines onderhoudbaarder maakt.

De auteurs merken op dat UMB momenteel modellen met symbolische expressies (bijv. real-time klok guards) uitsluit, maar dat het formaat is ontworpen om dergelijke functies in toekomstige versies te accommoderen via JSON-gebaseerde annotaties. Het werk vertegenwoordigt een verschuiving van geïsoleerde toolontwikkeling naar een modulaire, interoperabele ecosystem.