اتوماتای ترکیبی

مثالی ساده از اتوماتای ترکیبی، کنترل‌گری است که دمای یک نیروگاه هسته‌ای را کنترل می‌کند. این کنترل‌گر یک سری وضعیت مثل عادی، حاد، و غیرفعال دارد که در هر زمانی در یکی از این وضعیت‌ها قرار دارد. این سیستم یک دماسنج دارد که متناظر با یک متغیر پیوسته در اتوماتا است. با تغییر این متغیر ممکن است وضعیت سیستم تغییر کند.

اتوماتای ترکیبی H از اجزای زیر تشکیل شده‌است:

۱- متغیرها: مجموعهٔ ${\displaystyle X=\{X_1,X_2,\dots ,X_n\}}$

1. گراف کنترلی: یک گراف جهت‌دار چندگانهٔ ${\displaystyle G=(V,E)}$
   که رئوس آن «حالت‌های کنترلی» و یال‌های آن «سوییچ‌های کنترلی» نام دارند.
2. شرایط اولیه، جاری و ناوردا: سه برچسب که به هریک از راس‌ها تعلق می‌گیرد. برچسب اول، حالت اولیه است (${\displaystyle init(v)}$
   ) که تابعی است که متغیرهای آزاد آن از مجموعهٔ ${\displaystyle X}$
   می‌آید. برچسب دوم، ناوردا یا ${\displaystyle inv(v)}$
   است که همانند حالت اولیه تابعی‌ست با متغیرهای اولیه از مجموعهٔ ${\displaystyle X}$
   . برچسب سوم جریان یا ${\displaystyle flow(v)}$
   است که متغیرهای آن از مجموعهٔ ${\displaystyle X\cup \dot{X}}$
   می‌آیند.
3. شرایط پرش: برچسبی متعلق به هر یال ${\displaystyle e}$
   که به آن تابعی با متغیرهایی از ${\displaystyle X\cup \dot{X}}$
   با عنوان ${\displaystyle jump(e)}$
   نسبت می‌دهد.
4. پیشامدها: مجموعه‌ای متناهی از پیشامدها مانند ${\displaystyle \mathrm{\Sigma }}$
   و یک تابع برچسب‌گذاری مانند ${\displaystyle Event:\mathrm{\Sigma }\to E}$
   که به هر یال انتقالی گراف یک پیشامد نسبت می‌دهد.

در مثال زیر قواعد بالا را بررسی می‌کنیم:

اتوماتای ترکیبی که تصویر روبه‌رو می‌بینید یک ترموستات را مدل می‌کند. متغیر ${\displaystyle x}$

اگر ${\displaystyle H_1}$

در چک کردن مدل که بخشی از سیستم‌های تصدیق است، هدف چک کردن این موضوع به صورت سیستماتیک است که با توجه به تعریف داده‌شده از مدل و ویژگی‌های آن، آیا این ویژگی‌ها در مورد مدل صادق هستند یا خیر. یک نمونه از چنین سیستمی توسط Clarke, Sifakis و Emerson ارائه شده‌است که با کمک گرفتن از اتوماتاهای ترکیبی این کار را انجام می‌دهند. دو نمونه از قابلیت‌هایی که اتوماتاهای ترکیبی از حیث تصدیق سیستم به ما می‌دهند به شرح زیر است:

۱- قابلیت رسیدن یا ضمانت: آیا سیستم می‌تواند به حالتی برسد که دارای ویژگی ${\displaystyle p}$

۲- قابلیت امنیت: آیا سیستم می‌تواند برای همیشه در حالتی که دارای ویژگی ${\displaystyle p}$

به یک اتوماتای ترکیبی، مستطیلی گفته می‌شود هرگاه شرایط جاری مستقل از حالت‌های کنترلی باشند و متغیرها نیز دو به دو مستقل باشند. به‌طور خاص، در هر وضعیت کنترلی، مشتق اول هر یک از متغیرها دارای مجموعه‌ای از مقادیر است که این مقادیر با توجه به یال‌های گراف تغییری نمی‌کنند. با هر یال گراف یک اتوماتای مستطیلی، مقدار هریک از متغیرها یا تغییری نمی‌کند یا به صورت غیرقطعی به مقداری در یک گسترهٔ جدید تغییر می‌یابد. رفتار متغیرها جدا از هم است، چرا که به دلیل استقلالی که تعریف کردیم مقادیر متغیرها و مشتق آن‌ها نمی‌تواند وابستهٔ به یکدیگر باشد.