Temporal Monitoring of Agent Beliefs Under Uncertainty with Subjective LTL

Abstract

ML-based agents acting in open environments must form and revise beliefs under pervasive perceptual and epistemic uncertainty. Verifying such agents over time therefore requires reasoning about how their uncertain beliefs evolve. However, existing temporal verification and monitoring frameworks -- including probabilistic and multi-valued logics -- typically reason about Boolean or graded truth of propositions along system runs, rather than about an agent’s internal belief state. We propose Subjective LTL (SLTL), a temporal specification language whose atomic propositions are Subjective Logic opinions, i.e., tuples of belief, disbelief, and uncertainty about predicates in an agent’s symbolic knowledge model. Under an evidential semantics, temporal operators aggregate evidence over time about persistent hypotheses, so SLTL formulas constrain how the agent’s belief state should evolve. This supports temporal verification and monitoring directly over the dynamics of knowledge-grounded, uncertainty-aware agents, and can equally be used to equip such agents with introspective monitors over their own evolving beliefs, which we illustrate on a simple example.