Pr-1st-1.1-m10-Slajd11

Detekcja zakończenia dla atomowego modelu przetwarzania - twierdzenie 10.1

Twierdzenie 10.1

Jeżeli

$RC^{*}=SC^{*}=RC^{**}=SC^{**}$

to monitorowane przetwarzanie aplikacyjne osiągnęło stan zakończenia przed zakończeniem procesu detekcji

Dowód

W celu udowodnienia powyższego twierdzenia wykażemy, że jeżeli $RC^{*}=SC^{**}$, to przetwarzanie jest w stanie zakończenia. W tym wykażemy w dalszym ciągu prawdziwość pięciu lematów.

<< Poprzedni slajd | Spis treści | Następny slajd >>