مقاله زمانبندی سامانه حمل و نقل ریلی با استفاده از وارسی مدل احتمالاتی

بخشی از مقاله

چکیده

در این مقاله به ارائه روشی برای زمانبندی حرکت قطارها با در نظر گرفتن احتمال تاخیر برای هر حرکت و تاثیر آن بر دیگر قطارها می-پردازیم. این روش مبتنی بر وارسی مدل احتمالاتی بوده و برای پیاده سازی آن از ابزار PRISM استفاده میکنیم. نتایج کار نشان می دهد که با استفاده از روش ارائه شده میتوانیم زمانبندی بهتری ارائه دهیم تا احتمال رخداد تاخیرهای طولانی را کمینه کنیم.

مقدمه

زمانبندی یکی از مسائل مهم در صنعت حمل و نقل ریلی است. تعیین زمان مناسب برای حرکت قطارها با در نظر گرفتن شرایط محیطی، موجب کاهش هزینه و زمان خواهد بود. به دلیل اینکه در بسیاری از مسیرها بین هر دو ایستگاه تنها یک خط وجود دارد و در هر لحظه امکان عبور حداکثر یک قطار از هر خط وجود دارد، زمان-بندی نادرست میتواند باعث ایجاد تاخیر در رسیدن قطارها به مقصد شود. از طرفی با توجه به امکان خرابی و توقف قطار در یک خط امکان تعیین زمانبندی دقیق کار دشواری است زیرا تاخیر یک قطار میتواند بر حرکت سایر قطارها در مسیر مقابل نیز تاثیر بگذارد. در نتیجه میتوان محیط حمل و نقل ریلی را یک محیط غیرقطعی در نظر گرفت.

علاوه بر این با استفاده از دادههای آماری و اطلاعات فنی میتوان احتمال وقوع خرابی برای یک قطار در هر مسیر را تخمین زد و بر این اساس احتمال رسیدن به موقع یک قطار به مقصد ونیز احتمال تاخیر در یک بازه زمانی قابل قبول را با توجه به زمانبندی حرکت قطارها به دست آورد. در این مقاله از فرایندهای تصمیم مارکوف برای مدلسازی حرکت قطارها استفاده میکنیم و روشی برای تخمین احتمال به موقع رسیدن یک قطار به مقصد را ارائه خواهیم داد.

دلیل استفاده از فرایندهای تصمیم مارکوف1 این است که با استفاده از آن میتوان مفاهیم عدم قطعیت و تغییر وضعیتهای احتمالاتی را مدل کرد. از تکنیک وارسی مدل احتمالاتی استفاده خواهیم کرد تا به محاسبه ویژگیهای مورد نظر - یعنی احتمال رسیدن به مقصد با تاخیر مورد نظر - بپردازیم و روشی ارائه میکنیم تا با استفاده از آن بتوان به یک زمانبندی بهینه رسید. برای پیاده سازی مدل مورد نظر و انجام وارسی مدل از ابزار [1] PRISM استفاده میکنیم. در ادامه مقاله ابتدا به مرور کارهای قبلی میپردازیم. سپس به تعریف فرایند تصمیم مارکوف پرداخته و مسئله مورد بحث را تعریف خواهیم کرد. پس از آن به ارائه راه حل پرداخته و نتایج کار را نمایش میدهیم. در انتها مقاله را جمع بندی کرده و نتیجه گیری را ارائه میدهیم.

مرور کارهای قبلی

مسئله زمانبندی یکی از معروفترین مسائل در حوزه علوم و مهندسی کامپیوتر است و در بسیاری از موارد به مسائلی خارج از حوزه کامپیوتر نیز میپردازد. بسته به نوع مسئله مورد نظر و شرایط محیط روشهای مختلفی برای طرح و حل آن وجود دارد. یکی از روشهایی که در چند سال اخیر مورد توجه قرار گرفته است حل مسئله زمانبندی با استفاده از تکنیکهای مبتنی بر وارسی مدل است. در این روش معمولا فرایندهای مورد نظر با استفاده از ی ک ساختار کریپکی مدل میشوند و سپس مسئله زمانبندی به فرمولی در منطق زمانی - مثل CTL یا - LTL تبدیل شده و پس از انجام وارسی مدل، یک پاسخ برای مسئله زمانبندی به دست می آید.

مهمترین کارهایی که برای حل مسئله زمانبندی با استفاده از وارسی مدل انجام شده اند عبارتند از 3]،.[2 در تمامی این مثالها از ساختارهای کریپکی و یا اتوماتای زمانی برای مدلسازی فرایندها استفاده میشود. هر چند در این روشها به خوبی میتوان مفهوم عدم قطعیت را مدل کرد اما در برخی مسائل پاسخهایی که به دست میآید تنها یک کران بالا برای زمان اجرای فرایندها را مشخص می کند. در این مقاله با در نظر گرفتن احتمال رخداد برخی مسائل - مانند احتمال خرابی و احتمال زمان لازم برای رفع خرابی - راه حلی برای مسئله زمانبندی حرکت قطارها ارائه میدهیم. بر اساس بررسی ها و دانستههای ما تا کنون پژوهشی برای زمانبندی حرکت قطار با استفاده از وارسی مدل احتمالاتی انجام نشده است. بنابر این مهمترین نوآوری این مقاله ارائه روشی مبتنی بر وارسی مدل احتمالاتی برای زمانبندی حرکت قطارها است. ضمنا استفاده از وارسی مدل احتمالاتی برای مسائل ارزیابی ریسک در حمل و نقل اخیرا مورد توجه قرار گرفته است .[4]

مروری بر وارسی مدل احتمالاتی وارسی مدل احتمالاتی یک روش راستی آزمایی2 رسمی است که برای بررسی صحت، کارایی و قابلیت اطمینان سیستمهایی با رفتارهای تصادفی و احتمالاتی استفاده میشود. در این روش از زنجیرههای مارکوف و یا انواع توسعه یافته آن مانند فرایندهای تصمیم مارکوف برای مدلسازی سیستمی با رفتار احتمالاتی استفاده میشود. ویژگی و یا ویژگیهای مورد نظر با استفاده از منطق زمانی احتمالاتی بیان شده و فرایند وارسی مدل احتمالاتی به شکل خودکار سعی در محاسبه ویژگیهای مورد نظر میکند. در این بخش به مرور تعریف فرایند تصمیم مارکوف میپردازیم. تعاریف مربوط به منطق های احتمالاتی و الگوریتمهای وارسی مدل در منابع 6]،[5 وجود دارند. همچنین PRISM به عنوان یک ابزار معروف و شناخته شده برای وارسی مدل احتمالاتی وجود دارد و تعدادی از مسائل حل شده با وارسی مدل احتمالاتی در وب سایت PRISM ارائه شدهاند .[7]

تعریف فرایند تصمیم مارکوف

یک فرایند تصمیم مارکوف یک چندتایی به صورت چندتایی , R -     M   - S, s0 ,  , تعریف میشود که در آن S مجموعهای متناهی از حالتها، s0 حالت شروع،    مجموعهای متناهی از کنش ها، Dist - S -     : S   تابع تغییر وضعیت احتمالاتی و 0    R    R : S تابع پاداش است که برای مدل کردن هزینه و یا سود یک تغییر وضعیت استفاده میشود. مجموعه کنشها برای مدل کردن رفتار غیر قطعی سیستم استفاده میشود و برای هر حالت s S زیرمجموعهای از کنشهای قابل استفاده میباشد و معمولا از Act - s - برای تعیین مجموعه کنشهای قابل استفاده در حالت s استفاده میشود. تابع تغییر وضعیت است که به ازای هر حالت و کنش، یک توزیع احتمال برای حالتهای هدف را مشخص میکند.

فرایندهای تصمیم مارکوف برای مدل کردن سیستمهایی با رفتارهای غیر قطعی و احتمالاتی به کار میرود. بر این اساس حالت شروع سیستم s0 فرض میشود. سپس سیستم یکی از کنشهای قابل استفاده را به طور غیر قطعی انتخاب و بر اساس تابع توزیع احتمال تعریف شده یکی از حالتهای بعدی را به طور تصادفی انتخاب کرده و به آن حالت وارد میشود. این فرایند به همین شکل ادامه می یابد. تعریف فرایند تصمیم مارکوف اجازه میدهد تا سیستم به طور نامتناهی تغییر وضعیت دهد. همچنین میتوان کلاسهای متفاوتی از ویژگیها را با استفاده از منطق PCTL تعریف کرده و در وارسی مدل احتمالاتی به محاسبه و بررسی این ویژگیها پرداخت. ویژگی های دسترس پذیری احتمالاتی3 دسته مهمی از این ویژگیها هستند که در آنها احتمال اینکه سیستم در نهایت به برخی حالتهای خاص وارد شود مورد بررسی قرار میگیرد.

بیان مسئله

مسئله مورد بررسی در این مقاله زمانبندی حرکت قطارها در مسیرهای تک خطی است. همان طور که شکل 1 نشان می دهد در این مسئله فرض میکنیم دو ایستگاه مبدا و مقصد و تعدادی ایستگاه شکل -1 شمای ساده شده مسیر حرکت قطارها بین راهی وجود دارد به شکلی که هر قطار زمانی میتواند وارد یک خط شود که قطار دیگری در همان خط در حال عبور نباشد. در غیر این صورت قطار باید در ایستگاه توقف کند تا خط مربوطه آزاد شود و در نتیجه تاخیری در زمان رسیدن قطار به وجود میآید.

در حالت ایدهآل میتوان حرکت قطارها را طوری زمانبندی کرد که در هر لحظه حداکثر یک درخواست برای ورود به هر خط وجود داشته باشد. به عنوان مثال در شکل 1 قطار t2 با داشتن زمان حرکت قطار t1 و زمان لازم برای پیمودن فاصله بین ایستگاهها میتواند زمان ورود t1 به ایستگاه B را محاسبه و براساس آن در لحظه مناسب حرکت خود را آغاز کند. در این صورت هر دو قطار هم زمان به ایستگاه B رسیده و بدون مشکل و تاخیر به حرکت خود ادامه می دهند.

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

نکته مهمی که در این مسئله وجود دارد انتشار تاخیر پیش آمده برای یک قطار در میان قطارهای دیگر است. در واقع به دنبال ارائه یک زمان بندی مناسب هستیم تا احتمال انتشار تاخیرها را کمینه کند. با توجه به احتمال خرابی هر یک از قطارها ارائه راه حلی که زمان تاخیرها را صفر کند در عمل غیر ممکن است. بنابراین با در نظر گرفتن مقادیر مجاز برای تاخیرها سعی میکنیم زمانبندی را به شکلی انجام دهیم تا احتمال رسیدن قطارها در بازه تاخیر مجاز بیشینه شود.

راه حل پیشنهادی

محیط مسئله شامل ایستگاههای مبدا و مقصد و ایستگاههای بین راهی و خطوط ریلی بین ایستگاهها با فواصل مشخص را با فرایندهای تصمیم مارکوف مدل میکنیم. این مدلسازی را در ابزار PRISM انجام میدهیم. سپس با استفاده از این ابزار به محاسبه احتمال رسیدن قطارها به مقصد با در نظر گرفتن مقادیر مشخصی از تاخیر زمانی میپردازیم. در این مسئله دو نوع عدم قطعیت را در نظر داریم: شروع حرکت از ایستگاه مبدا را به طور غیر قطعی مشخص میکنیم.

در واقع با در نظر گرفتن زمان صفر برای حرکت قطار اول، زمان حرکت قطارهای دیگر را - به شکل غیر قطعی - طوری انتخاب می کنیم که احتمال رسیدن قطارها به مقصد در بازه تاخیر مجاز بیشینه شود. در واقع این انتخابهای غیر قطعی راه حل نهایی برای مسئله زمانبندی را میدهد. باید دقت کرد که مسئله زمانبندی قبل از حرکت قطارها باید حل شود و منظور ما حل مسئله به صورت پویا و در زمان حرکت قطارها نیست. با توجه به محدودیتهایی که ابزارهای وارسی مدل دارند از جمله مسئله انفجار حالات[ 7] 4 برای حل کارای مسئله باید چند مورد را برای ساده سازی در نظر گرفت:

-1 برای سادهتر شدن مسئله به جای در نظر گرفتن فاصله بین ایستگاهها، زمان لازم برای عبور قطار از هر خط را در نظر میگیریم.

-2 هر ده دقیقه زمان لازم برای عبور قطار را به عنوان یک واحد زمانی در نظر میگیریم. به عنوان مثال فاصله بین ایستگاه مبدا تا ایستگاه A در شکل 1 را برابر 7 واحد زمانی در نظر میگیریم.

-3 هر قطار در هر ایستگاه بین راهی بین ده تا بیست دقیقه توقف خواهد داشت. در صورتی که خط مقابل توسط قطار دیگری در حال استفاده باشد قطار نخست مجبور است در ایستگاه منتظر بماند تا قطار دوم از خط خارج شود.

-4 احتمال خرابی هر قطار در هر واحد زمانی را دو درصد در نظر میگیریم. هر چند در عمل این احتمال میتواند با یک تحلیل فنی و آمار به شکل دقیقتر محاسبه شود. ضمنا در صورت وقوع خرابی بین ده تا بیست دقیقه زمان برای تعمیر قطار در نظر گرفته میشود. برای سادگی فرض میکنیم یک قطار در صورت تعمیر تا پایان آن خط دچار خرابی مجدد نمیشود.

-5 در این مقاله و به دلیل محدودیت فضای نوشتاری تنها تعداد دو قطار را در نظر میگیریم. هر چند این تعداد را میتوان به تعداد بیشتری هم بسط داد - با این فرضیات و با محدودیتهای حافظه مصرفی تا تعداد 6 قطار را میتوان مدلسازی کرد - . فاصله بین مبدا و ایستگاه A را برابر 6 واحد، فاصله بین A و B برابر 7 واحد و فاصله بین B و مقصد برابر 8 واحد در نظر گرفتهایم.

ارائه مدل مربوط به حرکت قطارها در PRISM

در این بخش به شرح مدل مربوطه در PRISM میپردازیم. جزئیات این مدل در پیوست 1 آمده و قابل اجرا و بررسی است. در ابزار PRISM هر فرایند تصمیم مارکوف با تعداد ماژول تعریف میشود. هر ماژول دارای تعدادی متغیر است که در مجموع حالت-های مدل را مشخص میکنند. در این مسئله برای هر قطار یک ماژول تعریف میکنیم که شامل سه متغیر میباشد:

-1 متغیر : loc برای ثبت موقعیت کنونی قطار: اگر قطار در 

-2 مبدا باشد مقدار loc برابر صفر، اگر در ایستگاه A باشد مقدار آن 7 و اگر در ایستگاه B باشد مقدار آن 15 و نهایتا اگر در مقصد باشد مقدار آن 24 فرض میشود. مثلا اگر مقدار loc برابر 5 باشد به این معنی است که قطار مورد نظر 5 واحد زمانی از مسیر را پشت سر گذاشته است.

-3 متغیر : delay مقدار تاخیری را که قطار پس از شروع حرکت داشته است نشان میدهد. این مقدار در ابتدا صفر است و هدف مسئله زمانبندی حرکتها به شکلی است که این مقدار کمینه باشد.

-4 متغیر : stat اگر قطار سالم باشد و در این خط تعمیر نشده باشد مقدار صفر، اگر در حال تعمیر باشد مقدار یک و اگر قبلا در همین خط تعمیر شده مقدار دو میگیرد. با توجه به اینکه در این مقاله تنها حرکت دو قطار را در نظر گرفته-ایم نام متغیرها را به شکل loc 1, delay1, stat1 برای قطار نخست و loc2، delay2 ، stat2 برای قطار دوم انتخاب میکنیم. ضمنا برای قطار دوم - که از راست به چپ حرکت میکند - loc2 مقادیر قرینه نسبت به قطار نخست دارد یعنی وقتی قطار دوم در ایستگاه سمت راست قرار دارد مقدار loc2 برابر صفر فرض میشود. وقتی وارد خط نخست میشود و به سمت B حرکت میکند مقدار loc2 بین 1 تا 8 تغییر میکند. این مقادیر معادل مقادیر 16 تا 23 برای قطار نخست - با حرکت از چپ به راست - است.

دستورات PRISM به شکلی است که ابتدا یک شرط بررسی میشود و در صورت برقراری آن تغییر وضعیت انجام میشود. به عنوان مثال ماژول train 1 به شرطی شروع به حرکت میکند که ابتدا در loc1 قرار داشته و ضمنا خط اول آزاد باشد یعنی قطار دوم در این خط نباشد. این موضوع با شرط loc 2 <= 17 بررسی میشود - چون مقادیر loc2 قرینه مقادیر loc1 هستند - . از طرف دیگر اگر قطار درایستگاه مبدا باشد و خط آزاد نباشد - مقدار loc2 بین 18 و 23 باشد - آنگاه قطار باید صبر کند و در هر گام یک واحد به میزان تاخیر افزوده میشود. برای همگامسازی حرکتهای بین دو قطار از کنش q استفاده کردهایم.

این انتخاب باعث میشود در مقابل هر حرکت قطار نخست یک حرکت از قطار دوم داشته باشیم و بالعکس. تنها استثنا هنگام ورود به خط است که برای جلوگیری از ورود همزمان دو قطار کنشی را برای این حرکت انتخاب نکردهایم. در واقع معناشناسی PRISM در این مورد به ما کمک میکند تا حل مسئله انحصار متقابل را به سادگی در مدل وارد نماییم. ضمنا فرض میکنیم ترک ایستگاه با ورود به خط همزمان اتفاق میافتد.

مدل کردن خرابی با احتمال 2 درصد در هر واحد زمانی با تغییر متغیر stat به مقدار یک و عدم افزایش loc اتفاق میافتد - قطار خراب حرکت نمیکند! - . سپس قطار پس از گذشت یک یا دو یا سه واحد زمانی با توزیع احتمالهای مشخص به حرکت خود ادامه میدهد. در این مدلسازی فرض کردهایم که توقف قطار در هر ایستگاه - بسته به شرایط محیط - باعث وقوع تاخیر به اندازه یک یا دو واحد زمانی می-شود.