💻 computer science

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

Este artigo apresenta o formato Unified Markov Binary (UMB), um padrão de arquivo binário eficiente e extensível projetado para superar barreiras de interoperabilidade em verificação de modelos probabilísticos ao fornecer uma representação unificada e de baixo nível de sistemas probabilísticos que já é adotada por ferramentas proeminentes e suportada por uma biblioteca Python abrangente.

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

Publicado 2026-06-17

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

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

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você esteja tentando construir uma máquina massiva e complexa (como um carro autônomo ou um sistema de previsão do tempo) usando diferentes equipes de engenheiros. Cada equipe fala uma linguagem ligeiramente diferente e usa seu próprio conjunto único de plantas.

A Equipe A escreve seus planos em uma carta longa e detalhada (código baseado em texto).
A Equipe B desenha seus planos em um quadro branco usando uma abreviação específica.
A Equipe C usa um modelo 3D digital.

O problema é que, quando a Equipe A quer enviar seu trabalho para a Equipe B, eles têm que reescrever toda a carta para a abreviação da Equipe B. Isso leva uma eternidade, cria enormes pilhas de papel e frequentemente leva a erros. No mundo da ciência da computação, isso é exatamente o que acontece com a Verificação de Modelos Probabilísticos. Essas são ferramentas usadas para provar matematicamente que sistemas (como softwares ou redes) se comportarão de forma segura e correta. Atualmente, essas ferramentas têm dificuldade em conversar entre si porque não compartilham um formato de arquivo "de baixo nível" comum.

Este artigo apresenta o UMB (Unified Markov Binary Format), uma nova solução para este colapso de comunicação.

A Ideia Central: A Caixa do "Tradutor Universal"

Pense no UMB não como uma linguagem, mas como um contêiner de transporte padronizado.

Antes do UMB, se você quisesse mover um modelo de uma ferramenta para outra, teria que desempacotar a máquina inteira, reconstruí-la do zero na linguagem da nova ferramenta e depois empacotá-la novamente. Era lento, bagunçado e ineficiente.

O UMB é um formato de arquivo binário (um código compacto legível por computador) que atua como um contêiner universal. Ele permite que diferentes ferramentas depositem um modelo no contêiner, enviem-no instantaneamente para outra ferramenta e que essa ferramenta o abra e o utilize imediatamente sem qualquer reconstrução.

Como Funciona: O "Bolo de Camadas" de Decisões

O artigo explica que o UMB é construído sobre uma ideia matemática inteligente chamada Sistema de Transição Anotado. Para entender isso, imagine um livro de "escolha sua própria aventura":

Estados (As Páginas): São as diferentes situações em que o sistema pode estar (ex: "O carro está se movendo", "O carro está parado").
Escolhas (As Decisões): Em algumas páginas, você tem que fazer uma escolha (ex: "Virar à esquerda" ou "Virar à direita"). Nos velhos tempos, diferentes ferramentas lidavam com essas escolhas de formas diferentes. O UMB trata todas elas como uma camada de "Escolha" padrão.
Ramos (Os Resultados): Uma vez feita uma escolha, existem resultados específicos (ex: "Virar à esquerda leva a um parque 50% das vezes, ou a uma rua 50% das vezes"). O UMB trata estes como "Ramos".

A Magia das "Anotações":
O que torna o UMB especial é que ele não apenas armazena o caminho; ele permite que você cole adesivos (anotações) em qualquer parte do livro.

Você pode colar um adesivo em uma página dizendo: "Este é um estado seguro".
Você pode colar um adesivo em uma escolha dizendo: "Esta é uma decisão humana".
Você pode colar um adesivo em um resultado dizendo: "Há uma probabilidade de 0,5 de chuva".

Como esses "adesivos" são separados da estrutura principal, o UMB pode lidar com todos os tipos de sistemas complexos — desde caminhadas aleatórias simples até jogos complexos com múltiplos jogadores — sem precisar de um novo formato de arquivo para cada um.

Por Que é Melhor? (Velocidade e Tamanho)

Os autores testaram o UMB contra formatos existentes (como os arquivos .tra e .drn usados por ferramentas populares). Eles descobriram três grandes benefícios:

É Rápido: Carregar um modelo de um arquivo UMB é como ler um código de barras. É significativamente mais rápido do que ler as longas cartas baseadas em texto (como a linguagem PRISM ou JANI) que as ferramentas costumam usar. O artigo mostra que o UMB pode carregar modelos em segundos que levam muito mais tempo com outros formatos.
É Compacto: Como utiliza código binário (0s e 1s) em vez de texto legível por humanos, os arquivos são menores. É como enviar um arquivo zip comprimido em vez de um documento de 500 páginas.
É Flexível: Se um novo tipo de sistema for inventado amanhã (um que ainda não foi visto antes), o UMB provavelmente poderá lidar com ele apenas adicionando novos "adesivos" (anotações) sem alterar o contêiner principal.

O Ecossistema: Um Esforço de Equipe

Isso não é apenas uma ideia teórica; já está sendo usado. O artigo destaca que ferramentas importantes como PRISM, Storm e mcsta já adotaram o UMB. Eles até construíram um "laboratório de testes" (chamado Observatório UMB) para garantir que, quando uma ferramenta salva um arquivo, outra ferramenta possa abri-lo perfeitamente.

Eles também criaram uma biblioteca Python (um conjunto de ferramentas de código pré-escrito) que torna fácil para os desenvolvedores ler, escrever e corrigir esses arquivos sem precisar ser especialistas nos detalhes de baixo nível.

Vitórias no Mundo Real (De acordo com o Artigo)

O artigo apresenta alguns exemplos de como isso ajuda pesquisadores agora:

O Melhor dos Dois Mundos: Uma ferramenta é ótima para construir modelos complexos, enquanto outra é ótima para resolvê-los rapidamente. Com o UMB, você pode construir o modelo na primeira ferramenta, salvá-lo no contêiner UMB e entregá-lo instantaneamente para a segunda ferramenta para resolvê-lo. Você obtém o melhor de ambos sem o tempo de espera.
Trabalho em Equipe: Agora você pode executar o mesmo modelo através de múltiplas ferramentas diferentes simultaneamente para ver qual delas fornece a melhor resposta, algo que era muito difícil antes porque as ferramentas não podiam compartilhar facilmente os dados brutos.
Preparação para o Futuro: Pesquisadores trabalhando em novos tipos de modelos experimentais podem usar o UMB para testar suas ideias imediatamente, sem esperar que um novo formato de arquivo seja inventado.

Resumo

Em suma, o UMB é um novo "contêiner de transporte universal" super eficiente para modelos probabilísticos. Ele substitui o processo lento e bagunçado de reescrever modelos entre diferentes ferramentas de software por um formato binário rápido, compacto e flexível. Ele permite que diferentes programas de computador conversem entre si de forma contínua, economizando tempo e permitindo que pesquisadores resolvam problemas mais difíceis mais rapidamente.

Resumo Técnico: UMB – Um Formato Binário de Markov Unificado para Verificação de Modelos Probabilísticos

Declaração do Problema

As ferramentas de verificação de modelos probabilísticos (PMC) amadureceram ao longo de décadas, suportando uma ampla gama de modelos, desde cadeias de Markov até jogos estocásticos. Embora linguagens de modelagem de alto nível (ex: PRISM, JANI) e formatos (ex: JANI baseado em JSON) facilitem o intercâmbio de descrições de alto nível, há uma carência crítica de mecanismos eficazes para o intercâmbio de representações de modelos de estado explícito de baixo nível.

Na prática, a interoperabilidade entre ferramentas é dificultada por duas abordagens ineficientes:

Recodificação: Converter modelos de estado explícito de volta para formatos textuais de alto nível (como a linguagem PRISM), o que acarreta um enorme overhead de armazenamento e custos de análise (parsing).
Formatos de Texto Específicos de Ferramentas: Utilizar formatos textuais ad-hoc (ex: .tra para PRISM, .drn para Storm) que são frequentemente limitados a tipos de modelos específicos, carecem de metadados e são ineficientes para gerar e analisar.

Essa fragmentação impede a construção contínua de toolchains que aproveitem as forças únicas de diferentes ferramentas de PMC.

Metodologia: O Formato Binário de Markov Unificado (UMB)

Os autores propõem o UMB, um formato de arquivo binário unificado, extensível e eficiente, projetado especificamente para sistemas probabilísticos de estado explícito. A metodologia baseia-se em três pilares:

1. Representação Matemática Unificada (Sistemas de Transição Anotados)

O formato é fundamentado em um modelo matemático formal chamado Sistema de Transição Anotado (ATS). Um ATS decompõe as transições em três entidades em camadas:

Estados ( $S$ ): Os estados do sistema.
Escolhas ( $C$ ): Escolhas não determinísticas disponíveis em um estado.
Ramos ( $B$ ): Resultados probabilísticos resultantes de uma escolha.

Esta estrutura é aumentada com anotações (mapeamentos de entidades para domínios como probabilidades, inteiros ou strings). Este formalismo é geral o suficiente para codificar naturalmente:

Cadeias de Markov (DTMCs, CTMCs)
Processos de Decisão de Markov (MDPs)
MDPs Parcialmente Observáveis (POMDPs)
Jogos Estocásticos (baseados em turnos e concorrentes)
Modelos com probabilidades de intervalo ou transições incertas
Sistemas de Transição Rotulados (LTS) não probabilísticos

2. Estrutura de Arquivo Binário

Um arquivo .umb é um arquivo tar (opcionalmente comprimido) contendo:

index.json: Um arquivo de metadados que define o tipo de modelo, estatísticas e um mapa das anotações incluídas.
Arquivos de Dados Binários: Três tipos específicos de arquivos binários usados para armazenar dados de forma eficiente:
- TO1: Arrays de tamanho fixo e indexados por inteiros (ex: para probabilidades ou IDs inteiros).
- SEQ: Listas de valores potencialmente de tamanho variável (ex: strings).
- CSR (Compressed Sparse Row): Índices para outros arquivos, espelhando esquemas padrão de armazenamento de matriz esparsa para permitir buscas em tempo constante de ramos por estado/escolha.

O formato suporta tipos primitivos (Booleanos, inteiros, doubles, racionais, intervalos) e permite anotações arbitrárias (ex: recompensas, proposições atômicas, valorações) anexadas a estados, escolhas ou ramos.

3. O Ecossistema UMB

Para garantir adoção e consistência, os autores desenvolveram um ecossistema de suporte:

Biblioteca umbi: Uma biblioteca Python que serve como implementação de referência para ler, criar, manipular e validar arquivos UMB. Ela fornece uma camada de abstração independente de formato (modelo de objeto ATS) para ocultar detalhes de layout binário.
Suporte de Ferramentas: Principais ferramentas de PMC (PRISM, Storm, mcsta do Modest Toolset, Paynt, Stamina, Stormvogel) integraram capacidades de importação/exportação de UMB.
Observatório UMB: Um ambiente de teste compartilhado com integração contínua para garantir o alinhamento entre as ferramentas e a biblioteca umbi, detectando inconsistências semânticas precocemente.

Principais Contribuições

Um Formato de Baixo Nível Universal: O UMB fornece o primeiro formato binário amplamente suportado e eficiente para o intercâmbio de modelos probabilísticos de estado explícito entre diferentes toolchains.
Extensibilidade: O design baseado em anotações permite que o formato suporte variantes de modelos "exóticas" ou futuras (ex: jogos estocásticos parcialmente observáveis, cadeias de Markov de tempo contínuo de intervalo) sem exigir uma nova especificação de formato de arquivo.
Eficiência: Ao utilizar primitivas binárias e esquemas de armazenamento esparso, o UMB evita o overhead de parsing de formatos textuais e o inchaço de recodificar modelos em linguagens de alto nível.
Ferramental Prático: O artigo entrega não apenas uma especificação, mas um ecossistema funcional incluindo uma biblioteca Python, bindings Java/C++ (via umbj) e um framework de integração contínua.

Resultados e Desempenho

Os autores avaliaram o UMB contra 36 modelos de benchmark padrão (DTMC, CTMC, MDP) comparando-o com formatos de alto nível (PRISM, JANI) e formatos de estado explícito existentes (DRN).

Velocidade de Carregamento: Carregar um arquivo UMB para obter uma representação de estado explícito é significativamente mais rápido do que gerar tais representações a partir de modelos PRISM/JANI ou carregar de arquivos DRN.
Velocidade de Exportação: Exportar para UMB é consistentemente e significativamente mais rápido do que exportar para DRN não comprimido. Embora a compressão torne ambos mais lentos, o UMB permanece mais rápido.
Tamanho de Arquivo: UMB e DRN (não comprimido) possuem tamanhos comparáveis. A compressão (GZip, XZ) reduz o tamanho de forma semelhante para ambos, sendo o XZ mais eficaz, porém mais lento.
Validação de Caso de Uso: O artigo demonstra toolchains práticas, como usar o mcsta para explorar espaços de estados complexos (com arrays dinâmicos) e exportar para o Storm para realizar verificação de modelos rápida. Em um estudo de caso (modelo de ataque Bitcoin), o Storm minimizou o espaço de estados e exportou para UMB em menos de 3 segundos, permitindo que o mcsta verificasse propriedades em 13 segundos — uma tarefa que expirou (timeout) quando tentada diretamente no Storm.

Significância e Alegações

O artigo afirma que o UMB aborda uma lacuna fundamental na comunidade de verificação de modelos probabilísticos: a incapacidade de trocar modelos de baixo nível de forma eficiente. Sua significância reside em:

Habilitar Novas Toolchains: Permite que pesquisadores e profissionais combinem as forças de modelagem de uma ferramenta (ex: suporte do mcsta para tipos de dados recursivos) com a velocidade de resolução de outra (ex: algoritmos do Storm).
Prototipagem Rápida: Pesquisadores podem desenvolver e testar algoritmos para novas classes de modelos (ex: modelos de intervalo) usando o umbi sem precisar implementar um parser completo e um explorador de espaço de estados do zero.
Padronização: Ao fornecer um padrão binário unificado, o UMB reduz o overhead de escrita e leitura de arquivos de modelo, facilitando scripts de geração e pipelines de avaliação mais sustentáveis.

Os autores observam que, embora o UMB atualmente exclua modelos com expressões simbólicas (ex: guardas de relógio em tempo real), o formato foi projetado para acomodar tais recursos em versões futuras via anotações baseadas em JSON. O trabalho representa uma mudança de um desenvolvimento de ferramentas isoladas para um ecossistema modular e interoperável.