The Model Checking Problem for Distributed Knowing How is $\Delta^p_2$-Complete

Resumo Técnico: O Problema de Verificação de Modelo para o Saber-Como Distribuído é $\Delta^p_2$-Completo

Definição do Problema
Este artigo investiga a complexidade computacional do problema de verificação de modelo para a lógica do Saber-Como Distribuído (DKH - Distributed Knowing How). O DKH é uma lógica modal projetada para formalizar as capacidades dos agentes em alcançar objetivos por meio de ações adequadas. Ele generaliza dois frameworks existentes:

1. Frameworks baseados em planejamento (ex: [5, 6]), que tratam o "saber-como" como a existência de um plano de múltiplos passos que executa, termina e garante um objetivo.
2. Frameworks baseados em coalizões (ex: [3, 4]), que tratam o "saber-como" de um grupo como a existência de uma ação conjunta de um único passo que assegura um objetivo.

A lógica DKH introduz uma modalidade $Kh_G \phi$, significando que um grupo de agentes $G$ possui uma estratégia para garantir que $\phi$ seja verdadeiro. A questão central abordada é: Dado um modelo finito $M$, um estado $s$ e uma fórmula $\phi$, a relação $M, s \models \phi$ é verdadeira?

Metodologia
Os autores estabelecem a complexidade deste problema provando tanto um limite superior quanto um limite inferior, utilizando um algoritmo específico de verificação de modelo e uma redução de um problema conhecido de alta complexidade.

1. Limite Superior ($\Delta^p_2$):
   Os autores propõem um procedimento de verificação de modelo, CHECKERDKH, que avalia fórmulas de baixo para cima (bottom-up).

   • Casos Booleanos e $K_G$: São tratados via operações de conjuntos em tempo polinomial sobre estados e classes de equivalência.
   • O caso $Kh_G$: Este é o componente não trivial. Em vez de construir explicitamente o conjunto de ações distribuídas potencialmente exponencial $A^*_G$, o algoritmo computa o conjunto de satisfação da fórmula interna $\psi$ e, então, realiza uma construção de ponto fixo mônotona sobre o conjunto quociente $S/\sim_G$ (o conjunto de classes de equivalência sob a relação de indistinguibilidade distribuída).
   • Uso de Oráculo: Em cada iteração do ponto fixo, o algoritmo verifica se uma ação distribuída "vencedora" existe para uma classe de equivalência específica. Esta verificação (HASWINDISTRIBUTION) é realizada por um procedimento não determinístico que supõe uma tupla de ações atômicas e verifica sua validade e executabilidade. Esta etapa de verificação é mostrada como pertencente a NP.
   • Como a iteração do ponto fixo envolve um número polinomial de passos, cada um chamando um oráculo NP, o procedimento geral reside em $\Delta^p_2$ (problemas decidíveis em tempo polinomial com polimamente muitas chamadas a um oráculo NP).

2. Limite Inferior ($\Delta^p_2$-Dureza):
   Para provar a dureza, os autores reduzem o problema SNSAT (um problema conhecido como $\Delta^p_2$-completo) ao problema de verificação de modelo DKH.

   • Instância SNSAT: Uma instância consiste em uma sequência de variáveis booleanas $x_1, \dots, x_n$ onde cada $x_i$ é definida por uma equivalência $x_i \iff \exists Z_i F_i(x_1, \dots, x_{i-1}, Z_i)$. O objetivo é determinar o valor de verdade de $x_n$.
   • Construção da Redução: Os autores constroem um modelo DKH $M$ e uma fórmula $\Psi_n$ tal que $M, s_n \models \Psi_n$ se, e somente se, $x_n$ é verdadeiro na instância SNSAT.
     • O modelo contém "estados de entrada" $s_i$ para cada camada e "estados ruins" $b^i_r$ representando cláusulas não satisfeitas.
     • Agentes são atribuídos a variáveis locais e ocorrências de variáveis anteriores.
     • A fórmula $\Psi_k$ é definida recursivamente: $\Psi_1 = Kh_{G_1} q$ e $\Psi_k = Kh_{G_k} (q \lor (r_k \land \neg \Psi_{k-1}))$.
     • A lógica garante que um grupo $G_k$ pode "saber como" alcançar o estado de sucesso $q$ (ou um estado de verificação negativa $n^k_{x_j}$) apenas se a fórmula booleana correspondente $F_k$ for satisfatível dadas as atribuições de verdade das variáveis anteriores determinadas pelas camadas inferiores.
   • A redução baseia-se no fato de que as ações distribuídas nesta construção específica podem ser achatadas em tuplas de ações singulares, permitindo que a estratégia codifique diretamente as atribuições de verdade.

Contribuições Principais e Resultados

• Classificação de Complexidade: O artigo prova que o problema de verificação de modelo para o Saber-Como Distribuído é $\Delta^p_2$-completo. Isso fornece um limite de complexidade estrito para o problema.
• Inovação Algorítmica: Os autores introduzem um algoritmo de verificação de modelo que evita a construção explícita do conjunto de ações distribuídas $A^*_G$. Em vez disso, utiliza um algoritmo de ponto fixo sobre o conjunto quociente $S/\sim_G$, delegando a existência de ações distribuídas válidas a um oráculo NP.
• Prova de Dureza: A redução de SNSAT demonstra que a interação entre os quantificadores aninhados na lógica (via definição recursiva de $Kh_G$) e a natureza distribuída das ações captura todo o poder de $\Delta^p_2$.

Significado
O artigo afirma que estabelecer este limite estrito é a principal contribuição. Ao caracterizar a complexidade como $\Delta^p_2$-completa, o trabalho delineia os limites computacionais de verificar capacidades distribuídas em sistemas multiagentes dentro deste framework lógico. Os autores observam que um próximo passo natural, baseado neste resultado, é investigar o problema de satisfatibilidade para a lógica do saber-como distribuído.