The implementation of the semantics of the timed until in the STL discrete time monitor has two unnecessarily nested loops.
Specifically, the innermost loop at line 428 can be moved out of the loop and substituted with a suffix minimum of buffer_left. This can be created with a single iteration over the interval instead of iterating over the whole interval at each iteration to get the new minimum.
Also, it is worth converting the deque objects to lists for faster referencing in the subsequent loops.