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

بررسی مدل، یکی از مهمترین روشهای درستی‌یابی سیستم‌هاست. یکی از مشکلات بررسی مدل، تولید فضای حالت است و معمولاً به‌دلیل بزرگ‌بودن فضای حالت، مشکل انفجار حالت پیش می‌آید. دلیل انفجار فضای حالت، رشد نمایی اندازه فضای حالت با تعداد متغیرهای مدل است. از راهکارهای غلبه بر این مشکل، نگهداری فضای حالت به‌صورت ضمنی به‌جای نگهداری صریح آن‌هاست. نگهداری فضای حالت به‌صورت نمادین، هزینه‌ی ذخیره‌ و پردازش فضای حالت را به مرتبه ذخیره‌سازی و پردازش گراف‌ها کاهش می‌دهد.در این مقاله، پیاده‏سازی نوینی برای تولید فضای حالت نمادین از توصیف sdes در ابزار pdetool ارایه شده است. این ابزار با هدف فراهم‌سازی چارچوبی یکپارچه برای مدل‌سازی و تحلیل سیستم‌ها طراحی شده است و برمبنای موتور شبیه‌‌سازی simgine و توصیف sdes عمل می‌‌کند. درواقع، از توصیف سیستم‌های تصادفی گسسته رخداد (sdes) به‌عنوان صورتبندی رابط استفاده می‌گردد که انواع مدل‌های صوری به آن تبدیل می‌شوند. در این روش، با استفاده از تولید فضای حالت نمادین به کمک گراف تصمیم دودویی مرتب کاهش‌یافته (robdd)، فضای حالت بسیار بزرگتری را می‌توان تولید و مدیریت کرد؛ درنتیجه با استفاده از این روش، تحمل‌پذیری بالاتری برای ابزار pdetool در مقابل مشکل انفجار حالت ایجاد شده است