Efficient Shield Synthesis via State-Space Transformation
Brorholt, Høeg-Petersen, Larsen et al.
We consider the problem of synthesizing safety strategies for control systems, also known as shields. Since the state space is infinite, shields are typically computed over a finite-state abstraction, with the most common abstraction being a rectangular grid. However, for many systems, such a grid does not align well with the safety property or the system dynamics. That is why a coarse grid is rarely sufficient, but a fine grid is typically computationally infeasible to obtain. In this paper, we show that appropriate state-space transformations can still allow to use a coarse grid at almost no computational overhead. We demonstrate in three case studies that our transformation-based synthesis outperforms a standard synthesis by several orders of magnitude. In the first two case studies, we use domain knowledge to select a suitable transformation. In the third case study, we instead report on results in engineering a transformation without domain knowledge.
تبحث هذه الورقة في مشكلة تركيب سياسات الأمان لأنظمة التحكم، المعروفة أيضاً بتركيب الدرع. نظراً لأن فضاء الحالة لا نهائي، يتم حساب الدرع عادة على تجريدات فضاء الحالة المحدودة، والتجريد الأكثر شيوعاً هو الشبكة المستطيلة. ومع ذلك، بالنسبة للعديد من الأنظمة، لا تتطابق هذه الشبكة بشكل جيد مع خصائص الأمان أو ديناميكيات النظام. عادة ما تكون الشبكات الخشنة غير كافية، بينما تكون الشبكات الدقيقة غالباً غير قابلة للتطبيق من الناحية الحسابية. توضح هذه الورقة أن تحويلات فضاء الحالة المناسبة يمكن أن تسمح باستخدام شبكات خشنة مع تكلفة حسابية قليلة جداً. من خلال ثلاث دراسات حالة، يتم إثبات أن طريقة التركيب القائمة على التحويل تحقق تحسناً في الأداء بعدة رتب من حيث الحجم مقارنة بطريقة التركيب القياسية.
المشكلة الأساسية التي تسعى هذه الدراسة لحلها هي كيفية تركيب سياسات الأمان (الدروع) بكفاءة لأنظمة التحكم. في الأنظمة الفيزيائية السيبرانية، يحتاج المتحكم الرقمي إلى ضمان سلامة النظام، مما يدفع تطوير طرق بناء المتحكم التلقائي.
من خلال تحويلات فضاء الحالة، يتم محاذاة الشبكة بشكل أفضل مع ديناميكيات النظام في فضاء الحالة الجديد، مما يحسن جودة التركيب مع الحفاظ على الكفاءة الحسابية.
تستشهد الورقة بـ 31 مرجعاً ذا صلة، تغطي أعمالاً مهمة في نظرية التحكم والطرق الرسمية والتعلم المعزز وتفسير التجريد، مما يوفر أساساً نظرياً متيناً للبحث.
التقييم الإجمالي: هذه ورقة بحثية عالية الجودة تقترح حلاً مبتكراً لمعالجة التحديات الحسابية في تركيب الدرع. تتمتع الطريقة بأساس نظري قوي وقيمة عملية كبيرة، مما يساهم بشكل كبير في مجال تركيب الأمان لأنظمة التحكم.