Pr-1st-1.1-m09-Slajd17

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Zakończenie dynamiczne \leftrightarrow statyczne

Zakończenie dynamiczne statyczne


Niech oznacza, że zajście predykatu prowadzi w skończonym choć nieprzewidzianym czasie do zajścia predykatu .

Twierdzenie 9.1

Dowód

W chwili , gdy , wszystkie procesy są pasywne, zachodzi , a część wiadomości może znajdować się w kanałach. Jednakże, wszystkie wiadomości transmitowane są brane pod uwagę, a ich dotarcie do węzłów docelowych iw konsekwencji ich dostępność, jest uwzględniona w wartości predykatu \neg . Wobec niezawodności kanałów, wiadomości transmitowane osiągną węzły docelowe po skończonym choć nieprzewidywalnym czasie, w pewnym momencie . Wówczas . Wobec stałej pasywności wszystkich procesów od chwili \tau, w każdej chwili , oraz .Stąd otrzymujemy:

Predykat przyjmuje zatem wartość True.

Udowodniliśmy więc, że opóźnienie między momentem zajścia predykatu a momentem zajścia predykatu jest skończone lecz nieprzewidywalne. Wybór między jedną a drugą definicją zakończenia zależy oczywiście od użytkownika. Łatwo przewidzieć, że detekcja stanu opisanego predykatem będzie trudniejsza, a więc w ogolności bardziej kosztowna. Z drugiej jednak strony, zajście może pozwolić, na przykład, na uznanie wyników przetwarzania za ostateczne (w konsekwencji możliwe do dalszego wykorzystania) nawet, gdy pewne wiadomości są jeszcze transmitowane.



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