Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

1. Enunciato del Problema

Il paper affronta la sfida di modellare la comunicazione asincrona nei sistemi multi-agente utilizzando la Logica Epistemica Dinamica (DEL).

• Il Divario: La DEL standard (ad esempio, la Logica dell'Annuncio Pubblico) tratta la comunicazione come istantanea e sincronizzata: un messaggio viene inviato e ricevuto da tutti gli agenti simultaneamente. Ciò fallisce nel catturare i sistemi distribuiti reali, dove l'invio e la ricezione sono eventi distinti che si verificano in momenti diversi.
• La Sfida Specifica: Gli autori mirano a formalizzare una logica in cui:
  1. Gli agenti hanno incertezza temporale riguardo alla storia dei messaggi (non sanno quanti messaggi gli altri hanno ricevuto).
  2. Gli agenti hanno incertezza epistemica riguardo allo stato del mondo.
  3. La logica deve distinguere tra l'invio di un messaggio (broadcast) e la ricezione di un messaggio (azione individuale).
  4. Il sistema deve gestire la validità in due contesti:
     • $\epsilon$-validità: Verità nello stato iniziale (storia vuota).
     • $\ast$-validità (Validità-sempre): Verità in qualsiasi stato data qualsiasi storia precedente di invio e ricezione.

Il lavoro precedente (in particolare il riferimento [4]) ha fornito un'assiomatizzazione ($AA$) per le $\epsilon$-validità utilizzando un sistema di riduzione (riducendo le modalità dinamiche a quelle epistemiche statiche). Tuttavia, questo approccio di riduzione fallisce per le $\ast$-validità perché le proprietà del sistema cambiano fondamentalmente una volta che esiste una storia (ad esempio, gli agenti possono aver ricevuto un numero diverso di messaggi).

2. Metodologia

2.1 Linguaggio e Sintassi

Gli autori definiscono un linguaggio $\mathcal{L}$ che estende la logica modale multi-agente con due tipi di modalità dinamiche:

• Broadcasting: $\langle \varphi \rangle \psi$ (La formula $\varphi$ viene annunciata/diffusa; successivamente $\psi$ vale).
• Ricezione: $\langle a \rangle \psi$ (L'agente $a$ riceve il prossimo messaggio nella sua coda; successivamente $\psi$ vale).
• Parole Storia: Sequenze di agenti e formule (ad esempio, $p.a.q$) rappresentano la sequenza degli eventi. Una storia è una parola in cui, per ogni agente, il numero di messaggi ricevuti non supera mai il numero di messaggi inviati (vincolo FIFO).

2.2 Semantica

La semantica è definita su coppie $(s, \alpha)$, dove $s$ è uno stato in un modello di Kripke e $\alpha$ è una parola storia.

• Eseguibilità ($\triangleright\triangleleft$): Una relazione che determina se una storia $\alpha$ può essere eseguita nello stato $s$. Ciò garantisce che:
  1. La storia sia una sequenza valida (FIFO).
  2. Tutte le formule annunciate fossero vere al momento della loro diffusione.
  3. Gli agenti considerino eseguibili solo storie in stati che ritengono possibili.
• Relazione di Visione ($\triangleright_a$): Definisce ciò che l'agente $a$ considera possibile. L'agente $a$ considera una storia $\beta$ possibile rispetto alla storia effettiva $\alpha$ se la sequenza di messaggi che $a$ ha ricevuto in $\beta$ corrisponde esattamente a ciò che ha ricevuto in $\alpha$. Crucialmente, gli agenti non immaginano storie contenenti messaggi che non hanno ancora ricevuto.
• Tono Trivalente: La semantica si comporta in qualche modo come una logica trivalente. Se una storia non è eseguibile in uno stato ($s \not\triangleright\triangleleft \alpha$), le formule non sono né vere né false in quella coppia, sebbene la logica mantenga le validità standard.

2.3 La Formula "Vuota"

Un'innovazione tecnica centrale è la definizione di una formula empty:
$$\text{empty} := \bigwedge_{a \in A} [a]\bot \land \bigwedge_{a,b \in A} K_a [b]\bot$$
Questa formula caratterizza lo stato in cui la storia è vuota ($\alpha = \epsilon$). Afferma che nessun messaggio è stato ricevuto da nessuno e che tutti lo sanno. Ciò è possibile solo in un contesto multi-agente ($|A| \ge 2$).

3. Contributi Chiave

3.1 Assiomatizzazione $AA^*$

Il contributo principale è la proposta di $AA^*$, un'assiomatizzazione per le $\ast$-validità (validità-sempre).

• Natura Infinitaria: A differenza del precedente sistema basato sulla riduzione $AA$, $AA^*$ è infinitaria. Non può ridurre le modalità dinamiche a quelle statiche perché la verità delle formule dipende dalla storia specifica.
• La Regola $(R^*)$: Il sistema include una regola infinitaria:
  • Premessa: Per tutte le parole $\alpha$, $\text{empty} \to [\alpha]\varphi$ è derivabile.
  • Conclusione: $\varphi$ è derivabile.
    Questa regola riduce efficacemente la $\ast$-validità alla $\epsilon$-validità "resettando" la storia a vuota tramite la formula empty.
• Assiomi: Il sistema include assiomi per:
  • Distribuzione della conoscenza e delle modalità dinamiche.
  • Condizioni di eseguibilità (ad esempio, un messaggio può essere ricevuto solo se è stato inviato).
  • Permanenza atomica (i valori di verità degli atomi non cambiano).
  • Un assioma specifico per la conoscenza in contesti asincroni: $\text{empty} \to (K_a \varphi \leftrightarrow ([\alpha]\bot \lor \bigvee_{\alpha \triangleright_a \beta} K_a [\beta]\varphi))$.

3.2 Completezza e Correttezza

• Correttezza: Gli autori dimostrano che ogni teorema in $AA^*$ è $\ast$-valido.
• Completezza: Dimostrano che ogni formula $\ast$-valida è un teorema di $AA^*$. La prova utilizza una costruzione di modello canonico basata su teorie massimamente consistenti. Un significativo ostacolo tecnico è stato definire le relazioni di accessibilità sul modello canonico per garantire che formino relazioni di equivalenza solo quando ristrette alle teorie contenenti empty.

3.3 Il Limite dell'Agente Singolo

Il paper dimostra rigorosamente che il metodo proposto fallisce per un singolo agente.

• In un sistema ad agente singolo, un agente sa sempre di aver ricevuto tutti i messaggi che ha visto. Non esiste una formula equivalente a empty che possa distinguere una storia vuota da una non vuota in cui l'agente ha ricevuto tutto.
• Di conseguenza, la riduzione dalla $\ast$-validità alla $\epsilon$-validità tramite empty è impossibile nel caso di agente singolo. Gli autori lasciano l'assiomatizzazione per il caso di agente singolo come problema aperto.

4. Risultati

1. Sistema Formale: Un'assiomatizzazione infinitaria completa e corretta ($AA^*$) per la logica epistemica asincrona con modalità separate di invio/ricezione.
2. Meccanismo di Riduzione: Un metodo innovativo per gestire la "validità-sempre" utilizzando la formula empty per ancorare la logica allo stato iniziale, aggirando la necessità di un sistema di riduzione finito.
3. Distinzione da S5: La logica non soddisfa globalmente l'assioma di verità standard S5 ($K_a \varphi \to \varphi$). La conoscenza è fattuale solo se l'agente sa che la storia è vuota. Altrimenti, la modalità si comporta più come una "credenza coerente".
4. Confronto con l'Informatica Distribuita: La semantica si allinea con il concetto di tagli coerenti nei sistemi distribuiti, ma lo rifina incorporando le condizioni di verità (eseguibilità) direttamente nella logica, prevenendo stati inconsistenti (ad esempio, ricevere un messaggio prima che sia inviato, o ricevere un annuncio falso).

5. Significato

• Avanzamento Teorico: Questo lavoro colma il divario tra la Logica Epistemica Dinamica standard (che assume sincronia) e le realtà dell'informatica distribuita (asincronia). Fornisce il primo quadro logico rigoroso che tratta l'invio e la ricezione come eventi distinti e asincroni con modalità separate.
• Gestione dell'Incertezza Temporale: Modella con successo il tipo specifico di incertezza in cui gli agenti non sono sicuri della lunghezza della storia di comunicazione rispetto agli altri, uno scenario comune nei protocolli di gossip e nel consenso distribuito.
• Innovazione Metodologica: L'uso di una regola infinitaria ($R^*$) combinata con una specifica formula di "reset" (empty) offre un nuovo modello per l'assiomatizzazione di logiche in cui le proprietà dinamiche non possono essere ridotte a quelle statiche tramite riscrittura finita.
• Direzioni Future: Il paper identifica percorsi chiari per la ricerca futura, inclusa l'estensione della logica alla conoscenza di gruppo (conoscenza distribuita), alla comunicazione non pubblica e alla risoluzione del problema dell'assiomatizzazione per l'agente singolo.

In sintesi, il paper stabilisce una solida base logica per il ragionamento sulla conoscenza in ambienti asincroni, dimostrando che, sebbene le tecniche di riduzione standard falliscano, un sistema infinitario attentamente costruito può catturare l'intera complessità del passaggio di messaggi asincrono.