O que podemos provar com gráficos infinitos que não podemos provar sem eles?

Esta é uma pergunta subsequente a esta sobre gráficos infinitos.

As respostas e os comentários a essa pergunta listam objetos e situações que são modelados naturalmente por gráficos infinitos. Mas também existem numerosos teoremas sobre gráficos infinitos (ver capítulo 8 no livro de Diestel), dos quais, por exemplo, o lema infinito de Koenig é muito famoso.

Agora, tenho a seguinte pergunta: O que podemos provar com gráficos infinitos que não podemos provar sem eles? Ou, mais especificamente, qual é um exemplo em que modelamos algo como um gráfico infinito, depois invocamos um teorema sobre gráficos infinitos e, no final, provamos algo sobre o problema original - sem saber como provar o contrário?

Aqui está um exemplo da computação distribuída:

1. Fundo

1.1 Modelo de memória compartilhada assíncrona

Vamos considerar uma coleção de nós distribuídos que se comunicam usando variáveis ​​de memória compartilhada. Há um adversário que controla quando um nó executa etapas e quando entregar mensagens. A computação é assíncrona , ou seja, o adversário pode atrasar as etapas dos nós por qualquer quantidade (finita) de tempo.
Você pode pensar em uma etapa de um nó como uma transição de estado de seu autômato local (de acordo com o algoritmo) em que o próximo estado é determinado pelo estado atual e pelas observações do nó desde a última etapa.

1.2 Segurança e Vida

Ao raciocinar formalmente sobre as propriedades de um algoritmo assíncrono, distinguimos entre propriedades de segurança e de vivacidade. Informalmente, uma propriedade de segurança pode ser interpretada como uma garantia de que algo "ruim" nunca acontece. (Por exemplo, para exclusão mútua, uma propriedade de segurança seria que dois nós não entrem na seção crítica simultaneamente.) A vitalidade , por outro lado, pode ser interpretada como "algo de bom acabará por acontecer", por exemplo: todo nó eventualmente termina.

${M}$$M$$\alpha,\beta \in M$$2^{-n}$$n$$\alpha$$\beta$

$S$$P\subseteq M$$P$$M\setminus P$

Aplicando o lema infinito de Koenig

Nem sempre é fácil verificar se uma propriedade específica é uma propriedade de segurança: considere a implementação de objetos atômicos de leitura / gravação em cima de variáveis ​​básicas de memória compartilhada. Essa implementação deve manipular solicitações e suas respostas de uma maneira que as faça parecer como se elas acontecessem em algum instante no tempo e não viole sua ordem de chamada. (Devido à operação assíncrona, a duração real entre solicitação e resposta pode ser diferente de zero.) A atomicidade também é conhecida como Linearizabilidade . A seção 13.1 de [A] fornece uma prova de que a atomicidade é uma propriedade de segurança. A prova usa o lema de Koenig para mostrar que o limite de qualquer sequência infinita de execuções (cada uma delas satisfaz a atomicidade) também satisfaz a atomicidade.

N. Lynch. Algoritmos distribuídos. Morgan Kaufmann, 1996.