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

1 Introduction

• Autonomous systems may need to act independently in remote or dangerous environments, or where interactions are too complex or fast for humans to handle.Examples include deep-sea exploration, space probes, contaminated-area cleanup, stock trading, robot swarms, and collision avoidance.Source: §1 · p. 3

1.1 Hybrid Autonomous Systems

• Hybrid automata make it difficult to separate decision-making from continuous control, while verification becomes difficult to apply and scales poorly as reasoning grows more complex.This separation affects design, code, understandability, reuse, and access to explanations for decisions.Source: §1.1 · p. 3

1.2 A Methodology for Verifying Autonomous Choices

• The proposed methodology model-checks a rational agent’s choices against its beliefs, including whether it avoids options it believes unsafe.It focuses on the agent’s internal decisions rather than verifying all real-world effects, relying on analysis of the underlying control system for action outcomes.Source: §1.2 · pp. 3–4

1.3 Autonomy in the Real World

• The approach abstracts from continuous behavior by exploring possible perception inputs, making environmental assumptions explicit and supporting compositional analysis of multi-agent systems.Individual agents can be checked separately and their results combined deductively to establish properties of the whole system.Source: §1.3 · pp. 4–5

1.4 Overview

• The methodology preserves the system’s natural decomposition, verifies symbolic and non-symbolic aspects separately, and makes assumptions about the real-world environment explicit.Its workflow models the agent and interface, checks the agent under a coarse environment approximation, uses environmental hypotheses when available, and combines individual-agent results deductively.Source: §1.4 · p. 5

2.1 Hybrid Control Systems

• Hybrid-automata implementations can hinder separation of decision algorithms from continuous control, reducing code understandability and reuse; they also scale poorly as decision-making complexity grows compared with agent-based control.Source: §2.1 · p. 6

2.2 Agents and Rational Agents

• Rational agents make choices for explicit reasons, supporting explanation to users and high-level reporting for certification, accidents, or near misses.In the BDI model, beliefs represent possibly incomplete or incorrect information, desires are long-term goals, and intentions are goals actively pursued.Source: §2.2 · p. 7, §2.2.1 · p. 7

2.2.1 BDI Agents and Programming Languages

• BDI-style languages and platforms include AgentSpeak, Jason, 3APL, Jadex, Brahms, GOAL, and GWENDOLEN; plans guide action from beliefs and goals and can change them.Agent-based hybrid control has been explored from MAHCA’s knowledge-based planners to spacecraft, unmanned aircraft, and robotics.Source: §2.2.1 · pp. 7–8, §2.2.2 · p. 8

2.3 Formal Verification and Model Checking

• Model checking checks a logical property against all executions of an executable model, while program model checking can exhaustively analyze actual Java executions through JPF.Program model checking avoids an extra abstraction layer but is typically slower than standard model checking.Source: §2.3 · p. 8

2.4 Verifying Hybrid Systems

• Hybrid-automata verification is hard to decompose, constrained by decidable fragments such as linear automata, and scales poorly with large discrete state spaces.Trajectory calculations depend on possible entry values, often requiring exploration of the whole automaton and limiting reuse; linear fragments also restrict logical formulas to conjunctions of inequalities.Source: §2.4 · p. 9

2.4.2 Solutions to the Modeling Problem

• Hybrid automata model computational and physical behavior together, so verification typically checks a model rather than the implementation; certification may require compiling the implementation and environment into an automaton.When complex decisions are abstracted as nondeterministic outcomes, verification can include states the real decision process would veto, producing false negatives.Source: §2.4 · pp. 9–10

2.4.1 Approaches to Compositionality and Expressivity

• PHAVER’s assume-guarantee approach abstracts composed subsystems for verification but retains linear-hybrid-automata limits and can return false negatives; KeYmaera supports more expressive hybrid programs but complex decisions remain cumbersome.Higher-level-language compilation has focused on synchronous languages such as LUSTRE and Quartz, while no system had compiled agent-based control into hybrid automata.Source: §2.4.1 · p. 10, §2.4.2 · pp. 10–11

2.5 Model Checking Agent Programs

• The MCAPL framework provides model checking for BDI programs through AIL interpreters and AJPF, and its general verification methodology does not depend on that framework.AJPF builds on JPF and can check AIL-based agents, including whole systems when their environment is programmed in Java; its property language combines temporal operators with belief, goal, action, intention, and percept modalities.Source: §2.5 · p. 11, §2.5.1 · p. 11, §2.5.2 · p. 12

2.5.2 Temporal and Modal Logics and the MCAPL Property Specification Language

• The Boolean semantics define disjunction as satisfaction of either operand and negation as failure to satisfy the operand.Source: §2.5.2 · p. 13
• MCAPL temporal formulae apply to JPF runs of program states, with the number of distinct states assumed finite for model checking.A run may be infinite and begins at the program’s initial state.Source: §2.5.2 · p. 13
• The U and R operators define temporal properties over runs, while eventually and always are derivable from them.The U definition requires ψ to hold at some state after ϕ holds at every earlier state; R specifies its release condition.Source: §2.5.2 · p. 13
• Future work includes adding knowledge and coalition modalities and investigating alternative logics for model checking autonomous systems.The proposed modalities would describe information evolution and cooperative systems [5].Source: §2.5.2 · p. 13

2.6 Abstracting from the Real World

• The approach chooses discrete decision states by accounting for all possible physical-environment responses and communications from other agents.These abstractions relate the continuous world to agent decisions.Source: §2.6 · pp. 13–14
• Using the abstractions, the approach defines basic behavior rules and goals that keep the system within constraints and set short- and long-term objectives.Goals, plans, and logical inference are captured within the rational agent.Source: §2.6 · p. 14
• Abstractions translate quantitative sensor data, such as precise coordinates, into qualitative facts relevant to reasoning, such as whether a vehicle is within desired bounds.The control system may need exact coordinates even when the reasoning system only needs a within-bounds condition.Source: §2.6 · p. 14
• The rational-agent architecture uses an abstraction engine to discretize continuous information explicitly for verification; the engine is currently a distinct agent, with stream processing planned for the future.The paper describes this as an architecture it has been exploring.Source: §2.6 · p. 14
• Hybrid-system model checking commonly partitions continuous search spaces into finite regions so a checker can trace a finite set of paths through a simpler representation.Such abstractions aim to preserve key features of the world.Source: §2.6 · p. 14
• The method uses a coarse abstraction that over-approximates the real world and primarily verifies decision-making algorithms, rather than the whole system.Where an explicit abstraction engine exists, it forms this coarse abstraction; the paper says the approach resembles PHAVER but does not decompose the system into parallel hybrid automata.Source: §2.6 · p. 14

3 Scenario: Urban Search and Rescue

• On a grid-based rescue task, a robot searches for humans by exploring squares; the scenario supports individual and cooperative behaviours.Robots detect a human when it is in the same grid square.Source: §3 · pp. 14–15

3.1 Implementation

• The GWENDOLEN searcher pursues the goal of leaving only when it believes it has found a human or that the area is empty.Its plans have a trigger, belief-based guard, and action-and-belief body; the interpreter polls sensors for perceptual belief changes.Source: §3.1 · pp. 15–16

3.2 Verification

• AJPF automatically verified the searcher’s specified properties under an explicit model that supplies possible incoming perceptions.The model supplies relevant inputs randomly and makes perception choices and their possible timing explicit.Source: §3.2 · p. 16

3.2.1 Deduction using Environmental Assumptions

• A proof that the robot will find a human follows from verified agent reasoning only under assumptions such as accurate sensors and motors and a stationary human.The proof fails without the stationary-human assumption, because eventual co-location cannot then be established.Source: §3.2.1 · p. 17

3.2.2 Multi-Agent Systems

• The searcher’s reasoning and the lifter’s response can be checked separately, then combined deductively to conclude that a received message eventually leads the lifter to believe the human is free.This compositional approach keeps the automata and search spaces smaller than checking the agents together.Source: §3.2.2 · p. 18

3.2.3 Goals and Intentions

• For the lifter, verification establishes that a belief about the human’s location leads eventually to an intention to free them; stronger conclusions depend on assumptions about perception.If forming that intention is assumed to lead eventually to believing the rubble is clear, a message from the searcher eventually leads to belief that the human is free.Source: §3.2.3 · pp. 18–19

4 Scenario: Rational Hybrid Agents for Autonomous Satellites

• The space industry has sought to replace large, tightly controlled satellites with teams of smaller, more autonomous satellites accomplishing larger vehicles’ tasks through distributed methods.Their cooperation, autonomy, mission-critical aspects, and real-world interaction make satellite systems a test-bed for analysing autonomous systems.Source: §4 · p. 19

4.1 System Architecture

• The architecture separates a BDI reasoning engine from control engines and uses an abstraction layer to translate continuous system information into discrete information for decisions.The reasoning engine can request calculations or physical actions through the abstraction engine, which also discretizes continuous results as shared beliefs.Source: §4.1 · p. 20, §4.1.1 · p. 20, Figure 2 · p. 21

4.1.1 Semantics of Interaction

• The abstraction engine filters real-world sensor perceptions into discrete shared beliefs, which define the inputs relevant to checking the reasoning engine.Shared beliefs are the agents’ common discrete understanding of the world.Source: §4.1.1 · p. 20

4.1.2 System Implementation

• The implemented architecture was deployed on satellite hardware test facilities and in simulations, but this paper verifies only the reasoning engine and does not examine separate whole-system testing.The physical and continuous engines were implemented in MATLAB; the abstraction and reasoning engines used a customized GWENDOLEN variant.Source: §4.1.2 · p. 20

4.2 Adapting the System for Model Checking

• Because communication between the reasoning engine and the physical and continuous engines passes through the abstraction engine, verification can focus on the abstraction and reasoning engines.The possible shared beliefs and messages can be read from the abstraction code and agent communications to define the reasoning engine’s inputs.Source: §4.2 · p. 22
• The verification environment asserts and retracts shared beliefs and messages, generating new sets randomly so the model checker explores all possible outcomes.The setup assumes reasoning is instantaneous and permits perception changes only when the reasoning engine acts; this limits the search space.Source: §4.2 · p. 22

4.3 Example: Autonomous Satellites in Low Earth Orbit

• The LEO scenario addresses restricted ground-station visibility by modelling satellites moving to formation positions and correcting a single fuel-line failure.LEO satellites complete an orbit in about 90 minutes, while ground-station visibility lasts 5–15 minutes per overhead passage.Source: §4.3 · p. 22, §4.3.1 · pp. 22–23

4.3.2 Implementation and Testing

• The system was tested in SIMULINK and a physical satellite simulation environment, with injected hardware failures in simulation and path-following failures in physical tests.Source: §4.3.2 · p. 23

4.3.4 Analysis of Multi-Agent Models and Communication

• The analysis limits possible inputs to manage combinatorial growth and excludes unknown or conflicting messages from potentially malicious agents.Construction time also depended on the complexity of generating new agent-code states.Source: §4.3.3 · pp. 24–25, §4.3.4 · p. 27

4.3.3 Analysis of a Single Satellite Agent

• Model checking exposed rapidly changing fault-report edge cases missed by simulation and testing, prompting additional plans in the final agent code.Examples include an abort followed by a newly reported broken thruster, and a successfully fixed thruster reported broken again.Source: §4.3.3 · p. 24
• Under assumptions about plan receipt and execution, the analysis connects the agent's belief in reaching the middle position to maintaining that position.Combining the checked result with correct-sensor analysis could extend the theorem to guarantee actual arrival.Source: §4.3.3 · pp. 24–25
• With planning success, x-thruster fixability, and successful fuel-line changes assumed, the agent eventually believes it maintains position; the checked property excludes y- and z-thruster failures.Including those additional thrusters made the automaton too large to construct in reasonable time.Source: §4.3.3 · p. 26

4.3.4 Analysis of Multi-Agent Models and Communication

• If all agents respond, the leader eventually believes a line formation is achieved, and the checked safety properties rule out assigning one agent to two positions or two agents to one position.The follower's eventual report that it is maintaining position is conditional on successful planning and execution.Source: §4.3.4 · pp. 27–28
• With all agents responding, the leader eventually believes a square formation is achieved and, whenever it believes the agents are in square formation, eventually believes they are in line formation.Source: §4.3.4 · p. 29

• Figure 4 models repeated discrete-control and dynamic-control cycles, with the follower’s acceleration choices constrained by safety and vehicle state.The dynamic part specifies position and velocity changes using standard equations of motion.Source: §5 · p. 30, Figure 4 · p. 30
• Representing more complex car control in hybrid programs is possible, but cumbersome because the language remains low-level.The described control uses nondeterministic choices over legal states and does not include goals in its decision constraints.Source: §5 · p. 30
• In single-lane cruise control, whenever the agent accelerates, it believes it is a safe distance from the car ahead.The agent is checked against constraints previously verified by Loos et al. [65].Source: §5 · p. 31
• For lane changes, the agent follows leftmost-lane and right-side-overtaking rules, with beliefs and goals governing when it switches contexts.The implementation handles changing situations by allowing goals to be dropped even if they have not been achieved.Source: §5 · pp. 31–32
• The agent changes lanes only when it believes the move is safe, in both directions.The verification checks adherence to the discrete-control constraints, assuming ‘safe’ is calculated correctly; it does not redo the full safety analysis.Source: §5 · p. 32

6 Concluding Remarks

• The compositional method model-checks a rational agent’s reasoning, avoids complex opaque external-system models, and combines results deductively with full-system results.This is presented as a feasible way to provide formal analysis of the whole system.Source: §6 · p. 32
• Different techniques suit different hybrid-system aspects: program model checking fits rational-agent code, while probabilistic, analytical, and deductive methods may better suit continuous domains.The methodology is also proposed for complex discrete control beyond rational-agent implementations.Source: §6 · p. 32
• Properties were proved for three examples—a RoboCup Rescue program, satellite-control code, and adaptive cruise control—without detailed formal analysis of real-world continuous aspects.The property language refers to agents’ beliefs, goals, and actions, limiting the theorems to agent internals.Source: §6 · p. 34
• Abstracting away continuous behavior can admit sensor inputs that may not make sense in the continuous system, and expanding input possibilities increases the search space.The paper notes that contradictory braking and acceleration reports could also arise from a malfunctioning sensor; input growth and program-model-checking inefficiency limit scope.Source: §6 · p. 34
• The authors seek to extend verification to probabilistic guarantees about sensor reliability and action success, building on initial AJPF–PRISM investigation.Their example specifies 98% sensor correctness and action success, with a 97% guarantee against the agent believing it reached a bad state.Source: §6 · p. 34
• Percepts were selected by hand in the examples; the authors propose automating selection to help ensure potential inputs are not overlooked.They also propose abstract automata to control state counts as sensor values grow, and identify cooperative, communicating, learning agents as further work.Source: §6 · pp. 34–35

A.1 A Satellite Agent

• The agent directly controls one satellite and receives formation information from a separate coordinating leader agent.Source: §A.1 · p. 41

A.1.1 The Abstraction Engine

• The Abstraction Engine uses a GWENDOLEN variant in the example, with shared-belief addition and removal constructs; stream-processing languages for this engine remain under investigation.The authors consider BDI-style programming appropriate for the Reasoning Engine.Source: §A.1.1 · p. 41
• Location percepts prompt a distance calculation against the desired position, and the result updates a shared belief about whether the satellite is in position.Source: §A.1.1 · p. 41
• Thruster percepts include fuel-line pressures, current, and voltage; output pressure below 1 leads the agent to assert a shared belief that the thruster is broken.The engine can retract that belief when the pressure is no longer below the threshold.Source: §A.1.1 · p. 41
• Reification translates Reasoning Engine requests into calculations or actions, including setting valves and updating shared beliefs about fuel lines and thruster status.The housekeeping code also abstracts specific thruster information into generic information and handles waiting.Source: §A.1.1 · pp. 41–42

A.1.2 The Reasoning Engine

• The Reasoning Engine’s actions and queries send goal requests to the Abstraction Engine, while queries suspend plan execution until a response belief arrives.The code uses a belief rule to deduce that a thruster failure is repairable when it is using the first fuel line.Source: §A.1.2 · p. 42
• Achieve goals persist until believed true and may trigger plans repeatedly, whereas perform goals disappear after execution without an implicit success check.Source: §A.1.2 · p. 42
• The agent can start formation assumption itself or receive it as a request, and it handles leader instructions to abandon the current formation attempt.Source: §A.1.2 · p. 42
• New leader-supplied position beliefs become the agent’s desired position, and once adopted, later suggestions are not accepted.The code also handles moving to a position using either a requested plan or an existing plan.Source: §A.1.2 · p. 42
• Position maintenance is pursued as an achieve goal; the agent waits for a broken thruster to be fixed unless aborted, then can resume or wait for new instructions.Thruster failures are handled by attempting repair or aborting; an abort drops maintenance goals and stops the maneuver.Source: §A.1.2 · pp. 42, 44
• The architecture represents high-level decisions through agent beliefs, goals, and observed events, with thruster-failure beliefs prompting fuel-line changes and valve actions.Source: §A.1.2 · p. 44

A.2 A Leader Agent

• The desired-formation rules support either attempting only a line or trying a square first and then changing to a line.The one-formation belief selects between these configurations, allowing different agents to be generated from the same code.Source: §A.2 · p. 44
• Formation selection and cleanup of old choices are handled in lines 15–24, with cleanup sub-plans not shown.The passage describes this portion of the listing without detailing the omitted sub-plans.Source: §A.2 · p. 44
• The leader informs agents which formation to adopt and waits for them to report that they have reached their positions.It chooses positions for all agents before communicating the adopted formation.Source: §A.2 · p. 44
• The leader assigns each available agent to an unassigned formation position and informs that agent of its position.The assignment goal remains selected until no available agent or unassigned position remains.Source: §A.2 · p. 44
• The presented listing omits follower messages reporting failures and aborts, which are excluded from the verification discussion.The description is simplified relative to the actual code.Source: §A.2 · p. 44

B Adaptive Cruise Control: The Abstraction Engines

• The single-lane engine receives car speed, pedal-driven acceleration, and whether the distance to the car ahead is safe as sensor inputs passed to the reasoning engine as shared beliefs.When the driver is using a pedal, its values govern acceleration or braking; otherwise, a simple command and a random simulation value are used.Source: B Adaptive Cruise Control: The… · pp. 44, 47
• In the single-lane example, sensor events update safe-distance and speed-limit beliefs, while reasoning-engine instructions trigger braking, acceleration, or speed maintenance.The plans use driver pedal values when available and otherwise invoke simple accelerating or braking behavior.Source: B Adaptive Cruise Control: The… · p. 47
• The lane-changing engine receives the car’s lane, distances to cars ahead in the current and left lanes, and whether the car is crossing lanes.The agent also starts with a belief about how close another car must be to justify initiating an overtaking maneuver.Source: B Adaptive Cruise Control: The… · p. 47

C Logics Workbench Input

• The examples encode agent concepts as propositions, abbreviating beliefs and locations such as Bs human as bh and at(robot,0,0) as ar00.The resulting propositions are used to represent the hypotheses and theorems in the workbench.Source: C Logics Workbench Input · p. 47
• The workbench is used to prove each defined hypothesis and theorem with the provable command.The paper shows a property about finding a human expressed using mc_thm, correct_sensors, correct_movement, and cond.Source: C Logics Workbench Input · pp. 47, 49
• The proof of theorem (10) uses assumptions for sending, receiving, and reliable communications to establish that a found human is eventually freed.The passage identifies the propositions as Bs found, Bs sent, Bl rec, and Bl free, respectively.Source: C Logics Workbench Input · p. 49