Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregationsby Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider and Dmitriy Traytel09 Apr