# Practical Verification of Decision-Making in Agent-Based Autonomous Systems

arXiv: https://arxiv.org/abs/1310.2431 · HTML: https://mlsanity.com/paper/1310.2431/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Oct 2013.

## Built on by (most cited first, 11 of 11)

- [Vibe Coding vs. Agentic Coding: Fundamentals and Practical Implications of Agentic AI](https://mlsanity.com/paper/2505.19443/) (2025)
- [Auditing of AI: Legal, Ethical and Technical Approaches](https://mlsanity.com/paper/2407.06235/) (2024)
- [Soda: An Object-Oriented Functional Language for Specifying Human-Centered Problems](https://mlsanity.com/paper/2310.01961/) (2023)
- [HARMONIC: A Framework for Explanatory Cognitive Robots](https://mlsanity.com/paper/2409.18037/) (2024)
- [Ensuring trustworthy and ethical behaviour in intelligent logical agents](https://mlsanity.com/paper/2402.07547/) (2024)
- [HARMONIC: Cognitive and Control Collaboration in Human-Robotic Teams](https://mlsanity.com/paper/2409.18047/) (2024)
- [Model Checking for Closed-Loop Robot Reactive Planning](https://mlsanity.com/paper/2311.09780/) (2023)
- [Towards Developing Ethical Reasoners: Integrating Probabilistic Reasoning and Decision-Making for Complex AI Systems](https://mlsanity.com/paper/2502.21250/) (2025)
- [Real-Time Model Checking for Closed-Loop Robot Reactive Planning](https://mlsanity.com/paper/2508.19186/) (2025)
- [HARMONIC: A Content-Centric Cognitive Robotic Architecture](https://mlsanity.com/paper/2509.13279/) (2025)
- [Evaluation of AI Ethics Tools in Language Models: A Developers' Perspective Case Study](https://mlsanity.com/paper/2512.15791/) (2025)

## Abstract (arXiv)

We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.