شهدت السنوات الأخيرة اهتماماً متزايداً بتعريف نماذج لآلات متحكِّمة مُدعَّمة بمفهوم الزمن. فعلى سبيل المثال، تم تقديم الآلات الزمنية باعتبارها آلاتاً مُوسَّعة بساعات زمنية. في هذا البحث ندرس نماذج من آلات الحالات المحدودة الزمنية (TFSMs)، أي آلات الحالات المحدودة المُدعَّمة بالزمن، التي تقبل كلمات إدخال زمنية وتُنتج كلمات إخراج زمنية. نناقش هنا بعض نماذج آلات الحالات المحدودة الزمنية ذات ساعة واحدة: الآلات ذات الحُرّاس الزمنيين، والآلات ذات المُهَل (Timeouts)، والآلات التي تجمع بين الحُرّاس والمُهَل. نقوم بحل مسألة التحقُّق من التكافؤ لجميع النماذج الثلاثة، ونقارن بين قوّة تعبيرها، ونحدّد الفئات الفرعية من الآلات ذات الحُرّاس وتلك ذات المُهَل التي تكون متكافئة مع بعضها.
تُعدّ الآلات المحدودة (FA) وآلات الحالات المحدودة (FSMs) نماذج شكلية واسعة الاستخدام في الهندسة والعلوم، على سبيل المثال في مجالات تتراوح بين الدوائر التسلسلية، وبروتوكولات الاتصال، والأنظمة المدمجة والتفاعلية، إلى النمذجة الحيوية.
منذ تسعينيات القرن الماضي، أُثريت الفئات القياسية للآلات المحدودة بإدخال قيود زمنية لتمثيل سلوك الأنظمة في الزمن المتقطّع أو المستمرّ بدقّة أكبر. وتُعدّ الآلات الزمنية (TA) مثالاً على ذلك: فهي آلات محدودة مُدعَّمة بعدد من الساعات الزمنية الحقيقية القابلة لإعادة الضبط، حيث تُفعَّل الانتقالات بناءً على شروط تتعلّق بقيم الساعات .
ومؤخّراً، اقتُرحت نماذج زمنية لآلات الحالات المحدودة في الأدبيات عبر إدخال قيود زمنية مثل الحُرّاس الزمنيين أو المُهَل. فالحُرّاس الزمنيون يقيّدون انتقالات الإدخال/الإخراج لتحدث ضمن فترات زمنية معيّنة. على وجه الخصوص، يتميّز نموذج آلة الحالات المحدودة الزمنية المقترح في بما يلي: ساعة واحدة، وقيود زمنية تحدّد الزمن المنقضي في الحالة، وإعادة ضبط الساعة عند تنفيذ الانتقال.
أمّا نموذج آلة الحالات المحدودة الزمنية المقترح في فيتميّز بوجود ساعة واحدة، وقيود زمنية لتحديد الزمن المنقضي عند الحاجة لإنتاج إخراج بعد تطبيق إدخال على الآلة، وإعادة ضبط الساعة عند إنتاج الإخراج، بالإضافة إلى المُهَل. ومعنى المُهلة هو: إذا لم يُطبَّق أي إدخال في الحالة الحالية خلال فترة المُهلة، تنتقل الآلة من الحالة الحالية إلى حالة أخرى وفق دالة المُهلة؛ والمُهَل شائعة في بروتوكولات وأنظمة الاتصالات.
تُستخدم الآلات الزمنية وآلات الحالات المحدودة الزمنية أيضاً عند اشتقاق اختبارات للأنظمة الحدثية المتقطّعة. ومع ذلك، فإن طرائق اشتقاق مجموعات اختبارات منتهية وكاملة مع ضمان تغطية الأخطاء متاحة عملياً لآلات الحالات المحدودة الزمنية، ولذلك تُفضَّل هذه الآلات على الآلات الزمنية وغيرها من النماذج عندما يكون اشتقاق اختبارات كاملة مطلوباً.
في هذا البحث، ندرس نماذج من آلات الحالات المحدودة الزمنية ذات ساعة واحدة: الآلات ذات الحُرّاس الزمنيين فقط، والآلات ذات المُهَل فقط، والآلات التي تجمع بين الحُرّاس والمُهَل. نقوم بحل مسألة التحقُّق من التكافؤ لجميع النماذج الثلاثة، ونقارن بين قوّة تعبيرها، ونُحدِّد الفئات الفرعية من الآلات ذات الحُرّاس وتلك ذات المُهَل التي تكون متكافئة مع بعضها. وقد حُصّلت هذه النتائج عبر تقديم علاقات محاكاة متبادلة (bisimulation) تُعرِّف آلات حالات محدودة غير زمنية تتضمّن حالاتُها معلومات عن مناطق الساعة. وهذا يذكّر ببناء رسم المناطق (region graph) المستخدم لإثبات أن مسائل التحقُّق في الآلات الزمنية (مثل خصائص الأمان) لها نفس الإجابة لجميع قيَم الساعة ضمن المنطقة نفسها . أمّا في حالتنا فنُثبت نتيجة أقوى: سلوكا آلتين زمنيتين متكافئان إذا وفقط إذا كان سلوك الآلتين غير الزمنيتين المرافقتين متكافئاً. وهكذا، تُحقّق نماذجنا من آلات الحالات المحدودة الزمنية توازناً جيّداً بين قوّة التعبير والتعقيد الحسابي.
لْتَكُن \(A\) أبجدية منتهية، ولْتكن \(\mathbb{R}^+\) مجموعة الأعداد الحقيقية غير السالبة. يُسمّى الرمز الزمني زوجاً \((a,t)\) حيث \(t \in \mathbb{R}^+\) هو الطابع الزمني للرمز \(a\in A\). وتُعرَّف الكلمة الزمنية بأنها تسلسل منتهٍ \((a_1,t_1)(a_2,t_2)(a_3,t_3)\dots\) من الرموز الزمنية حيث يكون تسلسل الطوابع الزمنية \(t_1,t_2,t_3,\dots\) متزايداً (غير تناقصي). جميع النماذج الزمنية المدروسة هنا هي آلات إدخال/إخراج تقرأ كلمة إدخال زمنية \((i_1,t_1)(i_2,t_2)\dots(i_k,t_k)\) معرفة على أبجدية إدخال \(I\)، وتُنتج كلمة إخراج زمنية مقابلة \((o_1,t_1)(o_2,t_2)\dots(o_k,t_k)\) على أبجدية إخراج \(O\). يُفترض أن إنتاج الإخراجات لحظي؛ أي إن الطابع الزمني للإخراج \(o_j\) هو نفسه طابع الإدخال \(i_j\). النماذج التي يوجد فيها تأخير بين قراءة الإدخال وإنتاج الإخراج ممكنة ولكنها غير مدروسة هنا. وإذا أُعطيت كلمة زمنية \((a_1,t_1)(a_2,t_2)\dots(a_k,t_k)\)، فإن \(\mathop{\mathrm{Untime}}((a_1,t_1)(a_2,t_2)\dots(a_k,t_k)) = a_1 a_2 \dots a_k\) تمثّل الكلمة الناتجة بعد حذف الطوابع الزمنية.
آلة الحالات المحدودة الزمنية (TFSM) قد تكون غير حتمية وجزئية، وهي آلة حالات محدودة مُدعَّمة بساعة زمنية. الساعة عدد حقيقي يقيس التأخير الزمني في الحالة، وتُعاد إلى الصفر عند تنفيذ الانتقال. في هذا القسم نعرض أولاً نموذج آلة الحالات المحدودة الزمنية ذات الحُرّاس الزمنيين كما في ونموذج الآلة ذات المُهَل كما في . ثم نُعرِّف نموذجاً يجمع بين الحُرّاس والمُهَل ويحتوي النماذج الأخرى. بالإضافة إلى ذلك، ندرس مسألة التكافؤ لكل من النماذج الثلاثة.
يُعرّف الحارس الزمني الفترة الزمنية التي يمكن فيها تنفيذ الانتقال. بصورة حدسية، إذا كانت الآلة في الحالة \(s\) وتستقبل الإدخال \(i\) عند زمن \(t\) يحقّق الحارس الزمني، فإنها تستجيب بالإخراج \(o\) وتنتقل إلى الحالة التالية \(s'\)، مع إعادة ضبط الساعة إلى الصفر وبدء تقدّمها في الحالة \(s'\).
تعريف 1 (TFSM مع الحُرّاس الزمنيين ). TFSM مع الحُرّاس الزمنيين هو خماسية \(M = (S, I, O, \lambda_S, s_0)\) حيث \(S\) و\(I\) و\(O\) مجموعات منتهية، منفصلة، وغير فارغة للحالات والإدخالات والإخراجات على التوالي، و\(s_0\) هي الحالة الابتدائية، و\(\lambda_S \subseteq S \times I \times \Pi \times O \times S\) علاقة الانتقال حيث \(\Pi\) هي مجموعة الحُرّاس الزمنيين للإدخال. كل حارس في \(\Pi\) هو فترة \(g = \langle t_{min}, t_{max} \rangle\) حيث \(t_{min}\) عددٌ صحيحٌ غيرُ سالب، و\(t_{max}\) إمّا عددٌ صحيحٌ غيرُ سالب أو \(\infty\)، مع \(t_{min} \leq t_{max}\)، و\(\langle \in \{ (, [ \}\) بينما \(\rangle \in \{ ), ] \}\).
الحالة الزمنية للآلة هي زوج \((s,x)\) حيث \(s \in S\) حالة من \(M\) و\(x \in \mathbb{R}^+\) هو القيمة الحالية للساعة. الانتقالات بين الحالات الزمنية نوعان:
المسار الزمني لآلة الحالات المحدودة الزمنية ذات الحُرّاس \(M\) يتناوب بين الانتقالات الزمنية وانتقالات الإدخال/الإخراج. إذا أُعطيت كلمة إدخال زمنية \(v = (i_1,t_1)(i_2,t_2)\dots(i_k,t_k)\)، فإن المسار الزمني لـ\(M\) على \(v\) هو التسلسل المنتهي
\(\rho = (s_0,0) \xrightarrow{t_1} (s_0,t_1) \xrightarrow{i_1,o_1} (s_1,0) \xrightarrow{t_2-t_1} (s_1,t_2-t_1) \xrightarrow{i_2,o_2} (s_2,0) \xrightarrow{t_3-t_2} \dots \xrightarrow{i_k,o_k} (s_k,0)\)
بحيث \(s_0\) هي الحالة الابتدائية، ونعرّف \(t_0 := 0\)، ولكل \(j \geq 0\) يكون \((s_j,0) \xrightarrow{t_{j+1}-t_j} (s_j,t_{j+1}-t_j) \xrightarrow{i_{j+1},o_{j+1}} (s_{j+1},0)\) تسلسلاً صحيحاً من الانتقالات. نقول إن المسار الزمني \(\rho\) يقبل كلمة الإدخال الزمنية \(v= (i_1,t_1)(i_2,t_2)\dots(i_k,t_k)\) ويُنتج كلمة الإخراج الزمنية \(u = (o_1,t_1)(o_2,t_2)\dots(o_k,t_k)\). ويُعرَّف سلوك \(M\) من خلال كلمات الإدخال/الإخراج التي تقبلها وتنتجها الآلة.
تعريف 2. سلوك آلة الحالات المحدودة الزمنية \(M\) هو دالة جزئية \(B_M: (I\times \mathbb{R}^+)^* \mapsto 2^{(O\times \mathbb{R}^+)^*}\) تربط كل كلمة إدخال \(w\) مقبولة من \(M\) بمجموعة كلمات الإخراج \(B_M(w)\) التي تُنتجها \(M\) تحت الإدخال \(w\). إذا كانت \(M\) آلة غير زمنية، يُعرّف السلوك كدالة جزئية \(B_M: I^* \mapsto 2^{O^*}\).
تُعدّ آلتان \(M\) و\(M'\) لهما نفس أبجديات الإدخال والإخراج متكافئتَيْن إذا وفقط إذا كان لهما نفس السلوك، أي \(B_M = B_{M'}\).
يمكن تعميم التعاريف المعتادة للآلات المحدودة (الحتمية، غير الحتمية، الجزئية، إلخ) على جميع نماذج آلات الحالات المحدودة الزمنية المدروسة هنا. على وجه الخصوص، تكون الآلة كاملة إذا كان لكل حالة \(s\)، ولكل إدخال \(i\)، ولكل قيمة للساعة \(x\) يوجد على الأقل انتقال واحد \((s,x) \xrightarrow{i,o} (s',0)\)؛ وإلا فهي جزئية. وتكون الآلة حتمية إذا كان لكل حالة \(s\)، ولكل إدخال \(i\)، ولكل قيمة للساعة \(x\) يوجد على الأكثر انتقال إدخال/إخراج واحد؛ وإلا فهي غير حتمية.
لأغراض التبسيط، سنقصر من الآن فصاعداً الدراسة على الآلات الكاملة والحتمية، ونترك معالجة الآلات الجزئية وغير الحتمية لأعمال مستقبلية. عندما تكون الآلة \(M\) حتمية وكاملة، تكون \(B_M(w)\) مجموعة أحادية لكل كلمة إدخال \(w\). لذا يمكننا إعادة تعريف السلوك \(B_M\) كدالة \(B_M: (I\times \mathbb{R}^+)^* \mapsto (O\times \mathbb{R}^+)^*\) تربط كل كلمة إدخال \(w = (i_1,t_1)(i_2,t_2)\dots(i_k,t_k)\) بكلمة الإخراج الوحيدة \(B_M(w)\) التي تُنتجها \(M\) تحت الإدخال \(w\).
علاوة على ذلك، يمكننا اعتبار علاقة الانتقال للآلة دالة كاملة \(\lambda_S: S \times I \times \mathbb{R}^+ \mapsto S \times O\) تأخذ كمدخل الحالة الحالية \(s\)، والتأخير \(t\)، ورمز الإدخال \(i\) وتُنتج الحالة التالية والإخراج بحيث \(\lambda_S(s,t,i) = (s',o)\) و\((s,0)\xrightarrow{t}(s,t)\xrightarrow{i,o}(s',0)\). ومع شيء من التجاوز في الترميز، يمكن تعميمها إلى دالة \(\lambda_S: S \times (I \times \mathbb{R}^+)^* \mapsto S \times O^*\) تأخذ كمدخل الحالة الابتدائية \(s\) وكلمة زمنية \(w\)، وتُعيد الحالة التي تصل إليها الآلة بعد قراءة \(w\) وكلمة الإخراج الناتجة. وسنستخدم الترميز \(s \xrightarrow{w,u} s'\) اختصاراً لـ\(\lambda_S(s,w) = (s',u)\).
نوضّح في هذا القسم كيفية حل مسألة التكافؤ لآلات الحالات المحدودة الزمنية ذات الحُرّاس عبر اختزالها إلى مسألة التكافؤ لآلات حالات محدودة غير زمنية. نفعل ذلك بثلاث خطوات: أولاً، نبيّن كيفية بناء آلة حالات محدودة «مجردة» من آلة بحُرّاس؛ ثم نُعرِّف مفهوماً مناسباً للمحاكاة المتبادلة (bisimulation) لمقارنة الآلة الزمنية المجَهَّزة بحُرّاس مع آلة غير زمنية؛ وأخيراً، نستنتج من خصائص علاقة المحاكاة المتبادلة أن آلتين بحُرّاس زمنيين متكافئتان إذا وفقط إذا كان تجريدهما متكافئاً.
لنفترض الآن أن \(M\) آلة حالات محدودة زمنية ذات حُرّاس. نُعرِّف \(\max(M)\) بأنه أكبر ثابت صحيح (غير مساوي لـ\(\infty\)) يظهر في الحُرّاس في \(\lambda_S\). ولكل عدد طبيعي \(N \geq \max(M)\)، نُعرِّف \(\mathbb{I}_N\) بأنها مجموعة الفترات
\(\mathbb{I}_N = \{[n,n] \mid n \leq N\} \cup \{(n,n+1) \mid 0 \leq n < N\} \cup \{(N,\infty)\}\).
وسيتناول التجريد المتقطّع لآلة الحالات المحدودة الزمنية ذات الحُرّاس مُدخلات من الشكل \((i,\langle n,n'\rangle)\) حيث \(i\) هو الإدخال الفعلي و\(\langle n,n'\rangle \in \mathbb{I}_N\) فترة تمثّل التأخير الزمني.
تعريف 3. إذا كانت \(M = (S, I, O, \lambda_S, s_0)\) آلة حالات محدودة زمنية ذات حُرّاس، و\(N \geq \max(M)\) عدداً طبيعياً، فإن آلة الحالات المحدودة المجرّدة \(A^N_M = (S, I\times \mathbb{I}_N, O, \lambda_A, s_0)\) هي آلة غير زمنية بحيث \((s, (i,\langle n,n'\rangle), o, s') \in \lambda_A\) إذا وفقط إذا \((s, i, \langle t,t'\rangle, o, s') \in \lambda_S\) لبعض الحارس \(\langle t,t'\rangle\) الذي يحقق \(\langle n,n'\rangle \subseteq \langle t,t'\rangle\).
لا يمكننا مقارنة سلوك آلة حالات محدودة زمنية مباشرة بسلوك تجريدها غير الزمني، لأن الأولى تقبل كلمات إدخال زمنية على \(I\)، بينما الثانية تقبل كلمات إدخال غير زمنية على \(I \times \mathbb{I}_N\). لذلك، نحتاج إلى تعريف تجريد للكلمة الزمنية.
تعريف 4. إذا كانت \(A\) أبجدية منتهية، و\(v = (a_1,t_1)(a_2,t_2)\dots(a_m,t_m)\) كلمة زمنية منتهية، و\(N\) عدداً طبيعياً، و\(\mathbb{I}_N\) مجموعة الفترات، فإن تجريدها بالنسبة إلى \(\mathbb{I}_N\) هو الكلمة \(\mathbb{I}_N(v) = (a_1,\langle n_1,n_1'\rangle)(a_2,\langle n_2,n_2'\rangle)\ldots(a_m,\langle n_m,n_m'\rangle)\) بحيث، مع تعريف \(t_0 := 0\)، يكون \(t_i - t_{i-1} \in \langle n_i,n_i'\rangle\) لكل \(1 \leq i \leq m\).
تربط المحاكاة المتبادلة المعتمدة على \(\mathbb{I}_N\) حالات آلة الحالات المحدودة الزمنية بحالات آلة غير زمنية.
تعريف 5. إذا كانت \(T = (S, I, O, \lambda_S, s_0)\) آلة حالات محدودة زمنية ذات حُرّاس، و\(U = (R, I\times \mathbb{I}_N, O, \lambda_R, r_0)\) آلة غير زمنية، و\(N \geq \max(T)\)، و\(\mathbb{I}_N\) مجموعة الفترات، فإن محاكاة متبادلة على \(\mathbb{I}_N\) هي علاقة \(\sim \subseteq S \times R\) تحقق الشروط التالية:
تُسمّى \(T\) و\(U\) متشابهتين بمحاكاة متبادلة على \(\mathbb{I}_N\) إذا وُجدت علاقة محاكاة متبادلة \(\sim \subseteq S \times R\) بحيث \(s_0 \sim r_0\).
الآلات المتشابهة بمحاكاة متبادلة على \(\mathbb{I}_N\) لها السلوك نفسه، كما يثبته ما يلي.
لمّة 1. إذا كانت \(T = (S, I, O, \lambda_S, s_0)\) آلة حالات محدودة زمنية ذات حُرّاس، و\(U = (R, I\times \mathbb{I}_N, O, \lambda_R, r_0)\) آلة غير زمنية، ووجِدت علاقة محاكاة متبادلة على \(\mathbb{I}_N\)، ولْنَقُل \(\sim\)، بحيث \(s_0 \sim r_0\)، فعندئذ لكل كلمة إدخال زمنية \(v = (i_1,t_1)(i_2,t_2)\dots(i_m,t_m)\) لدينا
\(\mathop{\mathrm{Untime}}(B_T(v)) = B_U(\mathbb{I}_N(v))\).