محمد ایزدی - دانشکده مهندسی کامپیوتر دانشگاه صنعتی شریف
علی موقر - دانشکده مهندسی کامپیوتر دانشگاه صنعتی شریف

در این مقاله ضمن توصیف مساله وارسی الگو در اعتبار سنجی سیستم های کامپیوتری، منطق زمانی نقطه ثابت یا حساب Mu ارائه شده، نحوه توصیف ویژگیهای سیستم در آن بررسی و الگوریتمهای مختلف درستی یابی ویژگیهای توصیف شده در حساب Mu دسته بندی و برخی از آنها بیان می شوند و از نظر مرتبه پیچیدگی بررسی می شوند . پیشنهاد مشخص این مقاله استفاده از روش مشخص سازی فرمولهای حساب Mu توسط خودکاره های بازگشتی مرتبه اول که به عنوان توسیع نظریه خودکاره های بوچی و رابین ارایه شده اند و سپس حل مساله وارسی الگو در ارتباط میان خودکاره توصیف کننده ویژگی لازم سیستم و مدل کریپکیایی سیستم است .

وارسی الگو(Model checking) ، درستی یابی سیستم های کامپیوتری ، (Verification of Computer Systems) ، حساب (Mu-Calculus) Mu ، منطقهای زمانی نقطه ثابت (Fixpoint Temporal Logics) ، نظریه خودکاره ها(Automata Theory)