Generating Local Shields for Decentralised Partially Observable Markov Decision Processes

Título: Geração de Escudos Locais para Processos de Decisão de Markov Parcialmente Observáveis Descentralizados (Dec-POMDP)

Autores: Haoran Yang e Nobuko Yoshida (Universidade de Oxford)
Publicação: 17th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2026)

---

1. O Problema

Sistemas multiagente operando sob observação parcial (Dec-POMDP) enfrentam desafios críticos de segurança. O problema central reside no fato de que a ação escolhida localmente por um agente individual não determina, de forma geral, a ação conjunta resultante. Isso pode levar a colisões, deadlocks ou livelocks, especialmente em ambientes onde:

• Não há comunicação entre os agentes.
• Os agentes possuem apenas informações locais (histórico de observações), sem acesso ao estado global do sistema.
• Técnicas existentes de "shielding" (proteção/escudo) falham porque assumem acesso a um estado global centralizado ou utilizam filtros locais sem memória que ignoram o histórico de interações.

A dificuldade é garantir que cada agente selecione uma ação concreta que seja garantidamente segura, dado que sua visão local é apenas um fragmento do estado global.

2. Metodologia

Os autores propõem uma abordagem baseada em uma Álgebra de Processos de Escudo com escolha guardada e recursão, compilada em máquinas de Mealy locais. O pipeline de implementação segue três etapas principais:

A. Álgebra de Processos de Escudo

Definem uma linguagem formal para especificar comportamentos globais seguros. A gramática inclui:

• idle / fail: Terminação bem-sucedida ou falha.
• µX.P: Recursão (assumida guardada).
• Sh.P: Continuação que afirma que o próximo estado deve pertencer a um conjunto de estados seguros globais ($Sh \subseteq S$).
• P1 ∥g P2: Escolha guardada, onde o processo comporta-se como $P1$ se o estado atual $s \in g$, e como $P2$ caso contrário.

B. Pipeline de Compilação

O processo de transformação da especificação para escudos executáveis ocorre em três fases:

1. Autômato de Processo: Tradução da especificação da álgebra de processos para um autômato determinístico que interpreta o comportamento seguro global.
2. Máquina de Mealy Global: Construção de um filtro de ações conjuntas seguras.
   • Entrada: Estado global do Dec-POMDP.
   • Saída: Um conjunto de ações conjuntas seguras.
   • Utiliza uma decomposição determinística ($Dec$) para mapear ações conjuntas em conjuntos de ações locais para cada agente, garantindo que a escolha independente de cada agente resulte em uma ação conjunta válida.
3. Máquinas de Mealy Locais (Projeção): Projeção da máquina global para cada agente individual.
   • Entrada: Observação parcial do agente ($\Omega_i$).
   • Estados: Subconjuntos de "crença" (belief-style) dos estados da máquina global que são consistentes com a observação atual do agente.
   • Saída: O conjunto de ações seguras para aquele agente específico, calculado pela interseção das saídas globais correspondentes aos estados de crença. Se o conjunto de crença indicar falha total, o escudo retorna $\perp$ (falha de escudo).

C. Implementação e Análise

• Linguagem: Implementado em Rust.
• Verificação: Integração com o PRISM (Probabilistic Symbolic Model Checker) para calcular probabilidades de segurança (melhor e pior caso) independentemente da política dos agentes.

3. Estudo de Caso: Multi-Agent Path Finding (MAPF)

O método foi validado em um problema de roteamento de agentes em grades (MAPF), onde o objetivo é mover agentes de posições iniciais para alvos sem colidir (conflitos de vértice).

• Cenário "Agentes Cegos" (Blind Agents): Um caso extremo onde o raio de observação é zero ($R=0$). Métodos baseados apenas em observações locais falham aqui, mas a álgebra de processos consegue especificar sequências seguras de estados globais que garantem a chegada aos alvos.
• Comparação de Políticas de Escudo:
  • $P_1$ (Conservador): Mantém o sistema em estados seguros, mas frequentemente força os agentes a permanecerem parados, limitando a exploração.
  • $P_2$ (Menos Conservador): Minimiza a perda de ações devido a interseções de ramos, permitindo o maior conjunto possível de próximos estados seguros.

4. Resultados

Os experimentos foram realizados em grades de tamanhos variados (3x3, 4x4, 5x5) com 2 e 3 agentes, comparando políticas aleatórias e políticas aprendidas via Q-learning.

• Eliminação de Colisões: Em todas as configurações testadas, os escudos eliminaram completamente os conflitos de vértice (colisões), enquanto a política aleatória não protegida apresentou taxas de colisão altas (ex: 72.7% em um cenário 4x4).
• Desempenho vs. Segurança:
  • A política $P_2$ superou consistentemente a $P_1$ e a baseline não protegida na métrica de "chegada" (agents reaching targets).
  • $P_2$ permitiu que os agentes explorassem mais estados e executassem mais ações, mantendo a segurança.
  • A política $P_1$ foi excessivamente conservadora, suprimindo ações seguras e reduzindo drasticamente a taxa de sucesso.
• Impacto da Observação: O aumento do raio de observação ($R$) melhorou significativamente o desempenho de $P_2$, reduzindo as falhas de escudo (quando o escudo não consegue propor nenhuma ação segura).
• Aprendizado por Reforço: Agentes treinados com Q-learning e protegidos por $P_2$ alcançaram as melhores taxas de sucesso com zero colisões. Escudos aplicados post-hoc também garantiram segurança zero, mas a integração durante o treinamento com $P_2$ foi superior.

5. Contribuições Principais

1. Álgebra de Processos de Escudo: Uma nova formalização com recursão e escolha guardada para especificar comportamentos seguros em ambientes descentralizados e sem comunicação.
2. Pipeline de Compilação: Um método completo que transforma especificações de processos em autômatos e, subsequentemente, em máquinas de Mealy locais executáveis, lidando com a complexidade da observação parcial através de estados de crença.
3. Implementação e Verificação: Uma ferramenta em Rust integrada ao PRISM, permitindo a análise de probabilidades de segurança sem fixar uma política específica de agentes.

6. Significado e Conclusão

Este trabalho aborda uma lacuna crítica na segurança de sistemas multiagente descentralizados. Ao demonstrar que é possível gerar escudos locais rigorosos sem acesso a um estado global compartilhado, o artigo oferece uma solução prática para garantir segurança em cenários de comunicação restrita.

A principal descoberta é que a expressividade da especificação do processo (como em $P_2$) é crucial: escudos excessivamente conservadores podem impedir a execução da tarefa, enquanto uma abordagem baseada em álgebra de processos permite um equilíbrio fino entre segurança estrita (zero colisões) e desempenho da tarefa (alta taxa de chegada). O trabalho abre caminho para futuras integrações com métodos de decomposição baseados em SAT e escudos aprendidos, reduzindo o esforço de especificação manual.