BDI agents

A BDI agent acts from three mental attitudes: what it believes about the world, what it desires, and what it has committed to — its intentions. The model comes from Michael Bratman’s philosophy of practical reasoning (1987) and was made precise by Anand Rao and Michael Georgeff (1991) as a modal logic. Hilbert takes that logic literally. An agent is a theory about itself: the compiler checks it against the BDI axioms, generates the inference engine that runs it, and refuses a plan network until the proof kernel has shown the plans cannot deadlock and do reach what the agent wants.

Three dialects work together:

Dialect	Says	Compiles to
`.ha`	the agent — beliefs, desires, intentions, commitment, attention, rewards	an inference engine that deliberates
`.hk`	the plans — communicating processes that change beliefs	a plan network, proved and then run
`.hb`	the values — how licensed choices are ordered	tensor formulas (Deliberation)

The theory

Let \(A\) be a set of agents, \(W\) a set of worlds and \(P\) a set of propositions, and let \(\mathrm{holds} \subseteq W \times P\) say which propositions are true at which world. For each agent \(i \in A\) let

\[R^B_i,\; R^D_i,\; R^I_i \;\subseteq\; W \times W\]

be its belief, desire and intention accessibility relations. Then for a proposition \(p\) and a world \(w\)

\[w \models B_i\,p \iff \forall u\,\big(w \mathrel{R^B_i} u \Rightarrow \mathrm{holds}(u, p)\big),\]

and likewise \(D_i\,p\) over \(R^D_i\) and \(I_i\,p\) over \(R^I_i\). “Agent \(i\) believes \(p\)” means \(p\) is true in every world \(i\) takes to be possible — not that a fact is stored somewhere. This is Agency.hs, and the axioms are properties of the relations:

Axiom	Frame condition	Reading
D (all three)	every world has an \(R\)-successor	no agent believes, desires or intends both \(p\) and \(\neg p\)
4 (belief)	\(R^B_i\) is transitive	an agent believes what it believes
5 (belief)	\(R^B_i\) is Euclidean	an agent believes what it does not believe
realism	\(R^D_i \subseteq R^I_i\)	\(I_i\,p \Rightarrow D_i\,p\) — an agent may not intend what it does not want

Belief is therefore KD45 and desire and intention are KD, which is Rao and Georgeff’s own assignment. Realism is written as an inclusion of relations rather than as a formula because, by correspondence theory, \(\Box_I p \Rightarrow \Box_D p\) holds exactly when \(R^D \subseteq R^I\) — and the inclusion is something the engine can check.

Commitment: how long an intention lasts

Bratman’s central point is that an intention resists reconsideration; an agent that re-decided everything every moment would have beliefs and desires but no intentions. How long the resistance lasts is the agent’s commitment strategy. Let \(X\) be “at the next step” and \(\Diamond p\) “\(p\) is still possible”. The three strategies, stated step by step over the trace the agent actually lives:

\[\begin{aligned} \textbf{blind:}\quad & I_i p \wedge \neg B_i p \;\Rightarrow\; X\, I_i p \\ \textbf{single-minded:}\quad & I_i p \wedge \neg B_i p \wedge \neg B_i \neg\Diamond p \;\Rightarrow\; X\, I_i p \\ \textbf{open-minded:}\quad & I_i p \wedge \neg B_i p \wedge D_i p \;\Rightarrow\; X\, I_i p \end{aligned}\]

A blind agent drops an intention only when it believes the goal achieved — even one it believes impossible.
A single-minded agent also drops it when it believes the goal cannot be reached. This is what practical BDI systems implement, and the strategy that makes an agent stop when the world turns against the plan.
An open-minded agent drops it when it no longer wants it — a change of mind, not of world.

Every agent declares exactly one. Note that each condition is about belief: an intention is released when the agent believes the goal met or unreachable, because an agent acts on what it takes to be the case.

An agent: `.ha`

A production line that makes three parts — unless it comes to believe the line is in danger, in which case it stops producing and makes the line safe:

-- Operator.ha
agent Operator(line: String) : Agency
{
  belief made(count: Int)
  belief alarm(state: String)
  belief safe(done: Int)
  belief halted(at: Int)

  desire Produced reachable by [Work]
  desire Safe reachable by [Stop]

  commit single_minded

  attention Producing initially
  attention Emergency

  intend Work for Produced when B(self) made(n) ∧ n < 3
  achieved Produced when B(self) made(3)

  impossible Produced when B(self) alarm("raised") because "the line is in danger, so production stops"
  when B(self) alarm("raised") attend Emergency
  intend Stop for Safe when B(self) alarm("raised")
  achieved Safe when B(self) safe(1)

  reward Stop positive when B(self) safe(1)

  plan Work ↦ Line.Produce
  plan Stop ↦ Line.Shutdown
}

Member	Meaning
`belief f(x: T)`	a proposition the agent may hold; conditions read it as \(B_{\mathrm{self}}\,f(x)\)
`desire D reachable by [P, …]`	a goal and the plans that may serve it
`commit s`	the commitment strategy: `blind`, `single_minded` or `open_minded`
`attention A initially` / `when φ attend A`	where the agent is looking, and what shifts its focus
`intend P for D when φ`	adopt plan \(P\) as the intention for \(D\) when \(\varphi\) holds
`achieved D when φ`	\(\varphi \Rightarrow B_{\mathrm{self}}\,D\) — releases the intention under every strategy
`impossible D when φ because "…"`	\(\varphi \Rightarrow B_{\mathrm{self}}\neg\Diamond D\) — releases a single-minded intention, with a reason a person can read
`reward P positive when φ`	a learning signal credited to the plan
`value v ≔ e`	Hilbert arithmetic used to order licensed choices
`plan P ↦ File.Plan`	the `.hk` plan (or host method) that runs when \(P\) is intended

The compiler refuses agents whose attitudes cannot hold together — for example a desire with no achieved rule, which could never be released. Conditions may compare numbers (n < 3) and combine beliefs with ∧ and ¬.

Plans: `.hk`

A plan is a process in Tony Hoare’s Communicating Sequential Processes. Plans talk over channels, run in parallel, change the agent’s beliefs, and can be stopped, resumed, aborted and restarted.

-- Line.hk
plan Feed(parts: chan Int) : Operator ≔ 1 → parts ; Feed(parts)

plan Build(parts: chan Int, made: Int) : Operator
{
  body ≔ match made { when 3 ↦ SKIP  other ↦ n ← parts ; forget made(made) ; believe made(made + n) ; Build(parts, made + n) }
  on abort ≔ believe halted(made)
}

plan Produce() : Operator
{
  parts : chan Int
  body ≔ believe made(0) ; (feed : Feed(parts) ‖ Build(parts, 0) ; abort feed)
  on abort ≔ believe halted(0)
}

plan Shutdown() : Operator ≔ believe safe(1)

Written	ASCII	Meaning
`v → c`	`v -> c`	send \(v\) on channel \(c\)
`x ← c`	`x <- c`	receive into \(x\)
`P ; Q`	`;`	\(P\), then \(Q\)
`P □ Q`	`[]`	external choice — whichever communicates first
`P ‖ Q`	`\\|\\|`	in parallel, synchronising on shared channels
`P △ Q`	`/\`	interrupt — \(P\) runs until \(Q\)’s first event, then \(Q\) takes over
`l : P`	same	a labelled process that commands can address
`believe φ` / `forget φ` / `tell j φ`	same	add a belief, remove one, inform another agent
`stop l` / `resume l` / `abort l` / `restart l`	same	control another plan (or `self`)
`on stop` / `on resume` / `on abort`	same	what a plan does when that command lands
`SKIP`, `STOP`	same	finish; deadlock

Commands land only at a communication, never in the middle of forget made(seen) ; believe made(seen + n), so a belief update is never half done.

The build proves the plans

For every plan an agent starts, the compiler explores every state the plan network can reach and hands the proof kernel obligations it must prove before the project builds. Compiling the two files above produces these theorems, all proved:

theorem Produce_no_deadlock  : ∀ w, produceReachable(w) ⇒ progress(w)
theorem Work_live_Produced   : inevitable(scene(call(Produce), empty), made(3))
theorem Shutdown_no_deadlock : ∀ w, shutdownReachable(w) ⇒ progress(w)
theorem Stop_live_Safe       : inevitable(scene(call(Shutdown), empty), safe(1))

_no_deadlock — every reachable state can move or has finished.
_live_<Desire> — on every path, the plan brings the agent to believe the achieved condition.
_released_<Desire> — wherever the agent believes the desire impossible, the plan’s abort finishes. It is generated when the impossible condition is one belief with constant arguments, as here, and it is proved over the scenes in which a plan itself raises that belief. In this example the alarm comes from outside — from sensors — so the compiler says, as warning HK0069, that the obligation holds without a proof in this network; the release is then enforced at run time by the commitment law (below).
_tell_feasible_<n> — before each tell j φ, the teller believes \(\varphi\) and does not believe \(j\) already does.

Two rules the compiler enforces: a plan an agent starts takes values, not channels (declare the channel inside the plan, as Produce does), and a plan may only believe facts its agent declares.

Deliberation: the theory licenses, the values order

Deliberation is split in two, and the split is the safety argument. The .ha theory computes which plans an agent may adopt — a licence mask \(m \in \{0, 1\}^k\) over \(k\) options. The Prelude’s Deliberation module orders the licensed options with values \(q \in \mathbb{R}^k\), learned or computed, by driving every unlicensed option to \(-\infty\) before a policy sees it:

\[\operatorname{licensed}(q, m) = m \odot q + (\mathbf{1} - m) \odot (-10^{300}), \qquad \operatorname{supp}(\pi) \subseteq \operatorname{supp}(m).\]

A policy \(\pi\) built this way — greedy, \(\varepsilon\)-greedy, softmax, upper-confidence — can choose a worse licensed plan if its values are poor, but never an unlicensed one. That is why learning is placed in plan selection: it can improve choices without being able to break the rules. leaked(π, m), the probability a policy puts on unlicensed options, is a number a test can require to be 0.

Running an agent

The runtime keeps the intention set as host state and drives the plans from it:

Event	Plan command
an intention is adopted	start the bound plan
the commitment law releases the intention (achieved, impossible, no longer desired)	abort it — its `on abort` runs
a higher intention takes over (a subgoal)	stop it, keeping its continuation
the subgoal is done	resume it where it stopped

Every command is journaled with the reason, so a run can be replayed. How often the agent deliberates again is a design parameter — David Kinny and Michael Georgeff showed in 1991 that neither extreme wins everywhere:

Policy	Deliberates	Suits
Bold	only when the running plan finishes	stable worlds — nothing changes under the plan
Cautious	every cycle	fast-changing worlds — a person typing, other agents acting
OnChange	when a named condition has changed	the practical middle — reconsider on evidence

These policies are provided by the runtime (MLambda.Hilbert.Runtime.Agency.Reconsideration) and chosen by the host; there is not yet a .ha keyword for them.

Continue with Reactive, deliberative and the LLM to see how an agent stops when it is in danger, thinks, and uses a language model — safely.