A semantics for Behavior Trees using CSP with specification commands

In this paper we give a formal definition of the requirements translation language Behavior Trees. This language has been used with success in industry to systematically translate large, complex, and often erroneous requirements documents into a structured model of the system. It contains a mixture of state-based manipulations, synchronisation, message passing, and parallel, conditional, and iterative control structures. The formal semantics of a Behavior Tree is given via a translation to a version of Hoare’s process algebra CSP, extended with state-based constructs such as guards and updates, and a message passing facility similar to that used in publish/subscribe protocols. We first provide the extension of CSP and its operational semantics, which preserves the meaning of the original CSP operators, and then the Behavior Tree notation and its translation into the extended version of CSP.

Research highlights
► We present an extension of CSP with hierarchical state and specification commands.
► It also extends CSP with message passing, in which the sender is not blocked.
► Its operational semantics uses transition labels that include specification commands.
► We formalise Behavior Trees, a notation for capturing behavioural requirements.
► The formalisation is given by translation into extended CSP.