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

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

خودکارهای بررشته های نامتناهی، منطقهای زمانی، توصیف صوری