پیادهسازی یک مولد فضای حالت نمادین برای توصیف های سیسستم های تصادفی گسسته رخداد در چارچوب PDETool

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