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进行了时间有界验证的自动化实验。