پياده ‏سازي يك مولد فضاي حالت نمادين براي توصيف سيسستمهاي تصادفي گسسته‌رخداد در چارچوب PDETool

Implementation of a Symbolic State Space Generator for Stochastic Discrete-Event Systems Descriptions in the PDETool Framework

بررسي مدل، يكي از مهمترين روشهاي درستي‌يابي سيستم‌هاست. يكي از مشكلات بررسي مدل، توليد فضاي حالت است و معمولاً به‌دليل بزرگ‌بودن فضاي حالت، مشكل انفجار حالت پيش مي‌آيد. دليل انفجار فضاي حالت، رشد نمايي اندازه فضاي حالت با تعداد متغيرهاي مدل است. از راهكارهاي غلبه بر اين مشكل، نگهداري فضاي حالت به‌صورت ضمني به‌جاي نگهداري صريح آن‌هاست. نگهداري فضاي حالت به‌صورت نمادين، هزينه‌ي ذخيره‌ و پردازش فضاي حالت را به مرتبه ذخيره‌سازي و پردازش گراف‌ها كاهش مي‌دهد. در اين مقاله، پياده‏سازي نويني براي توليد فضاي حالت نمادين از توصيف SDES در ابزار PDETool ارايه شده است. اين ابزار با هدف فراهم‌سازي چارچوبي يكپارچه براي مدل‌سازي و تحليل سيستم‌ها طراحي شده است و برمبناي موتور شبيه‌‌سازي SimGine و توصيف SDES عمل مي‌‌كند. درواقع، از توصيف سيستم‌هاي تصادفي گسسته رخداد (SDES) به‌عنوان صورتبندي رابط استفاده مي‌گردد كه انواع مدل‌هاي صوري به آن تبديل مي‌شوند. در اين روش، با استفاده از توليد فضاي حالت نمادين به كمك گراف تصميم دودويي مرتب كاهش‌يافته (ROBDD)، فضاي حالت بسيار بزرگتري را مي‌توان توليد و مديريت كرد؛ درنتيجه با استفاده از اين روش، تحمل‌پذيري بالاتري براي ابزار PDETool در مقابل مشكل انفجار حالت ايجاد شده است