Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)
When safety-critical systems are developed from a known internal specification, their correctness can be established by model checking. In the frequent case where such a specification is unknown or inaccessible, runtime verification presents an attractive alternative, e.g., to ascertain that autonomous and agentic syst...