2025-11-28T02:22:19.173778

On Probabilistic $ω$-Pushdown Systems, and $ω$-Probabilistic Computational Tree Logic

Lin, Lin
In this paper, we obtain the following equally important new results: We first extend the notion of {\em probabilistic pushdown automaton} to {\em probabilistic $ω$-pushdown automaton} for the first time and study the model-checking question of {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}), showing that model-checking of {\em stateless probabilistic $ω$-pushdown systems ($ω$-pBPA)} against $ω$-PCTL is generally undecidable. Our approach is to construct $ω$-PCTL formulas encoding the {\em Post Correspondence Problem}. We then study in which case there exists an algorithm for model-checking {\it stateless probabilistic $ω$-pushdown systems} and show that the problem of model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable, and further show that this problem is in $NP$-hard.
academic

حول الأنظمة الاحتمالية ω-Pushdown، والمنطق الاحتمالي ω-Computational Tree Logic

المعلومات الأساسية

  • معرّف الورقة: 2209.10517
  • العنوان: On Probabilistic ω-Pushdown Systems, and ω-Probabilistic Computational Tree Logic
  • المؤلفون: Deren Lin, Tianrong Lin
  • التصنيف: cs.LO (المنطق في علوم الحاسوب)، cs.FL (اللغات الشكلية)، quant-ph (الفيزياء الكمية)
  • وقت النشر: ورقة arXiv preprint، آخر إصدار v16 تم تقديمه في 9 نوفمبر 2025
  • رابط الورقة: https://arxiv.org/abs/2209.10517

الملخص

تحقق هذه الورقة إنجازين متساويي الأهمية في مجال الأنظمة الاحتمالية ω-Pushdown ومنطق ω-Probabilistic Computational Tree:

  1. توسيع الأتمتة الاحتمالية pushdown للمرة الأولى إلى الأتمتة الاحتمالية ω-pushdown، ودراسة مشكلة فحص النموذج للأنظمة الاحتمالية ω-pushdown بدون حالات (ω-pBPA) ضد منطق ω-PCTL، مع إثبات أن هذه المشكلة غير قابلة للحسم بشكل عام. تعتمد طريقة الإثبات على بناء صيغة ω-PCTL تشفر مشكلة Post المراسلة (PCP).
  2. دراسة الحالات التي توجد فيها خوارزميات فحص النموذج، مع إثبات أن مشكلة فحص النموذج للأنظمة الاحتمالية ω-pushdown بدون حالات ضد منطق ω-bounded probabilistic computational tree logic (ω-bPCTL) قابلة للحسم، وإثبات إضافي بأن هذه المشكلة هي NP-صعبة.

خلفية البحث والدافع

1. مشكلة البحث

تدرس هذه الورقة مشكلة فحص النموذج للأنظمة الاحتمالية ذات الحالات اللانهائية، مع التركيز بشكل خاص على مشكلة التحقق من صحة نموذج جديد من الأنظمة الاحتمالية ω-pushdown.

2. أهمية المشكلة

  • الأهمية النظرية: فحص النموذج هو أداة أساسية في التحقق الشكلي، مع قيمة تطبيقية مهمة في مجالات مثل التحقق من الدوائر الرقمية
  • الأساس المنطقي: تستند نظرية الحساب بشكل أساسي على المفاهيم المحددة من قبل منطقيين مثل Church و Turing، حيث يلعب المنطق دوراً أساسياً في علوم الحاسوب
  • الاحتياجات العملية: يركز فحص النموذج التقليدي بشكل أساسي على الأنظمة ذات الحالات المحدودة والبرامج غير الاحتمالية، بينما تتزايد احتياجات التحقق من صحة الأنظمة الاحتمالية ذات الحالات اللانهائية

3. قيود الطرق الموجودة

  • قيود PCTL/PCTL*: لا يمكن للمنطق الاحتمالي التقليدي للشجرة الحسابية وصف الخصائص ω-منتظمة، مع افتقار القدرة على التعبير عن الأحداث المتكررة اللانهائية (خصائص liveness)
  • فجوات البحث: على الرغم من أن Chatterjee وآخرين عرّفوا ω-PCTL في عام 2008، لم يتم طرح مفهوم الأتمتة الاحتمالية ω-pushdown من قبل
  • المشاكل غير المحلولة: تم طرح مشكلة فحص النموذج للأنظمة الاحتمالية pushdown بدون حالات ضد PCTL للمرة الأولى في EKM06، ولم يتم حلها إلا من خلال العمل الأخير للمؤلفين LL24

4. دافع البحث

  • توسيع الأنظمة الاحتمالية pushdown إلى نسخة ω للتعامل مع السلوك اللانهائي
  • الاستفادة من قوة التعبير القوية لمنطق ω-PCTL لوصف خصائص الأنظمة الاحتمالية ω-pushdown
  • تحديد حدود قابلية الحسم والتعقيد الحسابي لمشكلة فحص النموذج

المساهمات الأساسية

  1. تعريف الأتمتة الاحتمالية ω-pushdown للمرة الأولى: توسيع الأتمتة الاحتمالية pushdown الكلاسيكية إلى نسخة ω، مع إنشاء نموذج pushdown احتمالي يتعامل مع تسلسلات الإدخال اللانهائية
  2. إثبات عدم قابلية الحسم لـ ω-pBPA ضد ω-PCTL (النظرية 1):
    • إثبات عدم القابلية للحسم من خلال ترميز مشكلة Post المراسلة المعدلة كصيغة ω-PCTL
    • استخلاص نتيجتين: عدم قابلية حسم ω-pBPA ضد ω-PCTL* (النتيجة 2)؛ عدم قابلية حسم ω-pPDS ضد ω-PCTL* (النتيجة 3)
  3. تحديد حد القابلية للحسم (النظرية 4):
    • إثبات أن فحص النموذج لـ ω-pBPA ضد ω-bPCTL (النسخة المحدودة) قابل للحسم
    • إثبات إضافي بأن هذه المشكلة هي NP-صعبة
  4. الابتكار التقني:
    • بناء صيغ ω-PCTL ذكية Ψ₁ و Ψ₂ لترميز PCP
    • استخدام الدوال الاحتمالية ρ و ρ̄ لإنشاء علاقة تكافؤ بين تساوي السلاسل ومجموع الاحتمالات يساوي 1
    • تحقيق القابلية للحسم من خلال تقييد عامل until المحدود U≤k

شرح الطريقة

تعريف المهمة

مشكلة فحص النموذج: بالنظر إلى نظام احتمالي ω-pushdown Δ وصيغة ω-PCTL (أو ω-bPCTL) Ψ، تحديد ما إذا كان M̂_Δ ⊨_L Ψ، حيث M̂_Δ هي سلسلة ماركوف ذات الحالات اللانهائية المستحثة من Δ، و L هي دالة إسناد بسيطة.

الإطار التقني الأساسي

1. تعريف الأتمتة الاحتمالية ω-pushdown (التعريف 3.1)

ثمانية عناصر Θ = (Q, Σ, Γ, δ, q₀, Z, Final, P)، حيث:

  • Q: مجموعة الحالات المحدودة
  • Σ: أبجدية الإدخال المحدودة
  • Γ: أبجدية المكدس المحدودة
  • δ: دالة تعيين قواعد الانتقال
  • q₀: الحالة الأولية
  • Z: الرمز الأولي للمكدس
  • Final ⊆ Q: مجموعة الحالات النهائية
  • P: دالة احتمالية، حيث لكل (p,a,X)، ∑_{(q,α)} P((p,a,X)→(q,α)) = 1

التشغيل الناجح: يُعتبر التشغيل اللانهائي r ناجحاً إذا كان Inf(r) ∩ Final ≠ ∅، حيث Inf(r) هي مجموعة الحالات التي تظهر بشكل لانهائي في r.

2. النسخة بدون حالات: ω-pBPA (التعريف 3.4)

مبسطة إلى خمسة عناصر (Γ, δ, Z, Final, P)، حيث فضاء التكوين هو Γ*، و Final ⊆ Γ (رموز المكدس بدلاً من الحالات).

3. منطق ω-PCTL (القسم 3.1)

الصيغة النحوية:

Φ ::= true | p | ¬Φ | Φ₁ ∧ Φ₂ | P_⊳◁r(φ)
φ ::= XΦ | Φ₁UΦ₂ | φ^ω
φ^ω ::= Buchi(Φ) | coBuchi(Φ) | φ^ω₁ ∧ φ^ω₂ | φ^ω₁ ∨ φ^ω₂

الدلالات الرئيسية:

  • Buchi(Φ): ∀i≥0.∃j≥i. M̂,πj ⊨_L Φ (تحقيق Φ بشكل لانهائي)
  • coBuchi(Φ): ∃i≥0.∀j≥i. M̂,πj ⊨_L Φ (تحقيق Φ في النهاية دائماً)

تقنية إثبات عدم القابلية للحسم (القسم 4)

استراتيجية البناء

بالنظر إلى مثيل PCP معدل {(u'ᵢ, v'ᵢ) : 1≤i≤n}، بناء ω-pBPA Θ' بحيث يوجد حل إذا وفقط إذا كانت صيغة ω-PCTL محددة صحيحة.

تصميم أبجدية المكدس

Γ = {Z,Z',C,F,S,N} ∪ (Σ×Σ) ∪ {X_(x,y)} ∪ {G^j_i : 1≤i≤n, 1≤j≤m+1}

آلية العمل على مرحلتين

المرحلة 1: تخمين الحل (القاعدة (1))

Z → G¹₁Z' | ... | G¹ₙZ'  (احتمالية موحدة 1/n)
G^j_i → G^(j+1)_i (uᵢ(j), vᵢ(j))  (احتمالية 1)
G^(m+1)_i → C | G¹₁ | ... | G¹ₙ  (احتمالية موحدة 1/(n+1))

تولد عملية التخمين التسلسل j₁j₂...jₖ، المقابل لأزواج الكلمات (u_{j₁},v_{j₁})...(u_{jₖ},v_{jₖ}).

المرحلة 2: التحقق من الحل (القاعدة (2))

C → N (احتمالية 1)
N → F | S (احتمالية 1/2 لكل منهما)
(x,y) → X_(x,y) | ε (احتمالية 1/2 لكل منهما)
Z' → Z' (احتمالية 1، لبناء مسار لانهائي)

صيغ الترميز الرئيسية (الصيغة (3))

Ψ₁ = (¬S ∧ ⋀_{z∈Σ}¬X_(B,z)) U ([⋁_{z∈Σ}X_(A,z)] ∨ [Z' ∧ P=1(Buchi(Z'))])

Ψ₂ = (¬F ∧ ⋀_{z∈Σ}¬X_(z,A)) U ([⋁_{z∈Σ}X_(z,B)] ∨ [Z' ∧ P=1(Buchi(Z'))])

دوال الترميز الاحتمالي (اللمة 4.2)

تعريف الدوال ρ و ρ̄، التي تعيّن السلاسل إلى 0,1:

ρ(x₁...xₙ) = ∑ᵢ ϑ(xᵢ)/2ⁱ
ρ̄(x₁...xₙ) = ∑ᵢ ϑ̄(xᵢ)/2ⁱ

حيث ϑ(A)=1, ϑ(B)=0, ϑ(Z')=1؛ و ϑ̄(A)=0, ϑ̄(B)=1, ϑ̄(Z')=1.

الخاصية الرئيسية: u'{j₁}...u'{jₖ} = v'{j₁}...v'{jₖ} ⟺ ρ(u'{j₁}...u'{jₖ}Z') + ρ̄(v'{j₁}...v'{jₖ}Z') = 1

سلسلة اللمات الرئيسية

  • اللمة 4.3: P({π∈Run(FαZ') : π⊨L Ψ₁}) = ρ(u'{j₁}...u'_{jₖ}Z')
  • اللمة 4.4: u'{j₁}...u'{jₖ} = v'{j₁}...v'{jₖ} ⟺ P(FαZ',Ψ₁) + P(SαZ',Ψ₂) = 1
  • اللمة 4.6: PCP لديها حل ⟺ Θ',Z ⊨_L P>0(trueUC ∧ P=1(XP=t/2(Ψ₁) ∧ P=(1-t)/2(Ψ₂)))

إثبات القابلية للحسم والتعقيد (القسم 5)

تعريف ω-bPCTL

استبدال عامل until المحدود U≤k بدلاً من U:

M,π ⊨_L Φ₁U≤kΦ₂ ⟺ ∃0≤i≤k. M,π[i]⊨_L Φ₂ ∧ ∀j<i. M,π[j]⊨_L Φ₁

القابلية للحسم (النظرية 5)

نظراً لأن U≤k يتطلب فقط فحص عدد محدود من الخطوات، تصبح المشكلة قابلة للحسم.

إثبات صعوبة NP

من خلال الاختزال من PCP المحدود (معروف أنه NP-كامل):

  • بناء ω-pBPA أكثر تعقيداً Δ، حيث تحتوي أبجدية المكدس على {1,2,...,n} لترميز تخمين الحد k
  • قواعد الانتقال (7) ترمز في نفس الوقت تخمين الحد وتخمين الحل
  • بناء الصيغة (12)، بحيث يكون لدى PCP المحدود حل ⟺ صيغة فحص النموذج صحيحة
  • يمكن إجراء الاختزال في وقت متعدد الحدود

إعداد التجارب

ملاحظة: هذه الورقة عبارة عن ورقة بحثية نظرية في علوم الحاسوب البحتة، وليس تحتوي على جزء تجريبي. جميع النتائج تم الحصول عليها من خلال الإثبات الرياضي، وليس تتضمن مجموعات بيانات أو تقييمات تجريبية أو تحليل تجريبي.

نتائج التجارب

غير قابل للتطبيق: هذه الورقة لا تحتوي على قسم نتائج التجارب، وجميع الاستنتاجات هي إثبات نظري.

الأعمال ذات الصلة

1. فحص نموذج الأنظمة الاحتمالية Pushdown

  • EKM06: أول دراسة لفحص نموذج الأنظمة الاحتمالية pushdown، مع طرح مشكلة pBPA ضد PCTL (تم حلها فقط في LL24)
  • BBFK14: إثبات عدم قابلية حسم pPDS ضد PCTL، وعدم قابلية حسم pBPA ضد PCTL*
  • Brá07: دراسة التحقق من صحة البرامج الاحتمالية العودية

2. منطق خصائص ω-منتظمة

  • CSH08: تعريف Chatterjee وآخرين لـ ω-PCTL، القادر على التعبير عن خصائص ω-منتظمة
  • CCT16: دراسة أهداف ω-منتظمة (parity objectives) لعمليات اتخاذ القرار الاحتمالية المرئية جزئياً
  • LL14: توسيع ω آخر لمنطق شجرة حسابي متفرع (لكن يصعب احتمالته)

3. نظرية الأتمتة ω-Pushdown

  • CG77: العمل الكلاسيكي لـ Cohen و Gold حول اللغات ω-خالية من السياق
  • DDK22: النظرية المنطقية للأتمتة ω-pushdown

4. نقاط الابتكار في هذه الورقة

  • أول تطبيق للتوسيع الاحتمالي على الأتمتة ω-pushdown
  • أول دراسة لمشكلة فحص النموذج لـ ω-pBPA/ω-pPDS
  • تحديد حدود القابلية للحسم لـ ω-PCTL و ω-bPCTL

الخلاصة والمناقشة

الاستنتاجات الرئيسية

  1. نتائج عدم القابلية للحسم:
    • فحص النموذج لـ ω-pBPA ضد ω-PCTL غير قابل للحسم بشكل عام (النظرية 1)
    • فحص النموذج لـ ω-pBPA ضد ω-PCTL* غير قابل للحسم (النتيجة 2)
    • فحص النموذج لـ ω-pPDS ضد ω-PCTL* غير قابل للحسم (النتيجة 3)
  2. القابلية للحسم والتعقيد:
    • فحص النموذج لـ ω-pBPA ضد ω-bPCTL قابل للحسم (النظرية 4)
    • هذه المشكلة هي NP-صعبة (النظرية 4)
  3. المساهمات التقنية:
    • تعريف ناجح للنموذج الشكلي للأتمتة الاحتمالية ω-pushdown
    • إنشاء علاقة تكافؤ بين PCP وقابلية الرضا لصيغ ω-PCTL
    • تحقيق القابلية للحسم من خلال تقييد عدد خطوات عامل until

القيود

  1. نقص الخوارزميات: على الرغم من إثبات قابلية الحسم لـ ω-bPCTL، لم يتم تقديم خوارزمية محددة
  2. الحد الأعلى للتعقيد غير معروف: تم إثبات صعوبة NP فقط، ولم يتم تحديد ما إذا كانت المشكلة في NP، والتعقيد الدقيق لا يزال مفتوحاً
  3. قيود الإسناد البسيط: لتجنب ترميز خصائص غير قابلة للحسم، تم النظر فقط في دوال الإسناد البسيطة (التعريف 3.5)، مما يحد من قدرة التعبير للنموذج
  4. عدم التحقق من الجدوى العملية: كعمل نظري بحت، لم تتم مناقشة السيناريوهات التطبيقية الفعلية أو جدوى التنفيذ

الاتجاهات المستقبلية

تحدد الورقة بوضوح المشاكل المفتوحة التالية:

  1. تصميم الخوارزميات: إيجاد خوارزمية محددة لفحص النموذج لـ ω-pBPA ضد ω-bPCTL
  2. التعقيد الدقيق: تحديد ما إذا كانت هذه المشكلة في NP، وما إذا كانت NP-كاملة
  3. مشكلة الرضا: دراسة مشكلة الرضا لـ ω-PCTL (مشابهة لكون الرضا LTL هو PSPACE-صعب):
    • بالنظر إلى صيغة حالة ω-PCTL φ، هل يوجد نظام احتمالي ω-pushdown Δ بحيث M̂_Δ,s ⊨_L φ؟
  4. متغيرات منطقية أخرى: استكشاف نسخ أخرى مقيدة من ω-PCTL، والبحث عن التوازن بين القابلية للحسم وقدرة التعبير

التقييم المتعمق

المميزات

  1. الابتكار النظري قوي:
    • أول طرح للأتمتة الاحتمالية ω-pushdown، ملء الفجوة في هذا المجال
    • ترميز PCP بذكاء كصيغة ω-PCTL، تقنية الإثبات لها أصالة عالية
    • فكرة تحقيق القابلية للحسم من خلال عامل محدود لها قيمة إرشادية
  2. الإثبات دقيق وكامل:
    • سلسلة اللمات واضحة، من اللمة 4.1 إلى 4.6 تبني إثبات عدم القابلية للحسم تدريجياً
    • تصميم دوال الترميز الاحتمالي ρ و ρ̄ ذكي، مع الاستفادة من التوسيع الثنائي لإنشاء علاقة تكافؤ
    • إثبات الاختزال مفصل، مع النظر في جميع الحالات الرئيسية
  3. أهمية النتائج:
    • تحديد عدم قابلية حسم فحص النموذج لـ ω-PCTL، رسم الحدود النظرية لهذا المجال
    • نتيجة صعوبة NP توفر مرجع حد أدنى للتعقيد لتصميم الخوارزميات
    • النتائج 2 و 3 توسع نطاق تطبيق نتائج عدم القابلية للحسم
  4. الكتابة واضحة:
    • هيكل الورقة معقول، من الخلفية إلى التعريف ثم الإثبات، مع تسلسل هرمي واضح
    • نظام الرموز كامل، التعاريف دقيقة
    • نقاط التقنية الرئيسية لها شرح حدسي كافٍ

أوجه القصور

  1. نقص تنفيذ الخوارزميات:
    • النظرية 4 تثبت القابلية للحسم لكن لم تعطِ خوارزمية، القيمة العملية محدودة
    • لا توجد مناقشة لحدود التعقيد الزمني/المكاني للخوارزمية
    • نقص إثبات بناء لصحة الخوارزمية وإنهاؤها
  2. وصف التعقيد غير كامل:
    • تم إثبات صعوبة NP فقط، لم يتم تحديد ما إذا كانت في NP
    • قد يكون هناك فئة تعقيد أكثر دقة (مثل PSPACE أو EXPTIME وغيرها)
    • لا توجد مناقشة للتعقيد المعامل (مثل حالات n أو m أو k المحددة)
  3. مناقشة التطبيق العملي غير كافية:
    • لم يتم تقديم سيناريوهات تطبيقية فعلية للأنظمة الاحتمالية ω-pushdown
    • نقص الربط مع مشاكل التحقق الفعلية
    • لا توجد مناقشة لقدرة النمذجة والقيود
  4. مشاكل التفاصيل التقنية:
    • قيد الإسناد البسيط (التعريف 3.5) قوي نسبياً، قد يحد بشكل مفرط من قدرة النموذج
    • ما إذا كان قيد الحد k≤n في اختزال PCP المحدود ضروري لم يتم توضيحه بشكل كافٍ
    • بعض خطوات الإثبات (مثل إثبات الاستقراء للمة 5.3) طويلة نسبياً، قد يكون هناك مجال للتبسيط
  5. مقارنة الأعمال ذات الصلة غير كافية:
    • لم تتم مقارنة تفصيلية مع نسخة غير احتمالية من الأتمتة ω-pushdown
    • لم تتم مناقشة العلاقة مع نماذج احتمالية أخرى (مثل آلات تورينج الاحتمالية)
    • نقص الربط مع نماذج الحساب الكمي (على الرغم من أن التصنيف يتضمن quant-ph)

التأثير

  1. المساهمة النظرية:
    • وضع الأساس لنظرية الأتمتة الاحتمالية ω
    • توفير حالة جديدة لدراسة تعقيد فحص النموذج
    • قد تلهم أبحاثاً أخرى حول الأنظمة ذات الحالات اللانهائية
  2. القيمة العملية:
    • القيمة العملية المباشرة محدودة (نقص الخوارزميات)
    • لكن توجيه واضح للأبحاث المستقبلية لتصميم الخوارزميات
    • نتائج عدم القابلية للحسم تتجنب البحث غير المجدي عن خوارزميات
  3. قابلية إعادة الإنتاج:
    • كإثبات نظري، يمكن إعادة إنتاجه بشكل أساسي
    • لكن التعقيد العالي للإثبات يتطلب خلفية عميقة في اللغات الشكلية والنظرية الاحتمالية
    • لم يتم توفير التحقق الشكلي (مثل إثبات Coq/Isabelle)

السيناريوهات المطبقة

  1. البحث النظري:
    • نظرية اللغات الشكلية والأتمتة
    • نظرية التعقيد الحسابي
    • نظرية فحص النموذج
  2. مجالات التطبيق المحتملة:
    • التحقق الشكلي من الأنظمة الاحتمالية
    • إثبات صحة الخوارزميات العشوائية
    • التحقق من خصائص الأنظمة المتزامنة الاحتمالية
    • النمذجة العشوائية للأنظمة البيولوجية والفيزيائية
  3. السيناريوهات غير المطبقة:
    • مشاريع التحقق الهندسية التي تتطلب أدوات فعلية (حالياً نقص تنفيذ الخوارزميات)
    • الأنظمة ذات الحالات المحدودة (توجد طرق أكثر كفاءة)
    • الأنظمة في الوقت الفعلي التي تتطلب حكماً سريعاً (صعوبة NP تعني كفاءة منخفضة في الحالة الأسوأ)

المراجع

تستشهد الورقة بـ 41 مرجعاً، والمراجع الرئيسية تشمل:

  1. BK08 Baier & Katoen: مبادئ فحص النموذج - كتاب مدرسي كلاسيكي لفحص النموذج
  2. CSH08 Chatterjee وآخرون: التعريف الأصلي لمنطق ω-PCTL
  3. EKM06 Esparza وآخرون: العمل الرائد في فحص نموذج الأنظمة الاحتمالية pushdown
  4. BBFK14 Brázdil وآخرون: نتائج عدم القابلية للحسم لـ pPDS و pBPA
  5. CG77 Cohen & Gold: النظرية الكلاسيكية للغات ω-خالية من السياق
  6. GJ79 Garey & Johnson: نظرية NP-الاكتمال، تعقيد PCP المحدود
  7. Pos46 Post: الورقة الأصلية لمشكلة Post المراسلة
  8. LL24 العمل السابق للمؤلفين: حل المشكلة المفتوحة لـ pBPA ضد PCTL

التقييم الشامل: هذه ورقة بحثية عالية الجودة في علوم الحاسوب النظرية، مع مساهمات مهمة في مجال نظرية الأتمتة الاحتمالية وفحص النموذج. تقنية إثبات عدم القابلية للحسم ذكية، ونتائج القابلية للحسم والتعقيد لنسخة ω-bPCTL تكمل الصورة النظرية. أوجه القصور الرئيسية تتعلق بنقص تنفيذ الخوارزميات والوصف الكامل للتعقيد، لكن كعمل نظري أساسي، قيمتها لا تُنكر. الورقة مناسبة للنشر في المجلات الرائدة في علوم الحاسوب النظرية (مثل JACM و LMCS و TCS وغيرها).