1

arXiv:1803.09099v1 [] 24 Mar 2018

A Resourceful Reframing of Behavior Trees
CHRIS MARTENS, North Carolina State University
ERIC BUTLER, University of Washington
JOSEPH C. OSBORN, University of California, Santa Cruz
Designers of autonomous agents, whether in physical or virtual environments, need to express nondeterminisim, failure, and parallelism in behaviors, as well as accounting for synchronous coordination between
agents. Behavior Trees are a semi-formalism deployed widely for this purpose in the games industry, but with
challenges to scalability, reasoning, and reuse of common sub-behaviors.
We present an alternative formulation of behavior trees through a language design perspective, giving a
formal operational semantics, type system, and corresponding implementation. We express specifications
for atomic behaviors as linear logic formulas describing how they transform the environment, and our type
system uses linear sequent calculus to derive a compositional type assignment to behavior tree expressions.
These types expose the conditions required for behaviors to succeed and allow abstraction over parameters to
behaviors, enabling the development of behavior “building blocks” amenable to compositional reasoning and
reuse.
Additional Key Words and Phrases: linear logic, behavior trees, programming languages, type systems
ACM Reference format:
Chris Martens, Eric Butler, and Joseph C. Osborn. 2016. A Resourceful Reframing of Behavior Trees. 1, 1,
Article 1 (January 2016), 17 pages.
DOI: 10.1145/nnnnnnn.nnnnnnn

1

INTRODUCTION

Specifying the desired behaviors of agents in environments is a major theme in artificial intelligence.
Analysts often need to define particular policies with explicit steps, but the agents must also
acknowledge salient changes in a potentially hostile or stochastic environment. This challenge
arises in applications including robotics, simulation, and video game development. Games in
particular bring challenges related to interaction with human decision-makers: even for games
notionally working against the objectives of the player, the activity of game design is centrally
concerned with helping the player learn something or have an emotional experience, and in this
sense can be thought of as a cooperative system between agents with different knowledge states,
not unlike human-robot teams. The behaviors of non-player characters (NPCs) in games must be
designed in support of this goal.
Game designers must be able to specify that a given agent should patrol a hallway until it gets
hungry (or its battery runs low) and goes home for a snack (or to recharge); but if the agent sees a
one-hundred dollar bill on the ground on the way to where it recuperates, it should force a detour.
In some designs, we would want an adversary (e.g., the player) to be able to trick the agent into
running out of fuel by this mechanism; in other designs we would hope the agent ignores optional
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and
the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored.
Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires
prior specific permission and/or a fee. Request permissions from permissions@acm.org.
© 2016 ACM. XXXX-XXXX/2016/1-ART1 $15.00
DOI: 10.1145/nnnnnnn.nnnnnnn

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:2

Chris Martens, Eric Butler, and Joseph C. Osborn

but attractive diversions and prioritizes severe need. We can easily imagine two distinct agents
within the same game which are differentiated only by whether they can be misled in such a way.
Game character AI designers have somewhat contradictory goals that distinguish their project
from, for example, game-playing AI whose objective is optimal play. On the one hand they want
believable characters who react reasonably to player actions and to the behaviors of other nonplayer characters; but on the other hand they want to craft certain very specific experiences that
nudge the player into trying new actions or approaching problems from a specific direction or that
prevent the agent from performing awkward-looking sequences of 3D animations. Traditionally,
game character AI was implemented with explicit state machines built by hand; more recently
behavior trees, goal-oriented action planning, and utility-based systems have come into vogue.

Fig. 1. A example behavior tree for a noise-investigation behavior. The tree is evaluated in preorder traversal.
Leaf nodes specify actions in the world (such as moving to a target), which can succeed or fail. Interior nodes
combine children into composite behaviors. The arrow (→) is sequencing (run each child until first failure),
and the question (?) is selection (run each child until first success).

Behavior trees are a scripting system for agents in virtual worlds, allowing designers of virtual
agents to visually construct behavioral flowcharts based on conditions on the world around them.
They are widely employed in the video games industry [16] for describing the “artificial intelligence”
behavior of non-player characters, such as enemy units in combat simulators and members of
virtual populations in open world-style games. Behavior trees have also been used for robot
control [12]. They are often described as merging the utility of decision trees and state machines,
allowing repeated or cyclic behaviors that modify and check state (internal or shared) as they
execute. Figure 1 shows an example behavior tree for a hypothetical security guard character. The
tree defines how to sequence and prioritize basic behaviors of listening for noises, investigating the
source of the noise, or doing idle activities. During game simulation, behavior trees are typically
re-executed with some frequency depending on the game, as often as once or more per time step.
The example in Figure 1, for instance, needs to be executed twice to both acquire a target and
investigate it.
Since behavior trees are often deployed in multi-agent simulations and with complex statechanging behavior, the ability for a designer to reason about the correctness of the tree quickly
succumbs to its size and branching factor. Even for straightforward sequences of behaviors, the
preconditions and postconditions are left unstated. For example, if an agent is told to move to door,
open door, and go through door, we might reasonably expect that in all circumstances where
the door is accessible, the agent will be on the opposite side of it by the time its behavior finishes.
However, this is not possible to conclude unless we reason both about the conditions and effects of
the individual actions and how the effects of earlier actions are expected to connect to the conditions
of later ones. Such a sequence of actions could fail, for instance, if the player were to intervene and
close the door immediately after the agent opened it. Furthermore, the success of behaviors may
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

A Resourceful Reframing of Behavior Trees

1:3

depend on external conditions on the environment: an agent may expect another agent to have
placed an important item that it needs, and the behavior is only correct on the condition that this
dependency has been satisfied.
We describe an approach to reasoning compositionally about behavior trees in such a way that
they may be constructed in small units, typechecked against an expected behavioral schema, and
combined to form behaviors with new, compositionally-defined types. The approach requires the
author to provide a linear logical specification of the atomic actions, i.e. the leaves of the tree; types
for complex expressions formed from these leaves are derived from a linear logical interpretation
of the behavior tree operations (sequencing, selection, and conditions). The present work can be
seen as a way to regain some of the guarantees given by reasoning about a behavior from start
to finish without losing the reactivity, which is the main benefit of using behavior trees over, for
example, static plan generation [7].
Since behavior trees are a relatively simple formalism repeatedly realized in different incarnations,
and since game developers are under somewhat notorious pressure to ship products, there is no
authoritative, standard version of behavior trees. As alluded to above, a recurring issue with
behavior trees is resolving the apparent tension between reacting to unexpected changes in the
environment on the one hand and to performing authored behaviors over a longer duration on
the other hand. The ad hoc extensions applied to behavior trees in the wild are often intended to
resolve this tension. The approaches described in this paper could give a theoretical foundation
for addressing these “hacks” employed in practice—and, potentially, for more principled and
better-behaved adaptations of behavior trees towards the problem of designing complex agent and
character behaviors.
Our contributions are a formal specification and operational semantics for our formulation of
behavior trees, a type system and synthesis algorithm backed by an interpretation in linear logic,
and an implementation of these systems in Standard ML. These results represent the first step of
toward building a toolkit for robust authoring of virtual agent behaviors, combining support for
correct human authorship and certified goal-driven synthesis of behaviors.
The rest of the paper is organized as follows: Section 2 discusses related work; Section 3 describes further how behavior trees are used in the games industry, Section 4 explains linear logical
specifications and how they may be used to describe a possibility space for virtual worlds; Section 5
describes the syntax and operational semantics of our behavior tree language; Section 6 describes
the type system and its guarantees; Section 7 describes our implementation; Section 8 discusses
our current scope and future work; and 9 summarizes our contributions.
2

RELATED WORK

For the most part, efforts to provide robust formalisms to designers of virtual agents have been
disjoint from formal and language-based approaches. We identify related work in two key areas:
previous attempts to characterize virtual agent behaviors from a formal methods standpoint, and
related models of computation that have been characterized with linear logic.
2.1

Formal accounts of behavior trees

Marzinotto et al. provide an account [12] of behavior trees in the context of robot control, citing a dearth of mathematical rigor prior to their contribution. Their work contributes the first
mathematical definition of behavior trees and accounts for their expressive capabilities.
More recently, there has been some very recent work in applying synthesis and verification to AI
behavior trees [4]. The formal basis for said work is model checking in linear temporal logic (LTL).
Our work, by contrast, seeks a type-theoretic solution that supports modular reuse of behaviors.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:4
2.2

Chris Martens, Eric Butler, and Joseph C. Osborn
Linear logical accounts of agents and processes

Linear Session Types [2] are an important touchstone for this work as another characterization
of a pre-existing system, π -calculus, under a semantics derived from linear sequent calculus. Our
work does not identify a direct logical correspondence between logical and operational notions in
the same way, but similarly provides a basis for static reasoning about complex behaviors.
The CLF [18] logical framework and corresponding implementation Celf [17] form a basis for
interpreting linear logic formulas as programs under a proof-construction-as-execution paradigm
(logic programming). While operationally, this approach diverges from the semantics of behavior
trees, the representation formalism informs out approach.
Finally, linear logic has been used to account for planning in a number of interesting ways:
deductive planning [5] runs with the observation that, in addition to Masseron et al.’s observation
that linear proof search can model planning [13], linear proofs generalize plans: they can characterize
recursive and contingent (branching) plans, recovering some of the same expressiveness as behavior
trees. Dixon et al. [6] apply deductive planning to an agent-based domain for dialogue-based
environments. This work encourages us to consider integrating the generative abilities of planners
with the reactivity of behavior trees in future work.
3

BACKGROUND: BEHAVIOR TREES IN GAMES

Behavior trees are widely used to define the behavior of non-player characters in digital game
genres ranging from strategy and simulation to first-person shooters. The major game-making
tools (Unreal Engine, Unity 3D, CryEngine, Amazon Lumberyard, and others) all either provide
natively or have third-party implementations of the technique. The canonical examples of behavior
trees’ use in games come from the Halo series of first-person shooter games [9]. Notable in their
formulation is that most of the tree is shared across the different types of enemy agents that appear
in the game, which reflects the difficulty of authoring good and reasonable behavior policies in
general. Behavior trees give authors a way to reuse some behaviors and override others from agent
to agent.
Behavior trees are usually characterized as a reactive AI formalism, in this context meaning that
agents are defined in terms of their reactions to a changing environment, rather than by a top-down
plan that tries to achieve a goal by considering contingencies in advance. Certainly, even finite
state machines can be made reactive by adding appropriate transitions, but scaling them to myriad
potential game events quickly overwhelms authors. Behavior trees reduce that burden by asking a
behavior author to structure the reactive behaviors in a tree, implicitly defining which behaviors
supersede or interrupt which other behaviors by their position in a preorder traversal of that tree.
A behavior tree is a data structure describing how an agent decides on its next actions, and at
the leaves some primitives for executing those actions. Behavior trees are repeatedly evaluated and
on each evaluation they process their nodes in sequence. When a node is processed, it evaluates
with some status: RUNNING, SUCCEEDED, or FAILED. Different sorts of nodes in the tree are specified
in terms of the circumstances under which they evaluate to each return value.
A key question in behavior tree semantics is whether a tree which ends an evaluation with
the RUNNING status should, on the next evaluation, continue from where it left off; the alternative
is for it to begin its next evaluation from the root again. The latter approach is more reactive to
changes in the environment or interruptions to behaviors, but in the former it is easier to specify
and conceptualize behaviors which take some time and should not be interrupted. It is also easier
to avoid behavior oscillations in the former evaluation strategy. For example, with the investigation
example from Figure 1: with the latter approach, the agent can be interrupted by a new noise
when moving to a target, while with the former approach, the agent will fully investigate a target
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

A Resourceful Reframing of Behavior Trees

1:5

without distraction. Game designers have explored both semantics and even hybrids between these
approaches; we leave our discussion of this issue until Sec. 5.
Leaf nodes of the tree can be domain-specific conditions (which succeed if the condition is
currently satisfied or fail otherwise) or domain-specific actions (for example, setting the value of a
variable or triggering some external action). These are the only operations which can interact with
the environment. The actions in Figure 1 include setting a variable representing the agent’s current
target or physically navigating the agent towards said target. Failure may come from, for example,
there being no navigable path to the target. In video games, these are often implemented using
arbitrary program code working outside of the behavior tree formalism.
Non-leaf nodes come in three key variants (others are usually possible to define as syntactic
sugar). First, sequences evaluate each of their child nodes from left to right, and are RUNNING if any
child node is RUNNING, FAILED if any child is FAILED, or SUCCEEDED otherwise. Second, selectors
also evaluate their child nodes left to right, but are RUNNING if any child is RUNNING, SUCCEEDED
if any child has SUCCEEDED, and FAILED if all the child nodes are FAILED. Third, the parallel node
evaluates each of its children independently of each other, and has SUCCEEDED if more than a certain
number of its children succeeds, FAILED if more than a certain number fail, and RUNNING otherwise.
It is also implicit in the definition of behavior trees that there is some external environment where
state can be stored and persisted from evaluation to evaluation.
In practice, there are many other types of nodes that can alter the semantics of the tree in
arbitrary ways, often violating the assumption of a preorder traversal: repeaters which evaluate
their children over and over until they evaluate with some status, stateful versions of sequence
and selector with memory that remember when they get stuck in RUNNING and only evaluate from
that stuck node forwards in their next evaluation, and so on. We ignore such extensions in this
work to simplify the presentation. Most of the extensions of behavior trees are meant to facilitate
long-running actions, to limit the reactivity of behavior trees (e.g., to allow interruptions only at
designer-defined times), and to ease the sharing of behavior tree or character state across situations,
characters, and actions. Actions, conditions, and decorators often themselves involve arbitrary code
in practice, so in our presentation of the formal semantics we require a linear logic formulation of
the leaf nodes.
4

ACTION SPECIFICATIONS IN LINEAR LOGIC

As a first step towards a type system for general behaviors, we concretize action specifications for
describing the behavior of an atomic action, such as “idly smoke cigarette” in Figure 1. Although
in reality, this behavior may simply take the form of an observable effect (e.g., some animation),
semantically, there are certain things we expect for it to make sense: for instance, that the agent has
a supply of cigarettes (and perhaps that this action spends one). Other actions, like passing through
a door, have more important requirements and effects, such as requiring being near the door and
resulting in the door being open: these are aspects of the environment that may be created, or
depended on, by other agents (or the same agent at another time).
There is a long line of successful work on describing actions in a protocols and virtual worlds
using any of a class of related formalisms: multiset rewriting, Petri nets, vector addition systems,
and linear logic. These systems have in common an approach to specification using rules (or
transitions in some systems) that describe dependencies and effects, such that the cummulative
effects of applying those rules may be reasoned about formally.1

1 Planning

domain description languages also share this approach, but most standards such as PDDL [14], do not have as
clean of a compositional interpretation due to their allowance for the “deletion” of facts that do not appear as preconditions.

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:6

Chris Martens, Eric Butler, and Joseph C. Osborn

Fig. 2. One step of multiset rewriting execution, visualized. Each color/shape (purple diamond, blue circle) represents a distinct predicate; the contents of those shapes are terms (a, b, c) or term variables
(X). This diagram represents a transition of the state ∆ = {diamond(a), circle(a), circle(b), diamond(c)}
along the rule circle(X ) ⊗ diamond(X ) ( diamond(c) ⊗ diamond(d) to the new state ∆ 0 =
{diamond(c), diamond(d), circle(b), diamond(c)}. The thick orange borders on some atoms highlight which
ones are replaced and added by the rule.

The following example uses a linear logic-based notation adapted from Ceptre [11] to describe
action specifications for an Investigation world that could assign meaning to the actions used in
Figure 1:
set_target
move_to_target
investigate
smoke
pace

:
:
:
:
:

no_target -o has_target.
has_target -o has_target * at_target.
has_target * at_target * heard_noise -o no_target.
has_cigarette -o 1.
1 -o 1.

The “lolli” syntax A -o B describes the ability to transition from a world in which A obtains to
one in which A no longer obtains and has been replaced with B. The atomic propositions include
facts like at_door and door_open, which represent pieces of world state, the “tensor” p * q syntax
conjoins them, and 1 is the unit of tensor. World configurations can be represented as multisets (or
linear contexts) ∆ specifying which facts hold, such as {no_target, heard_noise, has_cigarette,
has_cigarette}.
In general, predicates can take arguments (e.g., at(castle)) and rules can universally quantify
over variables that stand in for term arguments, in which case states are always ground (contain no
variables) and the application of rules identifies appropriate substitutions for variables for which
the rule applies. Figure 2 visualizes a step of execution for an example.
Multiset rewriting has been used commonly to model nondeterminism and concurrency: rulesets
can be nondeterministic whenever multiple rules may apply to a given state, and concurrency arises
from the partial-order causal relationships between rules firing. If two rules operate on disjoint
parts of the state, for instance, they can be considered to fire simultaneously, whereas rules that
depend on the effects of previous rules firing must obey sequential ordering. See Figure 3 for a
diagram of the causal relationships between actions for a particular program trace in which the
agent sets a target, moves to the target, investigates a noise, and smokes a cigarette.
For the work described in this paper, however, we are less interested in the multiset rewriting
interpretation of the rules. The specification under the multiset rewriting interpretation alone does
not give us as authors any control over strategies for action selection or goal-driven search. Instead,
it can be thought of as a description of the space of possible actions and a way of calculating their
cumulative effects. Behavior trees, then, can be understood as directives for how to explore this
space.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

A Resourceful Reframing of Behavior Trees

1:7

Fig. 3. A causal diagram for a possible trace of actions under the multiset rewriting interpretation of the
Investigate specification.

Formally, we define action specifications under the following grammar:
arд
arдs

::= t | x
::=

· | arд, arдs

S

::= p(arдs) | 1 | S ⊗ S

opdecl

::= name : xs. S ( S

Σ

::=

· | Σ, opdecl

Σ is a collection of specifications for operators op. Σ may also specify a collection of valid domain
types over which the arguments of operators may range; for example, the operator move(Dir, N )
may range over directions and natural numbers, perhaps meaning to move in that direction a
certain number of units. The world state ∆ is represented as a linear logic context, i.e. a multiset of
atomic propositions p(arдs) representing available resources.
In the next section, we assume an arbitrary signature Σ for each action that computes a function
on states, which does not depend on the linear logical interpretation. However, we revisit this idea
in Section 6 to assign types to behavior tree expressions.
5

BTL: A FORMAL SEMANTICS FOR BEHAVIOR TREES

In this section we describe BTL, a formal calculus for describing synchronous agent behaviors with
sequencing, branching, conditions, and loops.
The goals of this system are similar in many ways to the BTs used in practice: we aim to provide
simple authoring affordances for scripting reactions to different circumstances in an implicit
environment that is changing around the agent, and which the agent can change. We also adopt
some goals that are not currently met by industry practice:
• Compositional reasoning. In order to be able to reason about BT nodes in terms of the
behaviors of their subtrees, we need to know that subtree behaviors won’t be interrupted
in unknowable states.
• Debugging support—specifically, the ability for authors to state what they expect a behavior
to accomplish and have this expectation checked algorithmically. The algorithm should be
able to identify where in the tree a stated expectation is violated.
• Support for the expression of coordinated multi-agent behaviors. This requirement means
that we question the notion of an action dependency necessarily meaning failure and
instead (or additionally) require a blocking semantics (for instance, an agent may wait until
another agent joins them in the same location to hand off a needed item).
• Support for the eventual integration of behavior synthesis, or algorithms that accept a
propositional goal for the world state and generate BT subtrees corresponding to conditional
plans that achieve the goal.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:8

Chris Martens, Eric Butler, and Joseph C. Osborn

These nonstandard goals entail some tradeoffs of expressiveness. While it would be ideal to
retain, for example, the “reactive” nature of BTs that allow them to break sequential actions to
tend to urgent interruptions, we do not adopt this form of reactivity by default because it would
preclude the ability to reason about sequential behaviors compositionally. In Section 8 we revisit
these expressiveness tradeoffs and consider ways to re-incorporate additional features.
5.1

Expressions

The expressions of BTL are:
α

::= op(arдs) |?p. α | Seq{α; α } | Sel{α + α } | Seq{} | Sel{} | Repeat{α }

Intuitively, op(arдs) is an atomic action, invoking a pre-defined operator on a set of ground
arguments (such as move(left)); Seq{α; α } is a sequence node; Seq{α + α } is a selector node; Seq{}
is the unit of sequencers (does nothing); Sel{} is the unit of selectors (always fails); ?p. α checks the
condition p and executes α if it holds, failing otherwise; and Repeat{α } is a repeater node, running
α until failure.
5.2

Operational Semantics

We define an operational semantics for behavior trees in terms of what they may do to an abstract
world state, using a big-step evaluation judgment α . ∆ ⇓ δ , where ∆ is a world state and δ is the
result of evaluating a BTL expression, either a new world state (on successful execution) or FAIL.
The evaluation judgment requires a few preliminaries to define. First, we implicitly index the
judgment by a signature Σ, which provides a specification for a transition function t : τ → ∆ → δ
for each operator (atomic action) available to an agent, which takes arguments of type τ , computes
a transformation on a world state if the action can be performed, and returns FAIL otherwise.
Concretely, our linear logical action specifications can play this role. Second, we assume a notion of
a condition “holding for” a world state, expressed by the judgment ∆ p. Again, while evaluation
can be defined holding this judgment abstract, in we can fulfill this definition by expressing
conditions in terms of a (positive) subset of linear logic formulas and interpreting as affine
provability.
Evaluating an operation consists of looking up its transtition function in Σ and applying that
function to the current state; evaluating a condition requires that the current state satisfies the
condition, and otherwise fails:
Σ(op) = t t(arдs, ∆) = δ
∆ S α .∆⇓δ
∆6 S
op(arдs) . ∆ ⇓ δ
?S. α . ∆ ⇓ δ
?S. α . ∆ ⇓ FAIL
A sequence evaluates by chaining the states computed by successful subtrees through successive
subtrees in the sequence, and fails if any subtree fails:
α . ∆ ⇓ ∆ 0 Seq{α 0 } . ∆ 0 ⇓ δ
α . ∆ ⇓ FAIL
0
Seq{} . ∆ ⇓ ∆
Seq{α; α } . ∆ ⇓ δ
Seq{α; α 0 } . ∆ ⇓ FAIL
A selector succeeds with the first successful subtree and fails if no options are possible:
α . ∆ ⇓ FAIL Sel{α 0 } . ∆ ⇓ δ
α . ∆ ⇓ ∆0
Sel{} . ∆ ⇓ FAIL
Sel{α + α 0 } . ∆ ⇓ δ
Sel{α + α 0 } . ∆ ⇓ ∆ 0
Repeaters continue evaluating the underlying expression until failure:
α . ∆ ⇓ ∆ 0 Repeat{α } . ∆ 0 ⇓ δ
Repeat{α } . ∆ ⇓ δ
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

α . ∆ ⇓ FAIL
Repeat{α } . ∆ ⇓ ∆

A Resourceful Reframing of Behavior Trees

1:9

This definition of BTL adopts similar conventions and semantics to process algebras, such as
the adoption of two key operators, sequential (conjunctive) and choice (disjunctive) composition,
which have certain algebraic properties. In the case of BTL, evaluation respects the following
structural congruence:
Seq{Seq{}; α }
Seq{α; Seq{β; γ }}
Sel{Sel{} + α }

≡ Seq{α } ≡ Seq{α; Seq{}}
≡
≡ Sel{α } ≡

Seq{Seq{α; β }; γ }
Sel{α + Sel{}}

Sel{α + Sel{β + γ }}

≡

Sel{Sel{α + β } + γ }

Seq{α; Sel{β + γ }}

≡

Sel{Seq{α; β } + Seq{α; γ }}

Seq{Sel{α + β }; γ }

≡

Sel{Seq{α; γ } + Seq{β; γ }}

In other words, sequences form a monoid with the unit Seq{}; selectors form a monoid with the
unit Sel{}; and sequencing distributes over selection. We state that this equivalence is respected by
evaluation but omit the proof for brevity:
Conjecture 5.1. BTL operational semantics respects congruence: If α . ∆ ⇓ δ and α ≡ β then
β . ∆ ⇓ δ.
While the system bears resemblance to models of concurrency such as CSP [8] and (CCS) [15],
it differs in that interactions between BTL expressions and their environment happen implicitly
through manipulation of a shared world state, not through channel-based communication (as in
CSP) or explicit labels for inputs and outputs (as in CCS). The lack of such machinery is what
makes behavior trees so attractive to authors; it reduces the burden of needing to specify how
information is transmitted from one agent to another. However, it also makes the dependencies
between agents tacit and therefore difficult to debug when things go wrong, which is what this
paper aims to address.
Kleene algebra, particularly Kozen’s variant with tests (KAT) [10], offers another touchstone for
semantic insights; however, BTL does not quite satisfy the Kleene conditions: (1) order matters in
selector semantics due to fallthrough, so selectors are not commutative; (2) the annihilation law
does not hold; Seq{α; Sel{}} is not equivalent to Sel{} due to the state changes that α may incur.
5.3

Example

Below is BTL implementation of the behavior tree described in Figure 1. This and all future examples
use an n-ary form of Seq and Sel defined in the obvious way.
Sel{?heard_noise.set_target() +
Seq{move_to_target(); investigate_target()} +
Sel{idle_smoke() + idle_pace()}}

To illustrate how an BTL expression evaluates, we consider an evaluation of this tree in an environment where the agent already has a reachable target and has not heard a noise, i.e. the situation
{has target}. Starting evaluation at the root, the outer selector expression evaluates each child in
succession until one succeeds. The first child will fail because the heard noise condition does not
hold. The second child, a sequence, will evaluate each of its children in succession. The first action,
predicated on having a target, evaluates by modifying the world state such that the agent is in the
same location as the target. Upon the movement action succeeding, the investigate target()
action will be evaluated; however, this node fails in the absence of having heard a noise, and that
failure propagates to the root of the tree.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:10

Chris Martens, Eric Butler, and Joseph C. Osborn

Γ; p ` p

init

Γ; · ` 1

1R

Γ; ∆ ` M : C
1L
Γ; ∆, 1 ` C

Γ; ∆1 ` A Γ; ∆2 ` B
⊗R
Γ; ∆1 , ∆2 ` A ⊗ B
Γ; ∆, A ` B
(R
Γ; ∆ ` A ( B

>R

(no >L)

Γ; ∆, A, B ` C
⊗L
Γ; ∆, A ⊗ B ` C

Γ; ∆1 ` A Γ; ∆2 , B ` C
(L
Γ; ∆1 , ∆2 , A ( B ` C

Γ; ∆ ` A Γ; ∆ ` B
NR
Γ; ∆ ` ANB
Γ, x:τ ; ∆ ` A
∀R
Γ; ∆ ` ∀x:τ . A

Γ; ∆ ` >

Γ; ∆, Ai ` C
NLi
Γ; ∆, A1 NA2 ` C

Γ ` t : τ Γ; ∆, N [t]:A ` C
∀L
Γ; ∆, ∀x:τ . A ` C

Fig. 4. A fragment of intuitionistic linear sequent calculus.

If instead we started in an environment {has target, heard noise}, then at the same point in
the tree, the investigate target action will succeed and change the world state by replacing
has target with no target (in practice, this might have a more interesting effect like updating
variables representing the agent’s knowledge of its target). Because both children of the sequence
evaluate to success, the sequence evaluates to success. Thus, the root selector will itself evaluate
to success without evaluating the third branch, completing the evaluation of the entire tree, and
resulting in the state {no target}.
6

COMPOSITIONAL REASONING

Compositional reasoning for behavior trees means that understanding the effects of a whole BT can
be done by understanding the effects of its subtrees. The type system we describe gives a precise
account of the conditions under which a BT has successful execution and the consequences of that
execution. Accounting for the range of behaviors possible under failure is outside the scope of this
paper (see Section 8). However, these types are richer than sets of precondtions and postcondtions:
they account for the “reactive” nature of BTs by requiring dependencies to be filled not prior to
execution but just at the node of the tree where they are needed; types also describe resources that
are released periodically if they are not needed for later use.
This “open” structure of behavior types makes the account of agents’ behavior amenable to
analysis in the presence of multiple agent executing in parallel: BTs may both incur and use changes
in the environment.
6.1

A linear type system, take 1

Our guiding principle for assigning types to BTL expressions adopts a “formulas-as-processes”
point of view to imagine the proof-theoretic semantics of what the formula admits provable under
arbitrary environments. Consider linear logic formulas A ::= p | 1 | > | A ⊗ A | ANA | A ( A and
an intuitionistic sequenct calculus defining their provability (following [3]) shown in Figure 4.
The following intuition guides the correspondence we seek:
• Firing a leaf action op(arдs) of type S ( S 0 in an environment ∆ corresponds to the (-left
rule in linear sequent calculus: to succeed, it requires that the current environment match
the antecedent of the action and then changes the environment to replace it with the
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

A Resourceful Reframing of Behavior Trees

1:11

consequent. Correspondingly, evaluating op(arдs) in an environment ∆, ∆ 0 where ∆ 0 ` S
evaluates to ∆, S 0 in the operational semantics.
• The unit selector Sel{} always fails, having run out of options; this corresponds to the >
unit of N in linear logic, which has no left rule, so everything is beneath it in the preorder.
• The unit sequence Seq{} does nothing, corresponding to the left rule of the unit 1 of ⊗.
Correspondingly, the operational semantics of Seq{} take the environment ∆ to itself.
• Selectors Sel{α 1 +α 2 } nearly correspond to making a choice, as in Linear Logic’s N operator.
There is a difference in that N is symmetric; ANB and BNA are interprovable, whereas order
matters in BTL selectors. However, certain reasoning principles apply: if either α 1 . ∆ ⇓ ∆1
or α 2 . ∆ ⇓ ∆2 , then one of ∆1 or ∆2 will be the result of evaluating Sel{α 1 + α 2 } against ∆.
For reasons described above, however, accounting for sequences will be more difficult. It might
be tempting to think that ⊗ is an appropriate interpretation, despite the relative lack of ordering
constraints, for reasons similar to how N can approximate selectors. A conjectured rule:
α 1 : A1 α 2 : A2
BAD RU LE
Seq{α 1 ; α 2 } : A1 ⊗ A2
At this point we need to formulate the metatheorem we have so far been implicitly expecting to
hold:
Conjecture 6.1. If α : A and ∆, A ` S, then α . ∆ ⇓ ∆ 0 and ∆ 0 ` S.
(Recall that S stands for a formula with no Ns or (s, representing a successful state in the
course of a BTL expression’s execution.) The proposed rule violates this conjecture; we show a
counterexample next.
6.2

The trouble with sequences: an example

The following action specification describes a Doors world in which agents may pass through open
doors, open unlocked doors, and unlock locked doors if they have keys:
walk_to_door : at_elsewhere -o at_door.
pass_through : door_open * at_door -o door_open * through_door.
open_door : door_unlocked * at_door -o door_open * at_door.
smash_door : door_locked * at_door -o door_open * at_door.
close_door : door_open * through_door -o door_unlocked * through_door.

For a counterexample to Conjecture 6.1, let α = Seq{open door; walk to door} and let ∆ =
{at elsewhere, door unlocked}. According to BAD RU LE, α : A = (at door⊗door unlocked (
door open)⊗(at elsewhere ( at door). By straightforward rule applications, ∆, A ` door unlocked,
but it is not the case that Seq{open door; walk to door} . ∆ ⇓ door unlocked.
In addition to the clear unsoundness of describing a sequential behavior with a commutative
connective, there are also concerns regarding the granularity of concurrent execution. Consider a
simple sequential behavior for opening and going through a door:
Seq{walk_to_door; open_door; pass_through; close_door}

A type we could reasonably expect to ascribe to this behavior is:
at elsewhere ⊗ door unlocked ( through door ⊗ door unlocked
This formula corresponds to the assumption that if our starting environment has at elsewhere
and door unlocked, each element in this sequence of actions will consume the output of the
previous action as an input, resulting in through door. Each successive action depends on the
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:12

Chris Martens, Eric Butler, and Joseph C. Osborn

effects of previous actions: opening the door assumes that the previous walk action brought us to
the door; passing through assumes we successfully opened the door; and closing the door assumes
we passed through and the door is still open.
However, in a general, maximally concurrent environment, we would not be allowed to make
these assumptions: suppose, for example, another agent interferes and closes the door just after we
open it. This relaxed assumption instead observes that we might forfeit all of the effects of previous
actions, resulting in the following type:
at elsewhere ( at door ⊗ (at door ⊗ door unlocked (
at door ⊗ door open⊗
(at door ⊗ door open ( through door ⊗ door open⊗
(door open ⊗ through door ( through door ⊗ door unlocked)))
This formula characterizes the behavior that, at each step, a sequence releases some resources
into the world along with a “continuation” that could, in some cases, potentially reabsorb those
resources, or require new ones along the way.
These two ascriptions correspond to different assumptions about how behaviors interact with
other behaviors manipulating the environment. The former assumes an un-interruptable, “critical
section” behavior to sequences and gives a stronger guarantee, allowing us to treat the sequence
as a black-box behavior without worrying about internal failure. On the other hand, the latter
permits interruption and “race condition”-like scenarios that are common in games and interactive
simulations in practice, but offers less strict guarantees that reflect the complexity of reasoning
about fine-grained interaction.
Our type system makes the latter assumption that processes may be interrupted, but we discuss
the potential to accommodate both in Section 8.
6.3

Linear Behavior Interfaces

We constrain linear logical formulas to the following grammar of interfaces, expressed inductively
as nested stagings of inputs and outputs (and choice between multiple possible interfaces):
N

::= S | S ( N | S ⊗ N | N NN | >

This grammar mainly serves to prevent ( from appearing to the left of another ( while
representing staged inputs and outputs as described above.
We assign types as linear logic formulas N to BTL expressions α with the judgment α :Σ N .
where α is an expression, N is an interface type, and Σ is a specification giving types S ( S 0 to the
actions used at the leaves of the trees.
The typing rules are as follows, with Σ left implicit as an index to the judgment except when it is
needed. Atomic operations, conditions, the units, and selectors, are straightforward, and conditions
must assume, but then reproduce, the condition they depend on. Sequences are assigned a type
based on a computation seq of the types of their components:

Seq{} : 1
α1 : N1 α2 : N2
Sel{α 1 + α 2 } : N 1 NN 2

Sel{} : >

Σ ` op : xs. S ( S 0
op(arдs) :Σ [arдs/xs](S ( S 0)

α :N
?S. α : S ( S ⊗ N

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

α1 : N1 α2 : N2
Seq{α 1 ; α 2 } : seq(N 1 , N 2 )

A Resourceful Reframing of Behavior Trees

1:13

The seq operator is defined as follows:
seq(1, N ) =

N

seq(S 1 , S 2 ) = S 1 ⊗ S 2
seq(S, S 0 ⊗ N ) =

(S ⊗ S 0) ⊗ N

seq(S, N 1 NN 2 ) =

seq(S, N 1 )Nseq(S, N 2 )

seq(S 1 , S 2 ( N ) = S 1 ⊗ (S 2 ( N )
seq(S ⊗ N 1 , N 2 ) =

seq(S, seq(N 1 , N 2 ))

seq(S 1 ( N 1 , N 2 ) = S 1 ( seq(N 1 , N 2 )
seq(N 1 NN 2 , N ) =

(seq(N 1 , N )Nseq(N 2 , N ))

It can be interpreted as pushing the requirements of the first formula to the outside of the
whole formula, then conjoining its consequences with the specification of the second formula. The
correctness of this definition, and of the type system in general, with respect to the operational
semantics, is considered next.
6.4

Metatheory

We revisit Conjecture 6.1 and sketch a proof. First we establish a lemma about the seq operator:
Lemma 6.2. If ∆, seq(N 1 , N 2 ) ` S and ∆ is flat, i.e. consists only of propositions of the form S, then
there exists S 1 such that ∆, N 1 ` S 1 and ∆, S 1 ` N 2 .
Proof. By induction on the definition of seq. We show the interesting cases.
• Case: seq(S 1 , S 2 ( N ) = S 1 ⊗ (S 2 ( N ).
Assume ∆, S 1 , S 2 ( N ` S.Ë
In this case, we can
Ëjust tensor together the first state and feed
it into the second. ∆, S 1 `
(∆) ⊗ S 1 , and ∆, (∆) ⊗ S 1 , S 2 ( N ` S by untensoring that
proposition to get to the assumption.
• Case: seq(S 1 ( N 1 , N 2 ) = S 1 ( seq(N 1 , N 2 ).
Assume ∆, S 1 ( seq(N 1 , N 2 ) ` S. Because the proof of this sequent concludes with an S,
somewhere along the way we must discharge the (, i.e. some part of ∆ proves S 1 . Rewrite
∆ = ∆1 , ∆ 0 where ∆1 ` S 1 . Somewhere in the proof there is an application of ( L such
that ∆ 0, seq(N 1 , N 2 ) ` S is a subproof, and by inductive hypothesis, there exists S 0 such that
∆ 0, N 1 ` S 0 and S 0, N 2 ` S.
Now it suffices to show that ∆, S 1 ( N 1 ` S 0 (since we already have S 0, N 2 ` S). This
can be established by reusing the part of ∆ that discharges S 1 , using ( L on ∆1 ` S 1 and
∆ 0, N 1 ` S 0 .
• Remaining cases are straightforward.

Theorem 6.3. If α : A, ∆ is flat, and ∆, A ` S, then α . ∆ ⇓ ∆ 0 and ∆ 0 ` S.
Proof. By lexicographic induction on the typing derivation and proof. We show the sequence
case here.
• Case:
α1 : N1 α2 : N2
Seq{α 1 ; α 2 } : seq(N 1 , N 2 )
Known: ∆, seq(N 1 , N 2 ) ` S. By lemma, there exists S 0 such that ∆, N 1 ` S 0 and S 0, N 2 ` S.

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:14

Chris Martens, Eric Butler, and Joseph C. Osborn
By i.h., α 1 . ∆ ⇓ ∆ 0 where ∆ 0 ` S 0. By i.h., α 2 . {S 0 } ⇓ ∆ 00 where ∆ 00 ` S. By appropriate
equivalence between the positive propostion S 0 and context ∆ 0, and by the sequence
evaluation rule, Seq{α 1 ; α 2 } . ∆ ⇓ ∆ 00 where ∆ 00 ` S 0.


6.5

Example

We now return to the “investigating a sound” example whose evaluation was shown in Section 5.3.
The computed type for the example:
Sel{?heard_noise.set_target() +
Seq{move_to_target(); investigate_target()} +
Sel{idle_smoke() + idle_pace()}}

is:
(heard noise ( (heard noise ( no target ( has target)
N

(has target ( (has target ⊗ at target ⊗
(has target ⊗ at target ⊗ heard noise ( no target))

N

(has cigarette ( 1)

N
7

(1 ( 1)

IMPLEMENTATION

We implemented both an interpreter for BTL (with repeater nodes) and a type synthesis algorithm
for BTL excluding repeaters, both following the descriptions in the paper. The implementation is
written in 523 lines of Standard ML, including detailed comments, and we authored an additional
448 lines of examples, including those used in this paper.
The implementation is freely available on GitHub at (URL redacted for double-blind review).
8

DISCUSSION

A longer-term goal for this work is to be able to account for how behavior trees are used in practice,
to integrate the type system into the behavior authoring process (perhaps through a combination
of checking and synthesis), and to evaluate how it may make designers (particularly without
programming background) more effective. We anticipate using the implementation of BTs in the
Unreal Engine as a benchmark. Shorter term, there are a few theoretical concerns we still need to
consider. We now describe a roadmap for this project.
8.1

Parallel Composition

Currently, the semantics of agents operating in the world concurrently is not specified by the
language. To account for placing multiple world-manipulating agents into the environment, we
might consider introducing a “parallel” operator to BTL:
α ::= . . . | Par{α 1 k α 2 }
We may consider a few options for an operational semantics that warrant a different typetheoretic treatment. For instance, perhaps parallel behaviors split the state and operate in isolation
until complete. This behavior could be captured with the rule:
∆ = ∆1 , ∆2 α 1 . ∆1 ⇓ ∆10 α 2 . ∆2 ⇓ ∆20
Par{α 1 k α 2 } . ∆ ⇓ ∆10 , ∆20

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

A Resourceful Reframing of Behavior Trees

∆/skip → ∆/

Σ ` op[arдs] : A ( B ∆A ` A
step/op
∆, ∆A /op(arдs) → ∆, B/

step/skip

∆/α 1 →∗ ∆ 0/
step/;
∆/α 1 ; α 2 → ∆ 0/α 2

1:15

∆/α 1 + α 2 → ∆/α 1

∆, p/?p. α → ∆, p/α

step/?

∆1 /α 1 → ∆10 /α 10
step/k 1
∆1 , ∆2 /α 1 kα 2 → ∆10 , ∆2 /α 10 kα 2

step/+1

∆/α 1 9
step/+2
∆/α 1 + α 2 → ∆/α 2

∆/α →∗ ∆ 0/
step/∗
∆/α ∗ → ∆ 0/α ∗
∆2 /α 2 → ∆20 /α 20
step/k 2
∆1 , ∆2 /α 1 kα 2 → ∆1 , ∆2 /α 1 kα 20

Fig. 6. A small-step semantics for BTL without failure.

Additional rules may specify that if either
subbehavior fails, the whole behavior fails.
However, in practice, behavior trees allow for
finer-grained interactions between processes.
The above specification precludes, for example,
the below two behaviors succeeding:
// Agent 1 (a1)
Seq{move(a1,L);
give(a2,O)}

// Agent 2 (a2)
Seq{move(a2,L);
eat(a2,O)}

These behaviors will only succeed if they
interact when run; a1’s action give(a2,O) will
only succeed if a2’s first action, move(a2,L), is
permitted to succeed first. Figure 5 describes
Fig. 5. Composing processes that interact.
visually the behavior specification we would
like to result in this interaction.
To account for such fine-grained concurrent
behaviors formally, we require a small-step semantics over the judgment α/∆ → α/∆ 0. A
sketch of this semantics that includes parallel
composition is in Figure 6. However, note that this semantics does not properly handle failure;
instead, it embodies the synchronous semantics of behaviors simply pausing (failing to evolve)
if their conditions are not satisfied, instead permitting the possibility of a delayed transition if
their conditions become satisfied as another behavior evolves. While this behavior may be useful
in some scenarios, it is not universally desirable, so we need a way to account for this behavior,
perhaps through a stack-based semantics with success and failure continuations. Likewise, the type
system has a clear extension to count for arbitrarily “pausing” processes (⊗ is a straightforward
interpretation), but accounting for failure in the type system is also left to work.
8.2

Theoretical extensions

In addition to accounting for parallel execution, we also need to consider repeater nodes. The
operational semantics are fairly easy to specify, but guaranteeing convergence of computing fixed
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:16

Chris Martens, Eric Butler, and Joseph C. Osborn

points for a type-based characterization may prove difficult. Recursive types have been successfully
integrated into linear logic [1], and we plan to investigate their use, although readability may
remain a challenge.
Another step we would like to take is to introduce additional forms of lightweight verification
on top of the type system. For instance, selectors are often designed with the intent that all possible
cases are covered: each child of the selector is guarded by a condition, and the disjunction of the
conditions characterizes an invariant of the state. Provided a proof that the invariant actually holds,
it may be useful to simplify the type to omit the guards. This corresponds to provability between
e.g. (A ⊕ B) ⊗ ((A ( C)N(B ( D)) and (C ⊕ D).
Next, while we have established a correspondence between the type system and evaluation of
successful behaviors, we believe we can formulate a conjecture to the effect that the situations in
which types fail to yield a flat context (because there is some implication that cannot be discharged
on the left, say) correspond to the failure cases of execution. We expect this proof will be more
difficult than the former.
9

CONCLUSION

We have presented a formal semantics and type system for a fragment of behavior trees as they are
used to describe characters in virtual environments. Our system includes a reference implementation
and correctness proofs. This work represents substantial new ground broken towards a longer-term
vision of authoring robust, designer-friendly specifications for reactive agent behaviors.
If our long-term vision is successful, we can enable several new things for behavior authors:
integrating hand-authored trees with behavior synthesis algorithms through linear logic theorem
proving (akin to planning); the development of behavior libraries consisting of reusable, parameterized behavior trees whose specification precludes examining the entire tree; and certified behaviors
that are guaranteed to succeed under certain environments. These features would improve the
effectiveness of developing agents in virtual worlds with varied applications in entertainment, arts,
simulation modeling, research competitions and challenges, and computing education.
REFERENCES
[1] David Baelde. 2012. Least and greatest fixed points in linear logic. ACM Transactions on Computational Logic (TOCL)
13, 1 (2012), 2.
[2] Luis Caires, Frank Pfenning, and Bernardo Toninho. 2016. Linear logic propositions as session types. Mathematical
Structures in Computer Science 26, 3 (2016), 367–423.
[3] Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning. 2003. A judgmental analysis of linear logic. Technical
Report CMU-CS-03-131R. Department of Computer Science, Carnegie Mellon University. Revised December 2003.
[4] Michele Colledanchise, Richard M Murray, and Petter Ogren. 2017. Synthesis of Correct-by-Construction Behavior
Trees. (2017).
[5] Stephen Cresswell, Alan Smaill, and Julian Richardson. 1999. Deductive synthesis of recursive plans in linear logic. In
European Conference on Planning. Springer, 252–264.
[6] Lucas Dixon, Alan Smaill, and Alan Bundy. 2006. Planning as deductive synthesis in intuitionistic linear logic. Technical
Report. Technical Report EDI-INF-RR-0786, School of Informatics, University of Edinburgh.
[7] Malik Ghallab, Dana Nau, and Paolo Traverso. 2016. Automated Planning and Acting. Cambridge University Press.
[8] Charles Antony Richard Hoare. 1978. Communicating sequential processes. Commun. ACM 21, 8 (1978), 666–677.
[9] Damian Isla. 2005. Handling Complexity in the Halo 2 AI. In Proceedings of the 2005 Game Developers Conference.
[10] Dexter Kozen. 1997. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems (TOPLAS)
19, 3 (1997), 427–443.
[11] Chris Martens. 2015. Ceptre: A language for modeling generative interactive systems. In Eleventh Artificial Intelligence
and Interactive Digital Entertainment Conference.
¨
[12] Alejandro Marzinotto, Michele Colledanchise, Christian Smith, and Petter Ogren.
2014. Towards a unified behavior
trees framework for robot control. In Robotics and Automation (ICRA), 2014 IEEE International Conference on. IEEE,
5420–5427.

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

A Resourceful Reframing of Behavior Trees

1:17

[13] Marcel Masseron, Christophe Tollu, and Jacqueline Vauzeilles. 1993. Generating plans in linear logic: I. actions as
proofs. Theoretical Computer Science 113, 2 (1993), 349–370.
[14] Drew McDermott, Malik Ghallab, Adele Howe, Craig Knoblock, Ashwin Ram, Manuela Veloso, Daniel Weld, and
David Wilkins. 1998. PDDL-the planning domain definition language. (1998).
[15] Robin Milner. 1980. A calculus of communicating systems. (1980).
[16] Steven Rabin. 2013. Game AI Pro: Collected Wisdom of Game AI Professionals. A. K. Peters, Ltd., Natick, MA, USA.
[17] Anders Schack-Nielsen and Carsten Schürmann. 2008. Celf-A Logical Framework for Deductive and Concurrent
Systems (System Description).. In IJCAR, Vol. 5195. Springer, 320–326.
[18] Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2003. A concurrent logical framework I: Judgments
and properties. Technical Report. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie
Mellon University, 2002. Revised May.

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

