Shrinking Mission-time LTL Runtime Monitors with Equality Saturation

Abstract

Runtime Verification (RV) verifies safety-critical systems in real time, often under hard time and space constraints that only become more restrictive as systems grow in complexity. Equality Saturation (EqSat) is an algorithm that efficiently optimizes programs via rewriting thus reducing their cost in terms of time and memory. We propose applying EqSat to RV to automatically reduce the resource usage of RV monitors, enabling more efficient deployment in resource-constrained environments. In particular, we target the flight- and space-certified RV framework R2U2 and adapt EqSat for its specification logic, Mission-time LTL (MLTL). We then extract a resource-reduced MLTL formula from the output of EqSat using an Integer Linear Programming (ILP) encoding and offer an alternative, more-efficient greedy extraction method. We implement this approach in a fully-automated toolchain that applies EqSat to an input formula using the off-the-shelf tool EggLog, performs ILP-based extraction via Gurobi, and outputs an MLTL formula optimized for R2U2 resource usage. Experimental evaluation demonstrates memory reduction for 61% of 1,177 real-world RV benchmarks by an average of 22%. On balance, we find that applying EqSat using the greedy extraction method and associative/commutative rewrites disabled provides the best approach that effectively reduces R2U2 resource usage while maintaining low optimization overhead.