Progression alternative improves monitoring safety properties with arithmetic constraints

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

Logic in Computer ScienceArtificial Intelligence

Summary

When systems that can affect safety do not have a clear internal blueprint, checking their behavior while they run can help ensure they meet safety and correctness rules. The paper looks at ways to watch system actions and predict if problems might happen by considering both what has happened and all possible future events. Typical methods use complex automata that can be slow or not finish, especially when math conditions are involved. The authors propose a different approach based on progressing the rules forward and checking satisfiability, which often works better in practice, especially for math-based rules. They test and compare methods, finding that a hybrid of both approaches balances performance well for simpler cases.

What this means in practice

  • For autonomous system engineers: Enable real-time monitoring of autonomous systems to detect potential safety violations involving arithmetic conditions faster and more reliably than previous automata-based methods.
  • For business process managers: Implement runtime checks on business workflows that incorporate quantitative constraints to ensure compliance with rules dynamically and efficiently.

Authors

Sarah Winkler, Toryn Klassen, Sheila McIlraith, Marco Montali

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.
View PDFOpen arXiv