2024/01/10 by Tajana Ban Kirigin, Jesse Comer, Kirigin, Tajana Ban +7
Computer Science · Mathematics · #Algorithm #Artificial intelligence #Bounded function #Class (philosophy) #Complexity class #Computer science #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Hierarchy #Logic in Computer Science (cs.LO) #Mathematics #Model checking #Polynomial hierarchy #Programming language #Resilience (materials science) #Rewriting #Security and Verification in Computing #Simple (philosophy) #Theoretical computer science #Time complexity
paper · pdf · doi:10.48550/arxiv.2401.05585
openalex publication_date 2024/01/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 η-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 ΣP2n+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.