We consider the problem of Runtime Verification (RV) based on Propositional Linear Temporal Logic (LTL) with both future and past temporal operators. We generalize the framework to monitor partially observable systems using models of the system under scrutiny (SUS) as assumptions for reasoning on the non-observable or future behaviors of the SUS. The observations are generic predicates over the SUS, thus supporting both static and dynamic sets of observables. Furthermore, the monitors are \emph{resettable}, i.e. able to evaluate the monitoring properties at arbitrary positions of the input trace (roughly speaking, [u,i |= phi] can be evaluated for any u and i with the underlying assumptions taken into account). We present a symbolic monitoring algorithm that can be efficiently implemented in BDD. It is proved correct and the output monitor is double-checked by model checking. As a by-product, we also give the first automata-based monitoring algorithm for Past-Time LTL. Beside showing the feasibility and effectiveness of our RV approach, we also demonstrate that, under certain assumptions the resulting monitors are predictive.
Assumption-Based Runtime Verification with Partial Observability and Resets