I Would If I Could: Reasoning about Dynamics of Actions in Multi-Agent Systems

1. Declaração do Problema

Lógicas estratégicas padrão para Sistemas Multi-Agente (SMA), como a Lógica Temporal de Tempo Alternado (ATL) e sua extensão epistêmica (ATEL), modelam as capacidades dos agentes com base em modelos fixos. Embora essas lógicas permitam que os agentes reajam dinamicamente a estados ou históricos, elas assumem um conjunto estático de ações disponíveis para cada agente.

Em cenários realistas de longo prazo (por exemplo, robôs autônomos assistindo uma pessoa idosa), as capacidades de um agente não são estáticas. Os agentes podem precisar:

• Adquirir novas ações (por exemplo, um robô aprendendo a abrir uma gaveta emperrada).
• Perder ações (por exemplo, um robô sendo proibido de entrar em uma área quente).
• Raciocinar sobre essas mudanças e suas consequências epistêmicas (por exemplo, saber que lhes falta uma ação específica e que adquiri-la lhes permitiria alcançar um objetivo).

As lógicas existentes não conseguem modelar naturalmente a concessão e revogação dinâmica de ações nem as atualizações epistêmicas resultantes de tais mudanças. Este artigo aborda a lacuna no raciocínio sobre a evolução das habilidades dos agentes e seu conhecimento dessas habilidades dentro de um quadro lógico formal.

2. Metodologia

Os autores introduzem dois novos quadros lógicos que estendem as lógicas estratégicas existentes com operadores de atualização dinâmica de ações.

A. ATL com Ações Dinâmicas (ATL-D)

• Base: Estende a Lógica Temporal de Tempo Alternado (ATL) sobre Estruturas de Jogos Concorrentes (CGS).
• Nova Sintaxe:
  • has(a, α): Fórmula atômica afirmando que o agente $a$ possui atualmente a ação $\alpha$.
  • [π]+φ: Após aplicar uma atualização de concessão $\pi$, $\phi$ vale.
  • [π]−φ: Após aplicar uma atualização de revogação $\pi$, $\phi$ vale.
  • Operador de Atualização $\pi$: Definido como uma lista de atualizações condicionais φ : α → A. Isso especifica que, em todos os estados que satisfazem a condição $\phi$, a ação $\alpha$ é concedida a (ou removida de) a coalizão $A$.
• Semântica:
  • Atualizações modificam a função de disponibilidade $d(a, v)$ da CGS.
  • Restrição de Razoabilidade: Ao revogar ações, o sistema garante que um agente nunca fique com zero ações disponíveis. Se uma revogação deixasse um agente sem movimentos, a revogação é bloqueada para aquele agente.
  • A lógica avalia fórmulas sobre o modelo atualizado resultante da aplicação do operador de atualização.

B. ATL Epistêmico com Ações Dinâmicas (ATEL-D)

• Base: Estende ATL-D para lidar com Informação Imperfeita (iCGS), onde os agentes não conseguem distinguir entre certos estados.
• Nova Sintaxe:
  • Kaφ: O agente $a$ sabe $\phi$.
  • Atualização Estendida: [φ : α → A, B]+ (e -).
    • $A$: O conjunto de agentes que recebem a mudança de ação.
    • $B$: O conjunto de agentes informados sobre a pré-condição $\phi$ da atualização.
• Semântica:
  • Atualização de Ação: Similar ao ATL-D, ações são adicionadas/removidas com base em $\phi$.
  • Atualização Epistêmica: Agentes no conjunto $B$ (e $A$, por pressuposto padrão) tornam-se conscientes do valor de verdade de $\phi$. Isso é modelado "cortando" a relação de indistinguibilidade ($\sim$) entre estados onde $\phi$ é verdadeiro e estados onde $\phi$ é falso.
  • Isso permite modelar cenários que vão desde atualizações semi-privadas (apenas o ator sabe) até atualizações públicas (todos sabem a condição).

3. Contribuições Principais

1. Quadros Formais: A introdução de ATL-D e ATEL-D, que são as primeiras lógicas a modelar explicitamente o processo dinâmico de concessão/revogação de ações e as mudanças epistêmicas resultantes em SMA.
2. Análise de Expressividade:
   • Provou-se que ATL-D é estritamente mais expressiva que a ATL padrão.
   • Demonstrou-se que o fragmento com apenas atualizações de concessão (ATL-D+) e o fragmento com apenas atualizações de revogação (ATL-D−) são incomparáveis; nenhum pode expressar tudo o que o outro pode.
   • Mostrou-se como ATL-D− captura intuições-chave de Sistemas Normativos (leis sociais e restrições comportamentais), preenchendo a lacuna entre lógica estratégica e raciocínio normativo.
3. Resultados de Complexidade:
   • Verificação de Modelo:
     • ATL-D é P-completa (mesma complexidade que a ATL padrão).
     • ATEL-D é $\Delta^P_2$-completa (mesma complexidade que ATEL com informação imperfeita).
   • Existência de Atualização Limitada: O problema de determinar se existe uma sequência limitada de atualizações para satisfazer um objetivo é NP-completo.
4. Soluções Algorítmicas:
   • Fornecido um algoritmo global de verificação de modelo para ATL-D (Algoritmo 1) que atualiza iterativamente a função de disponibilidade do modelo.
   • Fornecido um algoritmo sofisticado de verificação de modelo para ATEL-D (Algoritmo 2) que rastreia atualizações por meio de uma lista rotulada de subfórmulas e modifica simultaneamente as relações de observação e a disponibilidade de ações.

4. Resultados Principais

• Teorema 1 & 2 (Expressividade):
  • $ATL \prec ATL\text{-}D^+$ e $ATL\text{-}D^+ \not\preceq ATL\text{-}D^-$.
  • $ATL \prec ATL\text{-}D^-$ e $ATL\text{-}D^- \not\preceq ATL\text{-}D^+$.
  • Isso confirma que a capacidade de adicionar ações e a capacidade de remover ações são capacidades lógicas distintas.
• Teorema 3 & 4 (Sistemas Normativos):
  • ATL-D− pode simular "leis sociais" (restrições comportamentais) e "leis sociais atômicas" encontradas na literatura de SMA normativos, provando sua utilidade para raciocínio regulatório.
• Teorema 5 (Verificação de Modelo ATL-D):
  • O problema está em P. O algoritmo executa em tempo polinomial em relação ao tamanho do modelo e da fórmula, pois requer apenas um número polinomial de atualizações de modelo.
• Teorema 6 (Existência de Atualização Limitada):
  • O problema é NP-completo. Uma redução de 3SAT é usada para provar a dureza, mostrando que encontrar uma sequência de atualizações para satisfazer um objetivo é computacionalmente difícil.
• Teorema 7 (Verificação de Modelo ATEL-D):
  • O problema é $\Delta^P_2$-completo. A complexidade permanece na mesma classe que a ATEL padrão, apesar da dimensão dinâmica adicionada, porque o número de palpites de estratégia permanece polinomial.

5. Significado e Aplicações

• Aprendizado Proativo: A lógica permite que os agentes raciocinem sobre o que precisam aprender para alcançar um objetivo. Por exemplo, um robô pode deduzir: "Se eu adquirir a ação $X$, posso alcançar o objetivo", e solicitar proativamente essa capacidade.
• Segurança e Regulação: O quadro permite a verificação formal de protocolos de segurança onde ações são desabilitadas dinamicamente (por exemplo, impedindo um robô de entrar em uma zona perigosa) e verificando se essas restrições não tornam inadvertidamente o sistema bloqueado (via a restrição de "razoabilidade").
• Dinâmicas Epistêmicas: Ao capturar como as atualizações de ações afetam o conhecimento, a lógica apoia o design de sistemas onde os agentes devem coordenar com base em conhecimento compartilhado ou privado de suas capacidades em mudança (por exemplo, em jogos de tabuleiro ou equipes de múltiplos robôs).
• Ponte Teórica: O trabalho conecta o raciocínio estratégico (ATL) com o raciocínio normativo (leis sociais) e a lógica epistêmica dinâmica (DEL), oferecendo uma abordagem unificada para modelar o ciclo de vida das capacidades dos agentes.

Em resumo, este artigo fornece uma base teórica robusta para o raciocínio sobre agentes adaptativos cujas capacidades e conhecimento evoluem dinamicamente, oferecendo tanto as ferramentas lógicas para descrever esses sistemas quanto as garantias computacionais para verificá-los.