aiqbench analysis
This research advances runtime verification for autonomous systems by introducing a progression-based method that overcomes the computational limits of traditional automata approaches when checking linear-time properties with arithmetic constraints. The study demonstrates that this alternative technique successfully generates safety verdicts in scenarios where standard methods fail to terminate, offering a more robust solution for verifying agentic AI behaviors without internal specifications.
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, runtime verification presents an attractive alternative, e.g., to ascertain that autonomous and agentic systems as well as business processes satisfy desirable properties and/or comply with safety requirements. In this paper we study anticipatory monitoring, an advanced form of runtime verification, where the monitoring state is determined by both the trace prefix seen so far, and all its possible finite-length, future continuations. We focus on monitoring linear-time properties that may involve arithmetic constraints. Automata-based approaches, the de-facto standard in this setting, are notorious for their computational complexity. We propose an alternative approach based on progression and LTLf satisfiability checking, for both propositional and arithmetic settings. We experimentally compare the automata- and progression-based approaches, and a third method that combines the two. Our experiments suggest that the progression-based approach often succeeds in producing a verdict when the automata constructions do not terminate, especially for the arithmetic setting. For the propositional setting, the combined technique provides a good tradeoff.
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, runtime verification presents an attractive alternative, e.g., to ascertain that autonomous and agentic systems as well as business processes satisfy desirable properties and/or comply with safety requirements. In this paper we study anticipatory monitoring, an advanced form of runtime verification, where the monitoring state is determined by both the trace prefix seen so far, and all its possible finite-length, future continuations. We focus on monitoring linear-time properties that may involve arithmetic constraints. Automata-based approaches, the de-facto standard in this setting, are notorious for their computational complexity. We propose an alternative approach based on progression and LTLf satisfiability checking, for both propositional and arithmetic settings. We experimentally compare the automata- and progression-based approaches, and a third method that combines the two. Our experiments suggest that the progression-based approach often succeeds in producing a verdict when the automata constructions do not terminate, especially for the arithmetic setting. For the propositional setting, the combined technique provides a good tradeoff.
Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI)
arXiv:2609.32912 [cs.LO]
(or arXiv:2609.32912v1 [cs.LO] for this version)
https://doi.org/10.48550/arXiv.2609.32912 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 285 words
Related coverage
When Automata Meet Streams: Temporal Logic Compilation for Stream-Based Robotics Task and Motion Planning
arXiv · Aug 21, 2026
Neuro-Symbolic Injection of LTLf Constraints in Autoregressive Reinforcement Learning Policies
arXiv · Jun 9, 2026
Automata from Agent Traces: Failure and Next-Step Prediction
arXiv · Aug 27, 2026
[AINews] not much happened today
Latent Space · Sep 18, 2026