Most research on formal system design has focused on optimizing various measures of efficiency. However, insufficient attention has been given to the design of systems optimizing resilience, the ability of systems to adapt to unexpected changes or adversarial disruptions. In our prior work, we formalized the intuitive notion of resilience as a property of cyber-physical systems by using a multiset rewriting language with explicit time. In the present paper, we study the computational complexity of a formalization of time-bounded resilience problems for the class of $\eta$-simple progressing planning scenarios, where, intuitively, it is simple to check that a system configuration is critical, and only a finite number of actions can be carried out in a bounded time period. We show that, in the time-bounded model with $n$ (potentially adversarially chosen) updates, the corresponding time-bounded resilience problem for this class of systems is complete for the $\Sigma^P_{2n+1}$ class of the polynomial hierarchy, PH. To support the formal models and complexity results, we perform automated experiments for time-bounded verification using the rewriting logic tool Maude.

翻译：大多数关于形式化系统设计的研究集中在优化各种效率度量上。然而，对于优化韧性的系统设计关注不足，韧性是指系统适应意外变化或对抗性干扰的能力。在我们先前的工作中，通过使用带有显式时间的多重集重写语言，将韧性的直观概念形式化为信息物理系统的一种属性。在本文中，我们研究了$\eta$简单进展规划场景类别的有界时间韧性问题的计算复杂性，直观上，这类场景中检查系统配置是否临界是简单的，且有限时间内只能执行有限数量的动作。我们证明，在具有$n$个（可能是对抗性选择的）更新的有界时间模型中，此类系统的对应有界时间韧性问题对于多项式谱系PH中的$\Sigma^P_{2n+1}$类是完备的。为支持形式化模型和复杂性结果，我们使用重写逻辑工具Maude对有界时间验证进行了自动化实验。