Что мы можем доказать бесконечными графами, что мы не можем доказать без них?

Это дополнительный вопрос к этому вопросу о бесконечных графах.

Ответы и комментарии к этому списку объектов и ситуаций, которые естественным образом моделируются бесконечными графами. Но есть также многочисленные теоремы о бесконечных графах (см. Главу 8 в книге Дистеля), из которых, например, лемма Кенига о бесконечности очень известна.

Теперь у меня следующий вопрос: что мы можем доказать с помощью бесконечных графов, что мы не можем доказать без них? Или, более конкретно, каков пример, в котором мы моделируем что-то как бесконечный граф, затем вызываем теорему о бесконечных графах, и в конце концов доказали что-то об исходной задаче - не зная, как доказать это иначе?

Вот пример из распределенных вычислений:

1. Фон

1.1 Модель асинхронной разделяемой памяти

Давайте рассмотрим коллекцию распределенных узлов, которые взаимодействуют с помощью переменных общей памяти. Есть злоумышленник, который контролирует, когда узел предпринимает шаги и когда доставлять сообщения. Вычисление асинхронное , т. Е. Злоумышленник может задержать шаги узлов на любое (конечное) количество времени.
Вы можете думать о шаге узла как переход состояния его локального автомата (в соответствии с алгоритмом), в котором следующее состояние определяется текущим состоянием и наблюдениями за узлом с момента последнего шага.

1.2 Безопасность и жизнедеятельность

При формальном рассуждении о свойствах асинхронного алгоритма мы различаем свойства безопасности и живучести. Неформально свойство безопасности может быть истолковано как гарантия того, что что-то «плохое» никогда не случится. (Например, для взаимного исключения свойство безопасности состоит в том, что никакие два узла не входят в критическую секцию одновременно.) Жизнеспособность , с другой стороны, может интерпретироваться как «что-то хорошее в конечном итоге случится», например: каждый узел в конечном итоге завершается.

${M}$$M$$\alpha,\beta \in M$$2^{-n}$$n$$\alpha$$\beta$ различаются.

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

Применяя лемму о бесконечности Кенига

Не всегда легко увидеть, является ли конкретное свойство безопасным свойством: рассмотрим реализацию атомарных объектов чтения / записи поверх базовых переменных общей памяти. Такая реализация должна обрабатывать запросы и их ответы таким образом, чтобы они выглядели так, как будто они происходят в какой-то момент времени, и не нарушали порядок их вызова. (Из-за асинхронной операции фактическая продолжительность между запросом и ответом может быть ненулевой.) Атомарность также известна как линеаризуемость. . Раздел 13.1 [A] дает доказательство того, что атомарность является свойством безопасности. В доказательстве используется лемма Кенига, чтобы показать, что предел любой бесконечной последовательности исполнений (каждое из которых удовлетворяет атомарности) также удовлетворяет атомарности.

[A] Н. Линч. Распределенные алгоритмы. Морган Кауфманн, 1996.