کاهش فضای حالت در تکنیک بررسی مدل به کمک روش سمبولیک بهبود یافته مبتنی بر دیاگرام تصمیم گیری دودویی

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

Keywords:

تکنیک بررسی مدل , انفجار حالت , دیاگرام تصمیم گیری دودویی (BDD)