استدلال خودکار: بررسی مدل نمادین

دوره Automated Reasoning: Symbolic Model Checking نشان می‌دهد که چگونه می‌توان ویژگی‌های سیستم‌ها و برنامه‌های فعال را به‌طور خودکار تأیید کرد. مفهوم اصلی یک سیستم انتقال است: هر سیستمی که بتوان آن را با حالت ها و مراحل توصیف کرد. ما ارائه می کنیم که چگونه در CTL (منطق درخت محاسباتی) ویژگی هایی مانند قابلیت دسترسی را می توان توصیف کرد. به طور معمول، یک فضای حالت ممکن است بسیار بزرگ باشد. یکی از راه‌های مقابله با این موضوع، بررسی مدل نمادین است: راهی که در آن مجموعه‌ای از حالت‌ها به صورت نمادین نمایش داده می‌شوند. یک راه مفید برای انجام این کار، نمایش مجموعه ای از حالت ها توسط BDD ها (نمودار تصمیم گیری دودویی) است. در این دوره تعاریف و ویژگی های اولیه BDD ها و الگوریتم های محاسبه آن ها در صورت نیاز برای بررسی مدل CTL ارائه شده است.