Run-time Quantitative Operational Monitoring for BDI Agents
TL;DR
This paper proposes a run-time quantitative operational monitoring methodology based on Discrete-Time Markov Chains (DTMCs), integrating execution traces with probabilistic model checking, and advances agent verification from pre-deployment analysis to ongoing quantitative assurance under uncertainty.
Abstract
The BDI (Belief-Desire-Intention) agent paradigm has been used to model decision-making in autonomous systems that operate with little to no human intervention, reasoning with beliefs, desires, and intentions on-the-fly to achieve goals. Since BDI agents are used to make decisions in safety-critical systems, verifying that they make correct decisions is vital. Existing design-time verification techniques are effective before deployment, but they cannot capture how agent behaviour evolves during execution, especially under imprecise actuation and probabilistic decision-making. This paper bridges the gap between design-time and run-time verification of probabilistic BDI agents. We propose a run-time quantitative operational monitoring methodology based on Discrete-Time Markov Chains (DTMCs), integrating execution traces with probabilistic model checking. Our approach constructs a DTMC representation of possible agent behaviours at design time, then incrementally updates it using observed execution traces to provide situational insight into agent operation. To demonstrate our work, we contribute a probabilistic BDI language extension, explicate our approach through smart manufacturing for probabilistic BDI agents, and use a rover case study to show the generality of our DTMC-based monitoring. We further implement this monitoring mechanism and evaluate its efficiency and scalability experimentally. This advances agent verification from pre-deployment analysis to ongoing quantitative assurance under uncertainty.