Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

1. Formulação do Problema

O artigo aborda o desafio de modelar a comunicação assíncrona em sistemas multiagente usando Lógica Epistêmica Dinâmica (DEL).

• A Lacuna: A DEL padrão (por exemplo, Lógica de Anúncio Público) trata a comunicação como instantânea e sincronizada: uma mensagem é enviada e recebida por todos os agentes simultaneamente. Isso falha em capturar sistemas distribuídos do mundo real, onde o envio e o recebimento são eventos distintos que ocorrem em momentos diferentes.
• O Desafio Específico: Os autores visam formalizar uma lógica onde:
  1. Os agentes possuem incerteza temporal quanto ao histórico de mensagens (eles não sabem quantas mensagens os outros receberam).
  2. Os agentes possuem incerteza epistêmica quanto ao estado do mundo.
  3. A lógica deve distinguir entre o envio de uma mensagem (transmissão) e o recebimento de uma mensagem (ação individual).
  4. O sistema deve lidar com a validade em dois contextos:
     • $\epsilon$-validade: Verdade no estado inicial (histórico vazio).
     • $\ast$-validade (sempre-válida): Verdade em qualquer estado dado qualquer histórico prévio de envio e recebimento.

Trabalhos anteriores (especificamente a referência [4]) forneceram uma axiomatização ($AA$) para $\epsilon$-validades usando um sistema de redução (reduzindo modalidades dinâmicas a epistêmicas estáticas). No entanto, essa abordagem de redução falha para $\ast$-validades porque as propriedades do sistema mudam fundamentalmente assim que um histórico existe (por exemplo, os agentes podem ter recebido números diferentes de mensagens).

2. Metodologia

2.1 Linguagem e Sintaxe

Os autores definem uma linguagem $\mathcal{L}$ que estende a lógica modal multiagente com dois tipos de modalidades dinâmicas:

• Transmissão: $\langle \varphi \rangle \psi$ (A fórmula $\varphi$ é anunciada/transmitida; subsequentemente $\psi$ vale).
• Recebimento: $\langle a \rangle \psi$ (O agente $a$ recebe a próxima mensagem em sua fila; subsequentemente $\psi$ vale).
• Palavras de Histórico: Sequências de agentes e fórmulas (por exemplo, $p.a.q$) representam a sequência de eventos. Um histórico é uma palavra onde, para cada agente, o número de mensagens recebidas nunca excede o número de mensagens enviadas (restrição FIFO).

2.2 Semântica

A semântica é definida sobre pares $(s, \alpha)$, onde $s$ é um estado em um modelo de Kripke e $\alpha$ é uma palavra de histórico.

• Executabilidade ($\triangleright\triangleleft$): Uma relação que determina se um histórico $\alpha$ pode ser executado no estado $s$. Isso garante que:
  1. O histórico seja uma sequência válida (FIFO).
  2. Todas as fórmulas anunciadas tenham sido verdadeiras no momento de sua transmissão.
  3. Os agentes considerem apenas históricos executáveis em estados que eles consideram possíveis.
• Relação de Visão ($\triangleright_a$): Define o que o agente $a$ considera possível. O agente $a$ considera um histórico $\beta$ possível em relação ao histórico real $\alpha$ se a sequência de mensagens que $a$ recebeu em $\beta$ corresponder exatamente ao que recebeu em $\alpha$. Crucialmente, os agentes não imaginam históricos contendo mensagens que ainda não receberam.
• Sabor Trivalente: A semântica comporta-se de certa forma como uma lógica trivalente. Se um histórico não for executável em um estado ($s \not\triangleright\triangleleft \alpha$), as fórmulas não são nem verdadeiras nem falsas naquele par, embora a lógica mantenha as validades padrão.

2.3 A Fórmula "Vazia"

Uma inovação técnica central é a definição de uma fórmula empty:
$$\text{empty} := \bigwedge_{a \in A} [a]\bot \land \bigwedge_{a,b \in A} K_a [b]\bot$$
Esta fórmula caracteriza o estado onde o histórico está vazio ($\alpha = \epsilon$). Ela afirma que nenhuma mensagem foi recebida por ninguém e que todos sabem disso. Isso só é possível em um cenário multiagente ($|A| \ge 2$).

3. Contribuições Principais

3.1 Axiomatização $AA^*$

A contribuição primária é a proposta de $AA^*$, uma axiomatização para $\ast$-validades (sempre-válidas).

• Natureza Infinitária: Diferente do sistema anterior baseado em redução $AA$, a$AA^*$ é infinitária. Ela não pode reduzir modalidades dinâmicas a estáticas porque a verdade das fórmulas depende do histórico específico.
• A Regra $(R^*)$: O sistema inclui uma regra infinitária:
  • Premissa: Para todas as palavras $\alpha$, $\text{empty} \to [\alpha]\varphi$ é derivável.
  • Conclusão: $\varphi$ é derivável.
    Esta regra efetivamente reduz a $\ast$-validade à $\epsilon$-validade ao "resetar" o histórico para vazio através da fórmula empty.
• Axiomas: O sistema inclui axiomas para:
  • Distribuição do conhecimento e modalidades dinâmicas.
  • Condições de executabilidade (por exemplo, uma mensagem só pode ser recebida se foi enviada).
  • Permeabilidade atômica (os valores de verdade dos átomos não mudam).
  • Um axioma específico para conhecimento em cenários assíncronos: $\text{empty} \to (K_a \varphi \leftrightarrow ([\alpha]\bot \lor \bigvee_{\alpha \triangleright_a \beta} K_a [\beta]\varphi))$.

3.2 Completude e Corretude

• Corretude: Os autores provam que todo teorema em $AA^*$ é $\ast$-válido.
• Completude: Eles provam que toda fórmula $\ast$-válida é um teorema de $AA^*$. A prova utiliza uma construção de modelo canônico baseada em teorias maximais consistentes. Um obstáculo técnico significativo foi definir as relações de acessibilidade no modelo canônico para garantir que elas formem relações de equivalência apenas quando restritas a teorias contendo empty.

3.3 A Limitação de Agente Único

O artigo demonstra rigorosamente que o método proposto falha para um único agente.

• Em um sistema de agente único, um agente sempre sabe que recebeu todas as mensagens que viu. Não há nenhuma fórmula equivalente a empty que possa distinguir um histórico vazio de um não vazio onde o agente recebeu tudo.
• Consequentemente, a redução de $\ast$-validade para $\epsilon$-validade via empty é impossível no caso de agente único. Os autores deixam a axiomatização para o caso de agente único como um problema em aberto.

4. Resultados

1. Sistema Formal: Uma axiomatização infinitária completa e correta ($AA^*$) para lógica epistêmica assíncrona com modalidades separadas de envio/recebimento.
2. Mecanismo de Redução: Um método inovador para lidar com "sempre-validade" usando a fórmula empty para ancorar a lógica de volta ao estado inicial, contornando a necessidade de um sistema de redução finito.
3. Distinção de S5: A lógica não satisfaz globalmente o axioma de verdade padrão S5 ($K_a \varphi \to \varphi$). O conhecimento é factual apenas se o agente souber que o histórico está vazio. Caso contrário, a modalidade comporta-se mais como "crença consistente".
4. Comparação com Computação Distribuída: A semântica alinha-se com o conceito de cortes consistentes em sistemas distribuídos, mas refina-o incorporando condições de verdade (executabilidade) diretamente na lógica, prevenindo estados inconsistentes (por exemplo, receber uma mensagem antes de ser enviada, ou receber um anúncio falso).

5. Significado

• Avanço Teórico: Este trabalho preenche a lacuna entre a Lógica Epistêmica Dinâmica padrão (que assume sincronia) e as realidades da computação distribuída (assincronia). Fornece a primeira estrutura lógica rigorosa que trata o envio e o recebimento como eventos distintos, assíncronos, com modalidades separadas.
• Tratamento da Incerteza Temporal: Modela com sucesso o tipo específico de incerteza onde os agentes não têm certeza do comprimento do histórico de comunicação em relação aos outros, um cenário comum em protocolos de fofoca e consenso distribuído.
• Inovação Metodológica: O uso de uma regra infinitária ($R^*$) combinada com uma fórmula específica de "reset" (empty) oferece um novo modelo para axiomatizar lógicas onde propriedades dinâmicas não podem ser reduzidas a estáticas via reescrita finita.
• Direções Futuras: O artigo identifica caminhos claros para pesquisa futura, incluindo a extensão da lógica para conhecimento de grupo (conhecimento distribuído), comunicação não pública e a resolução do problema da axiomatização de agente único.

Em resumo, o artigo estabelece uma base lógica robusta para o raciocínio sobre conhecimento em ambientes assíncronos, provando que, embora técnicas de redução padrão falhem, um sistema infinitário cuidadosamente construído pode capturar a complexidade total da passagem de mensagens assíncrona.