Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version).

arXiv:2609.32912v1 Announce Type: cross Abstract: 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