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

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

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