اتوماتون زمانی

اتوماتون زمانی در نظریه ماشین‌های خودکار (اتوماتون)، اتوماتون زمانی به یک حالت توسعه یافته از ماشین حالت متناهی گفته می‌شود که در آن، مجموعه ورودی‌ها با کلاک ساعت واقعی به ماشین داده می‌شود. در اجرای یک سیستم مبتنی بر اتوماتون زمانی، کلاک ساعت سیستم با روندی یکسان افزایش میابد. مقدار عددی این کلاک ساعت‌ها، عددی صحیح می‌باشد. واحد کنترلی وجود دارد که مقادیر این کلاک ساعت را کنترل می‌کند و با افزایش ویا کاهش آن می‌تواند در دریافت ورودی، محدودیت ایجاد کند. ازآن گذشته می‌تواند کلاک ساعت را بازنشانی مجدد کند. اتوماتون زمانی زیرمجموعه اتوماتون ترتیبی قرار میگید. اتوماتون زمانی کاربردهای گوناگونی در مدلسازی و تحلیل رفتارهای زمانبندی شده سیستم‌های رایانه ای از جمله شبکه‌ها و سیستم‌های بیدرنگ دارد. در طول ۲۰ سال گذشته پژوهش‌های بسیاری بر روی کنترل خواص ایمنی در سیستم‌ها و درست کارکرد آن‌ها انجام شده‌است. ثابت می‌شود که مشکل دسترسی به وضعیت معتبر برای اتوماتون‌های زمانی، قابل حل است. از این رو پژوهش‌های بسیاری انجام شده‌است که می‌توان در میان آن‌ها به stopwatches, real-time tasks, cost functions و timed games اشاره کرد. ابزار گوناگونی هم برای ورودی‌ها به یک اتوماتون زمانی و تحیل آن وجود دارد که می‌توان به مدل کنترلی UPPAAL, Kronos، و مدل TIMES که بر اساس تجزیه و تحلیل زمانی است، اشاره نمود. این ابزار در حال توسعه روز به روز تا رسیدن به فاز صنعتی هستند ولی امروزه هنوز ابزاری دانشگاهی به‌شمار می‌آیند.

تعریف رسمی

یک اتوماتون زمانی تاپلی به شکل (A = (Q,Σ,C,E,q0 می‌باشد که شامل اجزای زیر است:

• Q یک مجموعه متناهی است. به عناصری که در Q است، حالات سیستم A می‌گویند.
• Σ یک مجموعه متناهی به نام الفبا می‌باشد که عناصر آن اعمال قابل اجرا در A می‌باشد.
• C یک مجموعه متناهی است که به کلاک ساعت A می‌شناسند.
• E ⊆ Q×Σ×B(C)×P(C)×Q مجموعه‌ای گذرا از A است که:
  • (B(C مجموعه‌ای از نوع داده بولی شامل ساعت‌هایی از C است.
  • (P(C هم توانی از C می‌باشد.
• q₀ هم متغیری از Q می‌باشد که به متغیر حالت نخستین شناخته می‌شود.

عبارت ('q,a,g,r,q) بیانگر حالتی گذرا از E است که در آن با عمل a، کنترل g از حالت q به 'q رفته و کلاک ساعت را به r تنظیم می‌کنیم.