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

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