Specifying the desired behaviors of agents in environments is a major theme in artifcial intelligence. Analysts ofen need to defne particular policies with explicit steps, but the agents must also acknowledge salient changes in a potentially hostile or stochastic environment. Tis 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 diferent knowledge states, not unlike human-robot teams. Te 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 batery 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
1:2 Chris Martens, Eric Butler, and Joseph C. Osborn
but atractive diversions and prioritizes severe need. We can easily imagine two distinct agents within the same game which are diferentiated 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 non-player characters; but on the other hand they want to craf certain very specifc experiences that nudge the player into trying new actions or approaching problems from a specifc 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 fowcharts based on conditions on the world around them. Tey are widely employed in the video games industry [16] for describing the “artifcial 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]. Tey are ofen 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. Te tree defnes 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 ofen as once or more per time step. Te example in Figure 1, for instance, needs to be executed twice to both acquire a target and investigate it.
Since behavior trees are ofen 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 lef 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 fnishes. However, this is not possible to conclude unless we reason both about the conditions and efects of the individual actions and how the efects 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 afer the agent opened it. Furthermore, the success of behaviors may
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 satisfed.
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-defned types. Te approach requires the author to provide a linear logical specifcation 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). Te present work can be seen as a way to regain some of the guarantees given by reasoning about a behavior from start to fnish without losing the reactivity, which is the main beneft of using behavior trees over, for example, static plan generation [7].
Since behavior trees are a relatively simple formalism repeatedly realized in diferent 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. Te ad hoc extensions applied to behavior trees in the wild are ofen intended to resolve this tension. Te approaches described in this paper could give a theoretical foundation for addressing these “hacks” employed in practice—and, potentially, for more principled and beter-behaved adaptations of behavior trees towards the problem of designing complex agent and character behaviors.
Our contributions are a formal specifcation 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. Tese results represent the frst step of toward building a toolkit for robust authoring of virtual agent behaviors, combining support for correct human authorship and certifed goal-driven synthesis of behaviors.
Te 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 specifcations 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.
For the most part, eforts 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 atempts 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
Marzinoto 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. Teir work contributes the frst mathematical defnition of behavior trees and accounts for their expressive capabilities.
More recently, there has been some very recent work in applying synthesis and verifcation to AI behavior trees [4]. Te 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.
1:4 Chris Martens, Eric Butler, and Joseph C. Osborn
2.2 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.
Te 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. Tis work encourages us to consider integrating the generative abilities of planners with the reactivity of behavior trees in future work.
Behavior trees are widely used to defne the behavior of non-player characters in digital game genres ranging from strategy and simulation to frst-person shooters. Te 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. Te canonical examples of behavior trees’ use in games come from the Halo series of frst-person shooter games [9]. Notable in their formulation is that most of the tree is shared across the diferent types of enemy agents that appear in the game, which refects the difculty 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 defned 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 fnite 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 defning 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. Diferent sorts of nodes in the tree are specifed 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 lef of; the alternative is for it to begin its next evaluation from the root again. Te later 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 later 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
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-specifc conditions (which succeed if the condition is currently satisfed or fail otherwise) or domain-specifc actions (for example, seting the value of a variable or triggering some external action). Tese are the only operations which can interact with the environment. Te actions in Figure 1 include seting 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 ofen 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 defne as syntactic sugar). First, sequences evaluate each of their child nodes from lef 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 lef 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. Tird, 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 defnition 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, ofen 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-defned times), and to ease the sharing of behavior tree or character state across situations, characters, and actions. Actions, conditions, and decorators ofen themselves involve arbitrary code in practice, so in our presentation of the formal semantics we require a linear logic formulation of the leaf nodes.
As a frst step towards a type system for general behaviors, we concretize action specifcations for describing the behavior of an atomic action, such as “idly smoke cigarete” in Figure 1. Although in reality, this behavior may simply take the form of an observable efect (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 cigaretes (and perhaps that this action spends one). Other actions, like passing through a door, have more important requirements and efects, 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).
Tere 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. Tese systems have in common an approach to specifcation using rules (or transitions in some systems) that describe dependencies and efects, such that the cummulative efects of applying those rules may be reasoned about formally.1
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 along the rule to the new state {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.
Te following example uses a linear logic-based notation adapted from Ceptre [11] to describe action specifcations for an Investigation world that could assign meaning to the actions used in Figure 1:
Te “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. Te 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 confgurations can be represented as multisets (or linear contexts) specifying which facts hold, such as {no_target, heard_noise, 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 identifes 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 fring. If two rules operate on disjoint parts of the state, for instance, they can be considered to fre simultaneously, whereas rules that depend on the efects of previous rules fring 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 cigarete.
For the work described in this paper, however, we are less interested in the multiset rewriting interpretation of the rules. Te specifcation 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 efects. Behavior trees, then, can be understood as directives for how to explore this space.
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 defne action specifcations under the following grammar:
is a collection of specifcations for operators 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. Te world state is represented as a linear logic context, i.e. a multiset of atomic propositions 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.
In this section we describe BTL, a formal calculus for describing synchronous agent behaviors with sequencing, branching, conditions, and loops.
Te goals of this system are similar in many ways to the BTs used in practice: we aim to provide simple authoring afordances for scripting reactions to diferent 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—specifcally, the ability for authors to state what they expect a behavior to accomplish and have this expectation checked algorithmically. Te algorithm should be able to identify where in the tree a stated expectation is violated.
• Support for the expression of coordinated multi-agent behaviors. Tis 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 of 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.
1:8 Chris Martens, Eric Butler, and Joseph C. Osborn
Tese nonstandard goals entail some tradeofs 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 tradeofs and consider ways to re-incorporate additional features.
5.1 Expressions
Te expressions of BTL are:
Intuitively, is an atomic action, invoking a pre-defned operator on a set of ground arguments (such as is a sequence node; is a selector node; Seq{} is the unit of sequencers (does nothing); Sel{} is the unit of selectors (always fails); ?checks the condition p and executes if it holds, failing otherwise; and is a repeater node, running until failure.
5.2 Operational Semantics
We defne 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.
Te evaluation judgment requires a few preliminaries to defne. First, we implicitly index the judgment by a signature , which provides a specifcation for a for each operator (atomic action) available to an agent, which takes arguments of type a transformation on a world state if the action can be performed, and returns FAIL otherwise. Concretely, our linear logical action specifcations can play this role. Second, we assume a notion of a condition “holding for” a world state, expressed by the judgment . Again, while evaluation can be defned holding this judgment abstract, in we can fulfll this defnition by expressing conditions in terms of a (positive) subset of linear logic formulas and interpreting as afne 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 satisfes the condition, and otherwise fails:
A sequence evaluates by chaining the states computed by successful subtrees through successive subtrees in the sequence, and fails if any subtree fails:
Repeaters continue evaluating the underlying expression until failure:
A Resourceful Reframing of Behavior Trees 1:9
Tis defnition 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:
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 difers 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). Te lack of such machinery is what makes behavior trees so atractive to authors; it reduces the burden of needing to specify how information is transmited from one agent to another. However, it also makes the dependencies between agents tacit and therefore difcult to debug when things go wrong, which is what this paper aims to address.
Kleene algebra, particularly Kozen’s variant with tests (KAT) [10], ofers another touchstone for semantic insights; however, BTL does not quite satisfy the Kleene conditions: (1) order maters in selector semantics due to fallthrough, so selectors are not commutative; (2) the annihilation law does not hold; 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. Tis and all future examples use an n-ary form of Seq and Sel defned in the obvious way.
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. Te frst child will fail because the heard noise condition does not hold. Te second child, a sequence, will evaluate each of its children in succession. Te frst 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.
1:10 Chris Martens, Eric Butler, and Joseph C. Osborn
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 efect 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. Tus, 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}.
Compositional reasoning for behavior trees means that understanding the efects of a whole BT can be done by understanding the efects of its subtrees. Te 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 flled 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.
Tis “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 an intuitionistic sequenct calculus defning their provability (following [3]) shown in Figure 4.
Te following intuition guides the correspondence we seek:
• Firing a leaf action in an environment corresponds to the 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
A Resourceful Reframing of Behavior Trees 1:11
consequent. Correspondingly, evaluating in an environment where evaluates to in the operational semantics.
For reasons described above, however, accounting for sequences will be more difcult. It might be tempting to think that is an appropriate interpretation, despite the relative lack of ordering constraints, for reasons similar to how can approximate selectors. A conjectured rule:
At this point we need to formulate the metatheorem we have so far been implicitly expecting to hold:
(Recall that S stands for a formula with no s ors, representing a successful state in thecourse of a BTL expression’s execution.) Te proposed rule violates this conjecture; we show a counterexample next.
6.2 The trouble with sequences: an example
Te following action specifcation describes a Doors world in which agents may pass through open doors, open unlocked doors, and unlock locked doors if they have keys:
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:
A type we could reasonably expect to ascribe to this behavior is:
Tis 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
1:12 Chris Martens, Eric Butler, and Joseph C. Osborn
efects 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 afer we open it. Tis relaxed assumption instead observes that we might forfeit all of the efects of previous actions, resulting in the following type:
Tis 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.
Tese two ascriptions correspond to diferent assumptions about how behaviors interact with other behaviors manipulating the environment. Te 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 later permits interruption and “race condition”-like scenarios that are common in games and interactive simulations in practice, but ofers less strict guarantees that refect the complexity of reasoning about fne-grained interaction.
Our type system makes the later 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):
Tis grammar mainly serves to prevent from appearing to the lef 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 . where is an expression, N is an interface type, and is a specifcation giving types actions used at the leaves of the trees.
Te typing rules are as follows, with lef 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:
A Resourceful Reframing of Behavior Trees 1:13
Te seq operator is defned as follows:
It can be interpreted as pushing the requirements of the frst formula to the outside of the whole formula, then conjoining its consequences with the specifcation of the second formula. Te correctness of this defnition, 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 is fat, i.e. consists only of propositions of the form S, then there exists
Proof. By induction on the defnition of seq. We show the interesting cases.
Assume . In this case, we can just tensor together the frst state and feed it into the second. by untensoring that proposition to get to the assumption.
Proof. By lexicographic induction on the typing derivation and proof. We show the sequence case here.
1:14 Chris Martens, Eric Butler, and Joseph C. Osborn
By i.h., . By appropriateequivalence between the positive propostion and context , and by the sequence evaluation rule,
6.5 Example
We now return to the “investigating a sound” example whose evaluation was shown in Section 5.3. Te computed type for the example:
is:
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. Te implementation is writen in 523 lines of Standard ML, including detailed comments, and we authored an additional 448 lines of examples, including those used in this paper.
Te implementation is freely available on GitHub at (URL redacted for double-blind review).
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 efective. 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 specifed by the
language. To account for placing multiple world-manipulating agents into the environment, we
might consider introducing a “parallel” operator to BTL:
We may consider a few options for an operational semantics that warrant a diferent type-
theoretic treatment. For instance, perhaps parallel behaviors split the state and operate in isolation
until complete. Tis behavior could be captured with the rule:
A Resourceful Reframing of Behavior Trees 1:15
Fig. 6. A small-step semantics for BTL without failure.
Tese behaviors will only succeed if they interact when run; a1’s action give(a2,O) will only succeed if a2’s frst action, move(a2,L), is permited to succeed frst. Figure 5 describes visually the behavior specifcation we would like to result in this interaction.
To account for such fne-grained concurrent behaviors formally, we require a small-step semantics over the judgment . 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 satisfed, instead permiting the possibility of a delayed transition if their conditions become satisfed 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 lef to work.
8.2 Theoretical extensions
In addition to accounting for parallel execution, we also need to consider repeater nodes. Te operational semantics are fairly easy to specify, but guaranteeing convergence of computing fxed
1:16 Chris Martens, Eric Butler, and Joseph C. Osborn
points for a type-based characterization may prove difcult. 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 verifcation on top of the type system. For instance, selectors are ofen 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. Tis corresponds to provability between e.g. 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 efect that the situations in which types fail to yield a fat context (because there is some implication that cannot be discharged on the lef, say) correspond to the failure cases of execution. We expect this proof will be more difcult than the former.
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. Tis work represents substantial new ground broken towards a longer-term vision of authoring robust, designer-friendly specifcations 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 specifcation precludes examining the entire tree; and certifed behaviors that are guaranteed to succeed under certain environments. Tese features would improve the efectiveness of developing agents in virtual worlds with varied applications in entertainment, arts, simulation modeling, research competitions and challenges, and computing education.
[1] David Baelde. 2012. Least and greatest fxed 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 Peter 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 Artifcial Intelligence and Interactive Digital Entertainment Conference.
[12] Alejandro Marzinoto, Michele Colledanchise, Christian Smith, and Peter ¨Ogren. 2014. Towards a unifed behavior trees framework for robot control. In Robotics and Automation (ICRA), 2014 IEEE International Conference on. IEEE, 5420–5427.
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. Teoretical Computer Science 113, 2 (1993), 349–370.
[14] Drew McDermot, Malik Ghallab, Adele Howe, Craig Knoblock, Ashwin Ram, Manuela Veloso, Daniel Weld, and David Wilkins. 1998. PDDL-the planning domain defnition 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 Sch¨urmann. 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.