‫تسریع‬‫ وارسی‬ ‫مدل‬ ‫آماری‬ ‫با‬ ‫استفاده‬ ‫از‬ ‫رگرسیون‬ ‫خطی‬

‫وارسی‬‫ مدل‬ ‫آماری‬ ‫یکی‬ ‫از‬ ‫روش‬ ‫های‬‫ راستی‬ ‫آزمایی‬ ‫رسمی‬ ‫سیستم‬ ‫های‬‫ کامپیوتری‬ ‫است‪.‬‬ ‫این‬ ‫روش‬ ‫معمولا‬ ‫از‬ ‫زنجیره‬ ‫های‬‫ م‬ ارکوف‬‫برای مدلسازی‬‫ رفتار‬ ‫سیستم‬ ‫استفاده‬ ‫می‬ ‫کند‪.‬‬‫ ضمنا‬ ‫از‬ ‫یک‬ ‫منطق‬ ‫زمانی‬ ‫احتمالاتی‬ ‫برای‬ ‫توصیف‬ ‫ویژگی‬ ‫های‬‫ مورد‬ ‫نظر‬ ‫بهره‬ ‫گی‬‫ری‬‫ می‬ ‫شود‪.‬‬‫سپس یک‬‫ شبیه‬ ‫سازی‬ ‫شامل‬ ‫م‬ سیرهایی‬‫از‬ ‫حالت‬ ‫های‬‫ سیستم‬ ‫در‬ ‫مدل‬ ‫مورد‬ ‫نظر‬ ‫اجرا‬ ‫می‬ ‫شود‪ .‬‬‫نهایتا‬ ‫با‬ ‫بررسی‬ ‫آماری‬ ‫مسیرهای‬ ‫اجرا‬ ‫شده‬ ‫در طی‬‫ اجراهای‬ ‫شبیه‬ ‫سازی‪،‬‬ ‫یک‬ ‫معیار‬ ‫کمی‬ ‫برای‬ ‫ویژگی‬ ‫احتمالاتی‬ ‫مورد‬ ‫نظر‬ ‫ارائه‬ ‫می‬ ‫شود‪ .‬‬‫وارسی‬ ‫مدل‬ ‫آماری‬ ‫نیازمند‬ ‫ت‬میم‬‫گیری‬‫ بر‬ ‫ای خاتمه‬‫ هر‬ ‫یک‬ ‫از‬ ‫مسیرها‬ ‫در‬ ‫طی‬ ‫شبیه‬ ‫سازی‬ ‫ه‬‫ای‬‫ مورد‬ ‫نظر‬ ‫است‪.‬‬ ‫یک‬ ‫مسیر‬ ‫زمانی‬ ‫خاتمه‬ ‫می‬ ‫یابد‬‫که‬ ‫به‬ ‫یکی‬ ‫از‬ ‫حالت‬ ‫های‬‫ هدف‬ ‫تعریف‬ شده‬‫ در‬ ‫مدل‬ ‫برسد‬ ‫و‬ ‫یا‬ ‫به‬ ‫وضعیتی‬ ‫برسد‬ ‫که‬ ‫هیچ‬ ‫راهی‬ ‫برای‬ ‫رسیدن‬ ‫به‬ ‫یک‬ ‫حالت‬ ‫هدف‬ ‫وجود‬ ‫ندارد‪.‬‬ ‫تعیین‬ ‫وضعیت‬ ‫دوم‬ ‫یعنی رسیدن‬ ‫به حالتی‬‫که‬ ‫در‬ ‫آن‬ ‫هیچ‬ ‫مسیری‬ ‫برای‬ ‫رسیدن‬ ‫به‬ ‫یک‬ ‫حالت‬ ‫هدف‬ ‫وجود‬ ‫ندارد‪،‬‬ ‫یک‬ ‫مساله‬ ‫چالش‬ ‫برانگیز‬ ‫است‬ ‫که‬ ‫راه‬ ‫حل‬ ‫ساده‬ ‫ا‬‫ی‬‫ ندارد‪.‬‬ ‫در این‬‫ مقاله‬ ‫یک‬ ‫روش‬ ‫جدید‬ ‫برای‬ ‫تصمیم‬ ‫گیری‬ ‫در‬ ‫مورد‬ ‫خاتمه‬ ‫مسیرهای‬ ‫مورد‬ ‫اجرا‬ ‫در‬ ‫یک‬ ‫شبیه‬ ‫سازی‬ ‫ارائه‬ ‫می‬ ‫شود‪ .‬‬‫در‬ ‫این‬‫ روش‬ ‫ابتدا‬ تعدادی‬‫نمونه‬ ‫کوچک‬ ‫مقیاس‬ ‫از‬ ‫مدل‬ ‫مساله‬ ‫اصلی‬ ‫در‬ ‫نظر‬ ‫گرفته‬ ‫شده‬ ‫و‬ ‫برای‬ ‫آنها‬ ‫مجموعه‬ ‫ای‬‫ از‬ ‫مسیرهای‬‫ شبیه‬ ‫سازی‬ ‫اجرا‬‫می‬ ‫شود‪.‬‬ ‫میانگین‬‫ و‬ ‫انحراف‬ ‫معیار‬ ‫طول‬ ‫مسیرها‬ ‫برای‬ ‫نمونه‬ ‫های‬‫ کوچک‬ ‫در‬ ‫نظر‬ ‫گرفته‬ ‫شده‬ ‫و‬ ‫با‬ ‫اعمال‬ ‫رگرسیون‬ ‫خطی‪،‬‬ ‫یک‬ ‫تقریب‬ ‫با‬‫ضریب اطمینان‬‫ بالا ‫برای‬ ‫طول‬ ‫مسیرهای‬ ‫شبیه‬ ‫سازی‬ ‫مدل‬ ‫مساله‬ ‫اصلی‬ ‫ارائه‬ ‫می‬ ‫شود‪ .‬‬‫نتایج‬ ‫تجربی‬ ‫نشان‬ ‫می‬ ‫دهد‬‫ روش‬ ‫ارائه‬ ‫شده‬‫ زمان‬ ‫مصرفی وارسی‬‫ مدل‬ ‫آماری‬ ‫را‬ ‫کاهش‬ ‫می‬ ‫دهد‪.‬‬