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

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

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

مثال

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

تعریف ریاضی مدل

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

۱- متغیرها: مجموعهٔ $X=\{X_{1},X_{2},\ldots ,X_{n}\}$از متغیرهای حقیقی. به عدد $n$بعد اتوماتا گفته می‌شود. مجموعهٔ ${\dot {X}}=\{{\dot {X}}_{1},{\dot {X}}_{2},\ldots ,{\dot {X}}_{n}\}$نشان‌دهندهٔ مشتق متغیرها در هنگام تغییر است و مجموعهٔ $X'=\{X'_{1},\ldots ,X'_{n}\}$نشان‌دهندهٔ مقدار متغیرها هنگام یک تغییر گسسته‌است.

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

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

یک اتوماتای ترکیبی- تصویر ۱

اتوماتای ترکیبی که تصویر روبه‌رو می‌بینید یک ترموستات را مدل می‌کند. متغیر $x$نشانگر دما است. در حالت کنترلی خاموش، گرم‌کننده خاموش است، و دما با توجه به شرط جاری ${\dot {x}}=-2x$سقوط می‌کند. در حالت کنترلی روشن، گرم‌کننده روشن است و دما با توجه به شرط جاری ${\dot {x}}=-x$زیاد می‌شود. در ابتدا گرم‌کننده خاموش است و دما ۳۵٫۲ درجه است. با توجه به شرط پرش $x<35.5$، در لحظه‌ای که دما به زیر ۳۵٫۵ درجه برود، گرم‌کننده ممکن است روشن شود. با توجه به شرط ناوردای $x\geq 35$دیرترین زمانی که ممکن است گرم‌کننده روشن شود زمانی است که دما به ۳۵ برسد.

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

اگر $H_{1}$و $H_{2}$دو عدد اتوماتای هیبریدی باشند، منظور از $H_{1}||H_{2}$ترکیب این دو اتوماتا است. این دو اتوماتا توسط پیشامدهای مشترکشان تعامل می‌کنند. اگر پیشامد $a$میان $H_{1}$و $H_{2}$مشترک باشد، آنگاه این دو اتوماتا باید در هنگام گذر از این یال در گراف اتوماتاها هماهنگ باشند.

کاربرد اتوماتای ترکیبی در سیستم‌های تصدیق

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

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

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

اتوماتای مستطیلی

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