¿Qué podemos probar con gráficos infinitos que no podemos probar sin ellos?

Esta es una pregunta de seguimiento a esta sobre gráficos infinitos.

Las respuestas y los comentarios a esa pregunta enumeran objetos y situaciones que se modelan naturalmente mediante gráficos infinitos. Pero también hay numerosos teoremas sobre gráficos infinitos (ver capítulo 8 en el libro de Diestel) de los cuales, por ejemplo, el lema de infinito de Koenig es muy famoso.

Ahora tengo la siguiente pregunta: ¿Qué podemos probar con gráficos infinitos que no podemos probar sin ellos? O más específicamente, ¿cuál es un ejemplo en el que modelamos algo como un gráfico infinito, luego invocamos un teorema sobre gráficos infinitos y al final hemos demostrado algo sobre el problema original, sin saber cómo demostrarlo de otra manera?

Aquí hay un ejemplo de computación distribuida:

1. Antecedentes

1.1 Modelo asíncrono de memoria compartida

Consideremos una colección de nodos distribuidos que se comunican usando variables de memoria compartida. Hay un adversario que controla cuándo un nodo toma medidas y cuándo entregar mensajes. El cálculo es asíncrono , es decir, el adversario puede retrasar los pasos de los nodos por cualquier cantidad de tiempo (finito).
Puede pensar en un paso de un nodo como una transición de estado de su autómata local (de acuerdo con el algoritmo) donde el siguiente estado está determinado por el estado actual y las observaciones del nodo desde el último paso.

1.2 Seguridad y vida

Cuando razonamos formalmente sobre las propiedades de un algoritmo asíncrono, distinguimos entre propiedades de seguridad y de vida. Informalmente, una propiedad de seguridad puede interpretarse como una garantía de que algo "malo" nunca sucede. (Por ejemplo, para la exclusión mutua, una propiedad de seguridad sería que no hay dos nodos que ingresen a la sección crítica simultáneamente). La vida , por otro lado, puede interpretarse como "algo bueno eventualmente sucederá", por ejemplo: cada nodo finalmente termina.

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

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

Aplicando el Lema Infinito de Koenig

No siempre es sencillo ver si una propiedad específica es una propiedad de seguridad: considere la implementación de objetos atómicos de lectura / escritura sobre las variables básicas de memoria compartida. Dicha implementación debe manejar las solicitudes y sus respuestas de manera que parezca que suceden en algún momento y no violan su orden de invocación. (Debido a la operación asincrónica, la duración real entre la solicitud y la respuesta puede ser distinta de cero). La atomicidad también se conoce como linealización . La Sección 13.1 de [A] da una prueba de que la Atomicidad es una propiedad de seguridad. La prueba utiliza el lema de Koenig para mostrar que el límite de cualquier secuencia infinita de ejecuciones (cada una de las cuales satisface la Atomicidad) también satisface la Atomicidad.

[A] N. Lynch. Algoritmos Distribuidos. Morgan Kaufmann, 1996.