A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version)

Título: Uma Framework para Bisimulação Coalgebraica Sensível a Recompensas

Autores: Pedro H. Azevedo de Amorim, Mayuko Kori e Koko Muroya.

1. Problema e Motivação

A área de sistemas de transição com dados quantitativos (como custos, recompensas ou probabilidades) tem exigido extensões das noções clássicas de bisimulação. Enquanto a bisimulação tradicional lida bem com propriedades qualitativas (ex: "dois estados aceitam a mesma linguagem"), ela falha em capturar diferenças quantitativas, como distâncias entre estados ou acumulação de recompensas.

O problema central abordado é a falta de uma abstração comum e unificada que:

1. Integre noções de bisimulação sensíveis a recompensas (onde estados podem ser similares, mas com uma diferença de recompensa acumulada limitada).
2. Relacione formalmente essas noções graduadas (que rastreiam limites de recompensa) com as noções não graduadas (abstratas).
3. Forneça uma fundamentação coalgebraica e fibrada que explique quando uma bisimulação graduada pode ser vista como um refinamento de uma não graduada.

Exemplos existentes, como amortised bisimulations (para sistemas com custos) e approximate bisimulations (para processos de Markov), tratam casos específicos, mas carecem de uma teoria unificada que explique a relação estrutural entre o "gradado" e o "não gradado".

2. Metodologia

Os autores utilizam uma abordagem baseada em Teoria das Categorias, especificamente combinando Teoria Coalgebraica e Fibrações (Fibrations).

• Abordagem Coalgebraica: Os sistemas são modelados como coalgebras $c: S \to FS$ de um endofunctor $F$.
• Fibrações (Fibrations): Seguem o trabalho de Hermida e Jacobs, utilizando fibrações $p: E \to C$ para modelar relações (ou estruturas quantitativas) sobre os objetos do sistema. O foco é em CLat$\sqcap$-fibrations, onde as fibras são reticulados completos.
• Gluing Categorical (Colagem Categorical): A técnica central proposta é a aplicação de "gluing" (colagem) de fibrações, uma técnica da lógica categórica. Eles constroem uma fibração colada (glued fibration) que combina duas noções de relações:
  • Uma categoria de relações não graduadas ($E$).
  • Uma categoria de relações graduadas ($E_g$), onde os índices representam tolerâncias (ex: diferença de recompensa).
• Doutrina de Colagem Adjoint (Adjoint Gluing Doctrine): Eles axiomatizam a interação entre os dois mundos através de uma adjunção fibrada $\exists_g \dashv \Delta$, onde:
  • $\Delta$ embute relações não graduadas em graduadas (como relações constantes).
  • $\exists_g$ (união sobre as graduações) mapeia relações graduadas para não graduadas.
• Objetos Coma: Utilizam a construção de objetos coma para unir as duas noções de coalgebra em um único modelo coerente, permitindo provar teoremas de correção (soundness) de forma universal.

3. Contribuições Principais

1. Framework Unificado: Propõem uma axiomatização coalgebraica e fibrada que generaliza bisimulações sensíveis a recompensas. O framework trata a bisimulação graduada e a não graduada como análises diferentes de um mesmo sistema, conectadas por uma estrutura categórica rigorosa.
2. Construção de "Glued Coalgebras": Introduzem uma maneira canônica de combinar estruturas coalgebraicas graduadas e não graduadas usando colagem categórica. Isso permite definir um modelo onde ambas as noções coexistem e interagem de forma coerente.
3. Teorema de Correção Abstrato (Soundness): Provaram que, sob a doutrina de colagem adjoint, a união de uma bisimulação graduada é sempre uma bisimulação não graduada válida. Formalmente, se $A$ é uma simulação graduada, então $\exists_g A$ é uma simulação não graduada.
4. Caracterização de Coalgebras Finais: Demonstraram como calcular a coalgebra final no modelo colado, mostrando que ela é composta pelas coalgebras finais das estruturas graduada e não graduada individuais.
5. Generalização de Exemplos: O framework é suficientemente flexível para englobar diversos casos de estudo existentes e novos:
   • Autômatos Determinísticos com Recompensas (DAwR) e suas simulações.
   • Bisimulações amortizadas em Sistemas de Transição Rotulados (LTS).
   • Simulações em Processos de Decisão de Markov (MDPs) com recompensas.
   • Bisimulações aproximadas em Processos de Markov Rotulados (LMPs), conectando abordagens baseadas em pseudométricas (Lévy-Prokhorov) com abordagens baseadas em relações.

4. Resultados Chave

• Teorema 3 (Soundness): Estabelece a relação fundamental de que a "colagem" preserva a propriedade de simulação: a projeção de uma simulação graduada para o mundo não graduado resulta em uma simulação válida.
• Teorema 4: Mostra que as coalgebras coladas formam um par de seção-retração entre as categorias de coalgebras graduadas e não graduadas, validando a estrutura da doutrina.
• Teorema 6: Caracteriza a coalgebra final no modelo colado, provando que a estrutura final é a combinação das estruturas finais dos componentes graduado e não graduado.
• Aplicação em LMPs (Teorema 7 e 8): Para Processos de Markov Rotulados, o framework prova que bisimulações baseadas em pseudométricas (distância $\epsilon$) e bisimulações baseadas em relações graduadas são equivalentes em casos finitos, unificando duas linhas de pesquisa distintas.

5. Significado e Impacto

Este trabalho é significativo por fornecer a primeira fundamentação categórica unificada para bisimulações sensíveis a recompensas.

• Unificação Teórica: Resolve a incerteza sobre como as noções graduadas se relacionam com as não graduadas, mostrando que a primeira é um refinamento estrutural da segunda através de uma construção de colagem.
• Versatilidade: Ao abstrair os detalhes específicos de recompensas ou métricas para a estrutura de fibrações e adjunções, o framework permite a aplicação de resultados gerais (como teoremas de correção e existência de coalgebras finais) a uma vasta gama de sistemas, desde autômatos determinísticos até processos estocásticos.
• Novas Perspectivas: A introdução de "simulações em autômatos determinísticos com recompensas" (DAwR) como um novo conceito e a conexão explícita entre métricas e relações em processos de Markov abrem novas portas para a verificação formal de sistemas quantitativos.

Em resumo, o artigo oferece uma "linguagem comum" baseada em teoria das categorias para raciocinar sobre similaridade em sistemas onde a precisão quantitativa (recompensas, custos, distâncias) é tão importante quanto a estrutura qualitativa do comportamento.