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