2025-11-23T10:46:16.032830

Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control

Phalakarn, Pruekprasert, Hasuo
Stochastic games are fundamental in various applications, including the control of cyber-physical systems (CPS), where both controller and environment are modeled as players. Traditional algorithms typically aim to determine a single winning strategy to develop a controller. However, in CPS control and other domains, permissive controllers are essential, as they enable the system to adapt when additional constraints arise and remain resilient to runtime changes. This work generalizes the concept of (permissive winning) strategy templates, originally introduced by Anand et al. at TACAS and CAV 2023 for deterministic games, to incorporate stochastic games. These templates capture an infinite number of winning strategies, allowing for efficient strategy adaptation to system changes. We focus on two winning criteria (almost-sure and positive winning) and five winning objectives (safety, reachability, Büchi, co-Büchi, and parity). Our contributions include algorithms for constructing templates for each winning criterion and objective and a novel approach for extracting a winning strategy from a given template. Discussions on comparisons between templates and between strategy extraction methods are provided.
academic

স্টোকাস্টিক প্যারিটি গেমের প্রায়-নিশ্চিত এবং ইতিবাচক জয়ের জন্য কৌশল টেমপ্লেট: অনুমতিশীল এবং স্থিতিস্থাপক নিয়ন্ত্রণের দিকে

মৌলিক তথ্য

  • পেপার আইডি: 2409.08607
  • শিরোনাম: Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control
  • লেখক: Kittiphon Phalakarn, Sasinee Pruekprasert, Ichiro Hasuo
  • শ্রেণীবিভাগ: eess.SY cs.LO cs.SY
  • প্রকাশনার সময়: ২০২৪ সেপ্টেম্বর (arXiv v2: ২০২৫ অক্টোবর ১৬)
  • পেপার লিঙ্ক: https://arxiv.org/abs/2409.08607

সারসংক্ষেপ

স্টোকাস্টিক গেম বিভিন্ন প্রয়োগে মৌলিক ভূমিকা পালন করে, বিশেষত সাইবার-ফিজিক্যাল সিস্টেম (CPS) নিয়ন্ত্রণে, যেখানে নিয়ন্ত্রক এবং পরিবেশ গেম অংশগ্রহণকারী হিসাবে মডেল করা হয়। ঐতিহ্যবাহী অ্যালগরিদম সাধারণত নিয়ন্ত্রক উন্নয়নের জন্য একটি একক জয়ী কৌশল নির্ধারণ করার লক্ষ্য রাখে। তবে CPS নিয়ন্ত্রণ এবং অন্যান্য ক্ষেত্রে, অনুমতিশীল নিয়ন্ত্রক অত্যন্ত গুরুত্বপূর্ণ কারণ তারা অতিরিক্ত সীমাবদ্ধতা দেখা দিলে সিস্টেমের সাথে খাপ খাইয়ে নিতে এবং রানটাইম পরিবর্তনের প্রতি স্থিতিস্থাপক থাকতে পারে। এই কাজটি কৌশল টেমপ্লেট ধারণাটি নির্ধারণমূলক গেম থেকে স্টোকাস্টিক গেমে সাধারণীকরণ করে, যা অসংখ্য জয়ী কৌশল ক্যাপচার করতে পারে এবং সিস্টেম পরিবর্তনের জন্য দক্ষ কৌশল অভিযোজন সক্ষম করে। আমরা দুটি জয়ের মানদণ্ড (প্রায়-নিশ্চিত জয় এবং ইতিবাচক সম্ভাবনা জয়) এবং পাঁচটি জয়ের উদ্দেশ্য (নিরাপত্তা, পৌঁছানো, Büchi, co-Büchi এবং প্যারিটি) এর উপর ফোকাস করি।

গবেষণা পটভূমি এবং প্রেরণা

সমস্যার পটভূমি

  1. ঐতিহ্যবাহী পদ্ধতির সীমাবদ্ধতা: ঐতিহ্যবাহী গেম সমাধান অ্যালগরিদম সাধারণত শুধুমাত্র একটি একক জয়ী কৌশল খোঁজে, কৌশলের অনুমতিশীলতা (permissiveness) বিবেচনা করে না
  2. ব্যবহারিক প্রয়োগের চাহিদা: সাইবার-ফিজিক্যাল সিস্টেম নিয়ন্ত্রণে, অতিরিক্ত সীমাবদ্ধতা এবং রানটাইম পরিবর্তনের সাথে খাপ খাইয়ে নেওয়ার জন্য অনুমতিশীল নিয়ন্ত্রক প্রয়োজন
  3. স্থিতিস্থাপক নিয়ন্ত্রণের চাহিদা: সিস্টেমকে ব্যর্থতা বা পরিবেশগত পরিবর্তনের মুখোমুখি হলেও শক্তিশালী থাকতে হবে

গবেষণার প্রেরণা

  • বিদ্যমান কৌশল টেমপ্লেট ধারণা শুধুমাত্র নির্ধারণমূলক গেমে প্রযোজ্য, স্টোকাস্টিক গেমের জন্য সমর্থনের অভাব
  • অসংখ্য জয়ী কৌশল ক্যাপচার করতে পারে এমন একটি কাঠামোর প্রয়োজন যা দ্রুত কৌশল অভিযোজন সমর্থন করে
  • CPS নিয়ন্ত্রণ ইত্যাদি ব্যবহারিক প্রয়োগে, অনুমতিশীলতা এবং স্থিতিস্থাপকতা মূল প্রয়োজনীয়তা

মূল অবদান

  1. প্রায়-নিশ্চিত জয়ী কৌশল টেমপ্লেট অ্যালগরিদম: পাঁচটি জয়ের উদ্দেশ্যের জন্য (নিরাপত্তা, পৌঁছানো, Büchi, co-Büchi, প্যারিটি) প্রায়-নিশ্চিত জয়ী কৌশল টেমপ্লেট নির্মাণ অ্যালগরিদম প্রস্তাব করা
  2. ইতিবাচক সম্ভাবনা জয়ী কৌশল টেমপ্লেট: ইতিবাচক সম্ভাবনা জয়ের মানদণ্ডের অধীনে কৌশল টেমপ্লেট নির্মাণ এবং সমন্বয় অ্যালগরিদম বিকাশ
  3. কৌশল টেমপ্লেট তুলনা কাঠামো: অনুমতিশীলতা এবং আকারের উপর ভিত্তি করে টেমপ্লেট তুলনা আলোচনা প্রদান
  4. কৌশল নিষ্কাশন পদ্ধতি: প্রদত্ত টেমপ্লেট থেকে জয়ী কৌশল নিষ্কাশনের নতুন পদ্ধতি প্রস্তাব করা, জয়ের উদ্দেশ্য এবং অনুমতিশীলতার ভারসাম্য রক্ষা করে

পদ্ধতির বিস্তারিত বিবরণ

কাজের সংজ্ঞা

স্টোকাস্টিক গেমের সংজ্ঞা: G = (V, E, (V□, V○, V△)), যেখানে:

  • V হল শীর্ষবিন্দু সেট, E হল প্রান্ত সেট
  • V□, V○, V△ যথাক্রমে Even খেলোয়াড়, Odd খেলোয়াড় এবং Random খেলোয়াড়ের শীর্ষবিন্দু প্রতিনিধিত্ব করে
  • "২.৫" খেলোয়াড় গেম হিসাবে পরিচিত, যাতে দুটি প্রধান খেলোয়াড় এবং একটি র্যান্ডম খেলোয়াড় রয়েছে

কৌশল টেমপ্লেটের সংজ্ঞা: T = (P, L, C), যেখানে:

  • P ⊆ E□ হল নিষিদ্ধ প্রান্ত সেট
  • L ⊆ 2^E□ হল সক্রিয় গ্রুপ সেট
  • C ⊆ E□ হল সহ-সক্রিয় প্রান্ত সেট

মডেল আর্কিটেকচার

১. প্রায়-নিশ্চিত জয়ী কৌশল টেমপ্লেট নির্মাণ

নিরাপত্তা উদ্দেশ্য (G X):

SafetyTemplate(G, X):
1. W□ ← νY.(X ∩ (Pre□(Y) ∪ Pre(Y)))
2. P ← Edges□(W□, V \ W□)
3. return (P, ∅, ∅)

পৌঁছানো উদ্দেশ্য (F X):

ReachabilityTemplate(G, X):
1. A ← Attr'(X)
2. W□ ← Attr'□(A)
3. P ← Edges□(W□, V \ W□)
4. C ← Edges□(W□ \ A, W□ \ A)
5. return (P, ∅, C)

Büchi উদ্দেশ্য (GF X): LiveGroups ফাংশনের মাধ্যমে সক্রিয় গ্রুপ নির্মাণ, লক্ষ্য সেট অসীমবার পরিদর্শন নিশ্চিত করে।

প্যারিটি উদ্দেশ্য:

  1. স্টোকাস্টিক গেমকে নির্ধারণমূলক গেমে হ্রাস করা (Reduce অ্যালগরিদম ব্যবহার করে)
  2. নির্ধারণমূলক গেমের কৌশল টেমপ্লেট নির্মাণ
  3. স্টোকাস্টিক গেমের টেমপ্লেটে রূপান্তর

২. ইতিবাচক সম্ভাবনা জয়ী কৌশল টেমপ্লেট নির্মাণ

PositiveTemplate(G, φ):
1. W□, W○ এবং প্রায়-নিশ্চিত জয়ী টেমপ্লেট T^(a) গণনা করুন
2. W? ← V \ (W□ ∪ W○)
3. P^(p) ← P^(a) ∪ Edges□(W?, W○)
4. C^(p) ← C^(a) ∪ Edges□(W?, W?)
5. return T^(p) = (P^(p), L^(p), C^(p))

প্রযুক্তিগত উদ্ভাবনী পয়েন্ট

  1. সেট অপারেশন সম্প্রসারণ: Random খেলোয়াড় বিবেচনা করে নতুন সেট অপারেটর প্রবর্তন, যেমন Pre△(X', X) এবং Attr'□(X)
  2. টেমপ্লেট সমন্বয় অ্যালগরিদম: সংঘর্ষ সনাক্তকরণ প্রক্রিয়া প্রস্তাব করা, যখন টেমপ্লেট সংঘর্ষ হয় তখন পুনরায় গণনা করা
  3. প্যারামিটারাইজড কৌশল নিষ্কাশন: অনুমতিশীলতা এবং উদ্দেশ্য অর্জনের গতির ভারসাম্য রাখতে প্যারামিটার α এবং β ব্যবহার করা
  4. ইতিবাচক সম্ভাবনা জয় সম্প্রসারণ: প্রথমবারের মতো কৌশল টেমপ্লেট ইতিবাচক সম্ভাবনা জয়ের মানদণ্ডে সম্প্রসারণ

পরীক্ষামূলক সেটআপ

তাত্ত্বিক যাচাইকরণ

পেপারটি প্রধানত তাত্ত্বিক প্রমাণের মাধ্যমে অ্যালগরিদমের সঠিকতা যাচাই করে, যার মধ্যে রয়েছে:

  • বিভিন্ন টেমপ্লেট নির্মাণ অ্যালগরিদমের সঠিকতা উপপাদ্য
  • কৌশল নিষ্কাশন পদ্ধতির অনুমতিশীলতা উপপাদ্য
  • টেমপ্লেট সমন্বয় অ্যালগরিদমের সঠিকতা প্রমাণ

জটিলতা বিশ্লেষণ

  • কৌশল নির্মাণ অ্যালগরিদমের সর্বনিম্ন ক্ষেত্রে চলার সময় মান অ্যালগরিদমের সাথে মিলে যায়
  • টেমপ্লেট সমন্বয় এবং কৌশল নিষ্কাশন রানটাইমে দক্ষতার সাথে সম্পাদিত হতে পারে

পরীক্ষামূলক ফলাফল

তাত্ত্বিক ফলাফল

উপপাদ্য ১০-১৪: বিভিন্ন জয়ের উদ্দেশ্যের জন্য কৌশল টেমপ্লেট নির্মাণ অ্যালগরিদমের সঠিকতা প্রমাণ করা

  • SafetyTemplate দ্বারা নির্মিত টেমপ্লেট G X এর জন্য প্রায়-নিশ্চিত জয়ী
  • ReachabilityTemplate দ্বারা নির্মিত টেমপ্লেট F X এর জন্য প্রায়-নিশ্চিত জয়ী
  • অনুরূপভাবে অন্যান্য উদ্দেশ্যের জন্য প্রযোজ্য

উপপাদ্য ১৮: PositiveTemplate দ্বারা নির্মিত টেমপ্লেট প্রায়-নিশ্চিত জয়ী এবং ইতিবাচক সম্ভাবনা জয়ী উভয়ই

উপপাদ্য ২৭: প্যারামিটারাইজড নিষ্কাশন পদ্ধতি মূল Extract পদ্ধতির চেয়ে বেশি অনুমতিশীল

অনুমতিশীলতা বিশ্লেষণ

প্রস্তাব ২২: যদি P ⊇ P', L ⊇ L', C ⊇ C' হয়, তাহলে T, T' এর চেয়ে বেশি অনুমতিশীল নয়

প্রস্তাব ২৩: যদি T, T' এর চেয়ে বেশি অনুমতিশীল না হয় এবং T' জয়ী হয়, তাহলে T ও জয়ী

ব্যবহারিক প্রয়োগের সম্ভাবনা

পেপারটি নির্দেশ করে যে নির্ধারণমূলক গেমের উপর ভিত্তি করে পরীক্ষামূলক ফলাফল, কৌশল টেমপ্লেট বর্ধিত সংশ্লেষণে কমপক্ষে ২ গুণ ত্বরণ অর্জন করতে পারে এবং ত্রুটি-সহনশীল নিয়ন্ত্রণে ৩০% পছন্দ নিষিদ্ধ হলেও কার্যকরভাবে পুনরায় গণনা হ্রাস করতে পারে।

সম্পর্কিত কাজ

ক্লাসিক্যাল অনুমতিশীলতা তত্ত্ব

  • Ramadge এবং Wonham (১৯৮৭) তত্ত্বাবধায়ক নিয়ন্ত্রণে অনুমতিশীলতা ধারণা আনুষ্ঠানিকভাবে প্রবর্তন করেছেন
  • Bernet এবং অন্যরা প্যারিটি গেমে সর্বাধিক অনুমতিশীল কৌশলের অস্তিত্ব প্রমাণ করেছেন

কৌশল টেমপ্লেট উন্নয়ন

  • Anand এবং অন্যরা TACAS এবং CAV ২০২৩-এ নির্ধারণমূলক গেমের কৌশল টেমপ্লেট প্রবর্তন করেছেন
  • এই কাজটি স্টোকাস্টিক গেমে কৌশল টেমপ্লেট সম্প্রসারণের প্রথম গবেষণা

স্টোকাস্টিক গেম সমাধান

  • Chatterjee এবং অন্যদের স্টোকাস্টিক প্যারিটি গেম হ্রাস পদ্ধতি
  • Banerjee এবং অন্যদের স্টোকাস্টিক গেমের জন্য সেট অপারেটর

উপসংহার এবং আলোচনা

প্রধান উপসংহার

  1. কৌশল টেমপ্লেট ধারণা নির্ধারণমূলক গেম থেকে স্টোকাস্টিক গেমে সফলভাবে সম্প্রসারণ করা হয়েছে
  2. সম্পূর্ণ অ্যালগরিদম কাঠামো প্রদান করা হয়েছে, দুটি জয়ের মানদণ্ড এবং পাঁচটি জয়ের উদ্দেশ্য কভার করে
  3. নতুন কৌশল নিষ্কাশন পদ্ধতি সঠিকতা নিশ্চিত করার সাথে সাথে অনুমতিশীলতা উন্নত করে

সীমাবদ্ধতা

  1. ইতিবাচক সম্ভাবনা জয়ী কৌশল সর্বোত্তম সম্ভাবনা নিশ্চিত করে না
  2. অ্যালগরিদম বাস্তবায়ন এবং পরীক্ষামূলক যাচাইকরণ সম্পন্ন হওয়া বাকি
  3. শুধুমাত্র সীমিত অবস্থা গেম বিবেচনা করা হয়েছে

ভবিষ্যত দিকনির্দেশনা

  1. একই অনুমতিশীলতা বজায় রেখে ছোট টেমপ্লেট নির্মাণ
  2. মেট্রিক টাইমড লজিক (MTL) সূত্র দ্বারা সংজ্ঞায়িত উদ্দেশ্যে সম্প্রসারণ
  3. রিয়েল-টাইম সিস্টেমে প্রয়োগ

গভীর মূল্যায়ন

শক্তি

  1. উল্লেখযোগ্য তাত্ত্বিক অবদান: স্টোকাস্টিক গেমে কৌশল টেমপ্লেট প্রথমবারের মতো সম্প্রসারণ, সম্পূর্ণ তাত্ত্বিক কাঠামো
  2. যুক্তিসঙ্গত অ্যালগরিদম ডিজাইন: বিদ্যমান সেট অপারেশন এবং হ্রাস কৌশল দক্ষতার সাথে ব্যবহার
  3. বিস্তৃত প্রয়োগ সম্ভাবনা: সাইবার-ফিজিক্যাল সিস্টেম নিয়ন্ত্রণের জন্য গুরুত্বপূর্ণ ব্যবহারিক তাৎপর্য
  4. গাণিতিক কঠোরতা: সম্পূর্ণ সঠিকতা প্রমাণ প্রদান করা হয়েছে

অপূর্ণতা

  1. পরীক্ষামূলক যাচাইকরণের অভাব: প্রধানত তাত্ত্বিক কাজ, বাস্তব বাস্তবায়ন এবং কর্মক্ষমতা মূল্যায়নের অভাব
  2. সর্বোত্তমতা সমস্যা: ইতিবাচক সম্ভাবনা জয়ী কৌশল সর্বোত্তমতা নিশ্চিত করে না
  3. অপর্যাপ্ত জটিলতা বিশ্লেষণ: প্রকৃত গণনামূলক জটিলতার বিশ্লেষণ অপেক্ষাকৃত সংক্ষিপ্ত

প্রভাব

  1. একাডেমিক মূল্য: স্টোকাস্টিক গেম তত্ত্বে নতুন সরঞ্জাম এবং পদ্ধতি প্রদান করে
  2. ব্যবহারিক মূল্য: অনুমতিশীল নিয়ন্ত্রক ডিজাইনের জন্য তাত্ত্বিক ভিত্তি প্রদান করে
  3. সম্প্রসারণযোগ্যতা: পরবর্তী গবেষণার জন্য একটি ভাল ভিত্তি কাঠামো প্রদান করে

প্রযোজ্য পরিস্থিতি

  1. সাইবার-ফিজিক্যাল সিস্টেমের শক্তিশালী নিয়ন্ত্রণ
  2. অভিযোজনযোগ্যতার প্রয়োজন এমন স্বয়ংক্রিয় সিস্টেম
  3. বহু-উদ্দেশ্য অপ্টিমাইজেশনের নিয়ন্ত্রক সিস্টেম ডিজাইন
  4. ত্রুটি-সহনশীল নিয়ন্ত্রণ সিস্টেম

তথ্যসূত্র

পেপারটি ৩৫টি সম্পর্কিত তথ্যসূত্র উদ্ধৃত করে, যা প্রধানত অন্তর্ভুক্ত করে:

  • গেম তত্ত্ব মৌলিক সাহিত্য
  • তত্ত্বাবধায়ক নিয়ন্ত্রণ তত্ত্ব
  • কৌশল টেমপ্লেট সম্পর্কিত কাজ
  • স্টোকাস্টিক গেম সমাধান অ্যালগরিদম
  • রৈখিক সময় যুক্তি এবং মডেল পরীক্ষা

সামগ্রিক মূল্যায়ন: এটি একটি উচ্চ মানের তাত্ত্বিক গবেষণা পেপার যা কৌশল টেমপ্লেট ধারণা নির্ধারণমূলক গেম থেকে স্টোকাস্টিক গেমে সফলভাবে সম্প্রসারণ করে এবং অনুমতিশীল এবং স্থিতিস্থাপক নিয়ন্ত্রণের জন্য গুরুত্বপূর্ণ তাত্ত্বিক ভিত্তি প্রদান করে। যদিও পরীক্ষামূলক যাচাইকরণের অভাব রয়েছে, তবে তাত্ত্বিক অবদান উল্লেখযোগ্য এবং সম্পর্কিত ক্ষেত্রে গুরুত্বপূর্ণ প্রচারমূলক প্রভাব রয়েছে।