Assumption-Based Runtime Verification of Infinite-State Systems

Runtime Verification (RV) basically means monitoring an execution trace of a system under scrutiny and checking if the trace satisfies or violates a specification. In Assumption-Based Runtime Verification (ABRV), runtime monitors may be synthesized from not only the specification but also a system model (either full or partial), which represents the assumptions on which the input traces are expected to follow. With assumptions the monitor can additionally check if the input traces actually follow the assumptions. Some previous research has shown that monitors under assumptions can be more precise or even predictive, while non-monitorable specifications may become monitorable under assumptions. The question of synthesizing runtime monitors for finite-state systems and propositional or first-order temporal logics, with or without assumptions, has mostly been answered by prior work. For monitoring infinite-state systems, however, most existing approaches focus on supporting parametric or first-order specifications while they cannot be easily extended to support assumptions. This paper presents a general solution for ABRV of infinite-state systems by a reduction of RV problems to LTL Model Checking (MC), which is further based on Satisfiability Modulo Theories and other techniques. When First-Order Quantifier Elimination (QE) is also available, the corresponding algorithm can be greatly optimized. This solution is general because in theory any LTL MC (and QE) algorithms can be used, and the supported types of infinite-state variables also depend on these underlying algorithms. In particular, the relatively expensive model checking can be minimized by a modified version of Bounded Model Checking algorithm which performs model checking incrementally on each input of the monitor.