پاورپوینت

بخشی از پاورپوینت

اسلاید 1 :

بطور کلی یک سیستم گذار می تواند حالات زیادی داشته باشد از این رو چک کردن یک فرمول درآن بسیار زمانبراست، در نتیجه یافتن یک الگوریتم کارا می تواند بسیار موثر باشد.
در ابتدا الگوریتمهای CTL model checking مطرح می شود .
ما انتظار داریم که یک الگوریتم برای یک مدل M, s ∈ S وفرمول φبتواند محاسبه کند که آیا M ، φ را ارضا می کند یا نه :
M, s |= φ
در مواردی که φ ارضا نشود، الگوریتم باید مسیری را که M نمی تواند φرا ارضا کند تولید کند.
راههای مختلفی برای پاسخ به سوال فوق وجود دارد:
Model-checking algorithm

اسلاید 2 :

یک روش این است که M و φ و s0 به عنوان ورودی باشد.

هدف: ‘yes’ (M, s0|= φ holds)
‘no’ (M, s0|= φ does not hold)

روش دوم: M و φ به عنوان ورودی و خروجی،همه حالتهایی باشد از مدل M ،که φ را ارضا کند.
پیدا کردن الگوریتم بر اساس روش دوم راحت تر است که البته با این کار به سوال اول نیزپاسخ داده ایم. زیرا کافی است چک کنیم که آیا s0 عضو مجموعه خروجی هست یا نه.

The labelling algorithm
الگوریتم برچسب گذار :

ورودی: یک مدل M= (S,→, L) درCTLوφ یک فرمول CTL
خروجی: مجموعه حالتهایی از مدل M که فرمول φ را ارضا می کند.

اسلاید 3 :

1.ابتدا تابع φ, TRANSLATE(φ) را بر اساس عملگرهای AF, EU, EX, ∧, ￢ و⊥ بازنویسی می کند.
برای هر فرمول دلخواه φ به فرمCTL ، ما در ابتدا آن را به فرم معادلش با عملگرهای فوق تبدیل می کنیم و بعد الگوریتم را فراخوانی می کنیم.

2.حالتهایی از M را با زیر فرمولهای از φ که درآنجا برقرار شده برچسب گذاری می کنیم و برای شروع از کوچکترین زیرفرمول φ استفاده می کنیم و به سمت φ حرکت میکنیم.
3. این کار را برای همه زیرفرمولهای φ انجام می شود. در آخر حالتهایی که با φ برچسب خورده اند به خروجی می روند .
فرض کنید ψ زیر فرمولی از φ باشد وحالتهایی که زیر فرمولهای ψ را ارضا می کند پیش از این برچسب خورده اند.
نحوه برچسب خوردن حالتها با ψ به صورت زیر است :

اسلاید 7 :

پیچیدگی الگوریتم:
O(f ・ V ・ (V + E))

f تعداد رابط ها در فرمول، E تعداد گذارها، V تعداد حالتها .
با توجه به رابطه فوق، پیچیدگی بر اساس اندازه فرمول خطی و بر اساس سایز مدل درجه 2 است.


Handling EG directly

برای دو عملگر AG و EG می توان الگوریتمی در نظر گرفت که به صورت مستقیم برای آنها اجرا شود.

اسلاید 8 :

الگوریتم EG ψ1 :

همه حالتها را EGψ1 برچسب گذاری کن.
اگر حالتی با ψ1 برچسب نخورده بود، آنگاه برچسب EGψ1 را حذف کن.
اگر هیچ یک از حالتهای مابعد حالت جاری با EGψ1 برچسب نداشت آنگاه برچسب EGψ1 را حذف کن. این کار را تا زمانی ادامه بده که دیگر تغییری رخ ندهد.
این روش با روش قبل هیچ تفاوتی ندارد.در روش قبل هم باید از فرم معادل EGψ1 یعنی ￢AF￢ψ استفاده شود.

با یک راه هوشمندانه می توان زمان الگوریتم برچسب گذار را بهبود بخشید.به طوری که به جای استفاده از EX, EUوAF از EX, EU و EG استفاده می کنیم.

اسلاید 9 :

این الگوریتم برای EGψ به صورت زیر است :
گراف حالات را محدود به حالتهایی کن که ψ را ارضا می کند، (حالتهای دیگر و گذارهای آنها را حذف کن.)
بزرگترین مؤلفه قویاً همبند را در گراف حالات پیدا کن (SCCs) .
(بزرگترین مؤلفه قویاً همبند maximal strongly connected components :
بزرگترین زیرگرافی از یک گراف است که بین همه گره های آن حداقل یک مسیر وجود دارد.)
با استفاده از روش جستجوی سطح اول بصورت عقبگرد
(backwards breadth-first search ) روی زیرگراف محدود شده ، هر حالتی را که به یک (SCCs)می رسد پیدا کن.

پیچیدگی الگوریتم:

O(f ・ (V + E))

اسلاید 10 :

مثال (20 . 3 ): الگوریتم برچسب گذار اولیه را روی دومین مدل انحصارمتقابل با فرمول E[￢c2 U c1 ] اجرا می کنیم.

فاز 1: همه حالتهایی کهc1 را ارضا می کند با این E[￢c2 U c1 ] برچسب می خورند.
(s2 و s4 )

فاز 2: همه حالتهایی کهc2 را ارضا نمی کنند و یک حالت مابعدی دارند که قبلاً برچسب خورده اند برچسب گذاری می شود.
(s3 و s1 )

فاز 3 : تنها s0 برچسب گذاری می شود چون هم c2 را ارضا نمی کند وهم گره مابعد آن (s1)برچسب خورده است که در اینجا الگوریتم خاتمه می یابد.

اسلاید 12 :

The pseudo-code of the CTL model-checking algorithm
شبه کدی برای الگوریتم CTL model checking

دراین الگوریتم :
ورودی تابع SAT یک فرمولCTL است و فرض می شود که می تواند به هر قسمت مدل M ،
S ، L،→دسترسی داشته باشد و خروجی مجوعه حالاتی است که فرمول را ارضا می کنند.

X, Y , V وW زیر مجموعه ای از حالات هستند .

از توابع زیر نیز استفاده شده است :

pre∃(Y) = {s ∈ S | exists s´, (s → s´ and s´ ∈ Y )}
pre∀(Y) = {s ∈ S | for all s´, (s → s´ implies s´ ∈ Y )}.

اسلاید 13 :

pre∃(Y) = {s ∈ S | exists s´, (s → s´ and s´∈ Y )}
pre∀(Y) = {s ∈ S | for all s´, (s → s´ implies s´∈ Y )}.

1.زیرمجموعه ای از حالتها است که می توانند یک گذار به Y داشته باشند.
2.زیرمجموعه ای از حالتها است که فقط به Y گذار می کند

pre∃(Y) و pre∀(Y) به صورت زیر مکمل یکدیگرند:

pre∀(Y ) = S − pre∃(S − Y)

اسلاید 14 :

function SAT (φ)
/* determines the set of states satisfying φ */
begin
Case
φ is T : return S

φ is ⊥ : return ∅

φ is atomic: return {s ∈ S | φ ∈ L(s)}

φ is ￢φ1 : return S − SAT (φ1)

φ is φ1 ∧ φ2 : return SAT (φ1) ∩ SAT (φ2)

φ is φ1 ∨ φ2 : return SAT (φ1) ∪ SAT (φ2)

φ is φ1 → φ2 : return SAT (￢φ1 ∨ φ2)

φ is AXφ1 : return SAT (￢EX￢φ1)

اسلاید 15 :

φ is EXφ1 : return SATEX(φ1)

φ is A[φ1 U φ2] :
return SAT(￢(E[￢φ2 U (￢φ1 ∧￢φ2)] ∨ EG￢φ2))

φ is E[φ1 U φ2] : return SATEU(φ1, φ2)

φ is EFφ1 : return SAT (E( U φ1))

φ is EGφ1 : return SAT(￢AF￢φ1)

φ is AFφ1 : return SATAF (φ1)

φ is AGφ1 : return SAT (￢EF￢φ1)

end case
end function

اسلاید 16 :

function SATEX (φ)
/* determines the set of states satisfying EXφ */
local var X, Y
begin
X := SAT (φ);
Y := pre∃(X);
return Y
End
The function SATEX. It computes the states satisfying φ by
calling SAT. Then, it looks backwards along→to find the states satisfying EXφ.

اسلاید 17 :

function SATAF (φ)
/* determines the set of states satisfying AFφ */
local var X, Y
begin
X := S;
Y := SAT (φ);
repeat until X = Y
begin
X := Y ;
Y := Y ∪ pre∀(Y )
end
return Y
End
The function SATAF. It computes the states satisfying φ by
calling SAT. Then, it accumulates states satisfying AFφ in the manner described in the labelling algorithm.

اسلاید 18 :

function SATEU (φ, ψ)
/* determines the set of states satisfying E[φ U ψ] */
local var W,X, Y
begin
W := SAT (φ);
X := S;
Y := SAT (ψ);
repeat until X = Y
begin
X := Y ;
Y := Y ∪ (W ∩ pre∃(Y ))
end
return Y
End
The function SATEU. It computes the states satisfying φ by
calling SAT. Then, it accumulates states satisfying E[φ U ψ] in the manner described in the labelling algorithm.

اسلاید 19 :

The LTL model-checking algorithm

در الگوریتمی که در موردCTL بیان شد، زیرفرمولهای یک فرمول در حالتهای یک سیستم ارزیابی می شد، در صورتی که در LTL این زیر فرمولها باید در مسیرهای سیستم ارزیابی شوند. به این علت الگوریتم استراتژی متفاوتی دارد .
.
استراتژی پایه :
فرض کنیدM= (S,→, L) یک مدل است و φ فرمولی در منطقLTL ، s ∈ S، تعیین می

کنیم آیا : M, s|= φ
به طوریکه آیا φ در طول همه مسیرهای M که از s شروع می شود ارضا می شود یا نه.
تمام الگوریتمهایLTL model checking از 3 گام زیر استفاده می کنند.

اسلاید 20 :

1. یک اتوماتون برای ￢φ می سازیم که با A￢φ نمایش می دهیم.
(اتوماتون مانند Aψ مثل جدولی است برای فرمول ψکه یک تریس را می پذیرد.
تریس (trace) دنباله ای از مقادیر اتمهای گزاره ای است .برای هر مسیر π :
( π |= ψ iff the trace of π is accepted by Aψ

2. اتوماتون A￢φ را با مدل M ترکیب می کنیم به این صورت که سیستم ترکیبی شامل همه مسیرهای سیستم گذار و اتوماتون است .

3. پیدا کنید که آیا مسیری که از s مشتق شده در سیستم ترکیبی وجود دارد یا نه. اگر چنین مسیری باشد این طور تعبیر می شود که مسیری ازs است که φ را ارضا نمی کند. اگر چنین مسیری نباشد خروجی ‘Yes, M, s |= φ’ است در غیر این صورت. No