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 work, we study the computational complexity of a formalization of time-bounded resilience problems for the class of progressing timed systems (PTS), where, intuitively, 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 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.

翻译：大多数关于形式化系统设计的研究都集中在优化各种效率指标上。然而，针对系统韧性（即系统适应意外变化或对抗性干扰的能力）的设计优化，迄今尚未得到足够重视。在先前的工作中，我们通过使用带显式时间的多重集重写语言，将韧性的直观概念形式化为信息物理系统的一种属性。在本研究中，我们针对进展型计时系统（PTS）类，研究了时间有界韧性问题的形式化计算复杂性——这类系统在直觉上仅能在有界时间间隔内执行有限数量的动作。我们证明，在具有n次（可能由对抗性选择的）更新的时间有界模型中，相应的时间有界韧性问题对于多项式层次结构PH中的$\Sigma^P_{2n+1}$类是完备的。为支撑形式化模型和复杂性结果，我们使用重写逻辑工具Maude开展了时间有界验证的自动化实验。