Efficient Model Verification at Runtime through Adaptive Dynamic Approximation

TY - JOUR

T1 - Efficient Model Verification at Runtime through Adaptive Dynamic Approximation

AU - Alidoost Nia, Mehran

AU - Calinescu, Radu

AU - Kargahi, Mehdi

AU - Abate, Alessandro

N1 - Publisher Copyright: © 2025 Copyright held by the owner/author(s). Publication rights licensed to ACM.

PY - 2025/3/18

Y1 - 2025/3/18

N2 - In dynamic environments, safety-critical autonomous systems must adapt to environmental changes without violating safety requirements. Model verification at runtime supports adaptation through the periodic analysis of continually updated models. A major limitation of the technique is the high overhead associated with the regular analyses of large state-space models. Our article introduces an adaptive approximation strategy that tackles this limitation by delaying unnecessary model updates, significantly reducing the overheads of these analyses. The strategy is applicable to Markov decision processes (MDPs) and is partitioned into components that can be analyzed independently and approximately. Each component is assigned a priority that depends on its impact on the accuracy of verification, and only the highest-priority components affected by changes are scheduled for updating/approximating. A complete update and verification of the entire model is triggered infrequently when the accuracy drops below a predefined threshold. We provide theoretical guarantees and proofs which ensure that our strategy can be applied without impacting the overall safety of the verified autonomous system. The experimental results from a case study in which we applied the strategy to a rescue robot team show that it is fully robust against safety-critical errors and can achieve a decision accuracy of over 97%.

AB - In dynamic environments, safety-critical autonomous systems must adapt to environmental changes without violating safety requirements. Model verification at runtime supports adaptation through the periodic analysis of continually updated models. A major limitation of the technique is the high overhead associated with the regular analyses of large state-space models. Our article introduces an adaptive approximation strategy that tackles this limitation by delaying unnecessary model updates, significantly reducing the overheads of these analyses. The strategy is applicable to Markov decision processes (MDPs) and is partitioned into components that can be analyzed independently and approximately. Each component is assigned a priority that depends on its impact on the accuracy of verification, and only the highest-priority components affected by changes are scheduled for updating/approximating. A complete update and verification of the entire model is triggered infrequently when the accuracy drops below a predefined threshold. We provide theoretical guarantees and proofs which ensure that our strategy can be applied without impacting the overall safety of the verified autonomous system. The experimental results from a case study in which we applied the strategy to a rescue robot team show that it is fully robust against safety-critical errors and can achieve a decision accuracy of over 97%.

KW - formal approximation

KW - Markov models

KW - runtime model verification

KW - safety-critical systems

KW - self-adaptive systems

UR - http://www.scopus.com/inward/record.url?scp=105003490057&partnerID=8YFLogxK

U2 - 10.1145/3708560

DO - 10.1145/3708560

M3 - Article

AN - SCOPUS:105003490057

SN - 1556-4665

VL - 20

SP - 1

EP - 45

JO - ACM Transactions on Autonomous and Adaptive Systems

JF - ACM Transactions on Autonomous and Adaptive Systems

IS - 1

ER -