Apa yang bisa kita buktikan dengan grafik tak terbatas yang tidak dapat kita buktikan tanpa grafik?

Ini adalah pertanyaan lanjutan untuk ini tentang grafik tak terbatas.

Jawaban dan komentar untuk objek daftar pertanyaan dan situasi yang secara alami dimodelkan oleh grafik tak terbatas. Tetapi ada juga banyak teorema tentang grafik tak terbatas (lihat bab 8 dalam buku Diestel) yang, misalnya, lemma tak terhingga Koenig adalah yang sangat terkenal.

Sekarang saya memiliki pertanyaan berikut: Apa yang bisa kita buktikan dengan grafik tanpa batas yang tidak bisa kita buktikan tanpa grafik? Atau lebih khusus lagi, apa contoh di mana kita memodelkan sesuatu sebagai grafik tak terbatas, kemudian mengajukan teorema tentang grafik tak terbatas, dan pada akhirnya telah membuktikan sesuatu tentang masalah asli - tanpa mengetahui bagaimana membuktikannya sebaliknya?

Berikut ini contoh dari komputasi terdistribusi:

1 Latar Belakang

1.1 Model Memori Bersama Asinkron

Mari kita pertimbangkan kumpulan node terdistribusi yang berkomunikasi menggunakan variabel memori bersama. Ada musuh yang mengontrol kapan sebuah simpul mengambil langkah dan kapan harus mengirimkan pesan. Komputasi asynchronous , yaitu, musuh dapat menunda langkah-langkah node untuk setiap jumlah waktu (terbatas).
Anda bisa memikirkan langkah sebuah simpul sebagai transisi keadaan dari otomat lokalnya (sesuai dengan algoritma) di mana keadaan selanjutnya ditentukan oleh keadaan saat ini dan pengamatan simpul sejak langkah terakhir.

1.2 Keselamatan dan Kehidupan

Ketika secara formal beralasan tentang sifat-sifat algoritma asinkron, kami membedakan antara sifat-sifat keamanan dan sifat. Secara informal, properti keamanan dapat diartikan sebagai jaminan bahwa sesuatu yang "buruk" tidak pernah terjadi. (Misalnya, untuk saling pengecualian, properti keamanan adalah bahwa tidak ada dua node yang memasuki bagian kritis secara bersamaan.) Sebaliknya , Live , dapat diartikan sebagai "sesuatu yang baik pada akhirnya akan terjadi", misalnya: setiap node akhirnya berakhir.

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

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

Menerapkan Koenig's Infinity Lemma

Tidak selalu mudah untuk melihat apakah properti tertentu adalah properti keamanan: Pertimbangkan penerapan objek atom baca / tulis di atas variabel memori dasar bersama. Implementasi seperti itu harus menangani permintaan dan tanggapan mereka dengan cara yang membuat mereka tampak seolah-olah itu terjadi pada saat tertentu dan tidak melanggar urutan permohonan mereka. (Karena operasi asinkron, durasi aktual antara permintaan dan respons mungkin bukan nol.) Atomicity juga dikenal sebagai Linearizability . Bagian 13.1 dari [A] memberikan bukti bahwa Atomicity adalah properti keselamatan. Buktinya menggunakan lemma Koenig untuk menunjukkan bahwa batas dari setiap eksekusi tanpa batas (yang masing-masing memenuhi Atomicity) juga memenuhi Atomicity.

[A] N. Lynch. Algoritma Terdistribusi. Morgan Kaufmann, 1996.