This page aims at comparing our approach to the one proposed by the authors of the following paper:
Enabling Behaviour Tree Verification via a Translation to BIP by Qiang Wang1, Huadong Dai1, Yongxin Zhao2, Min Zhang2 & Simon Bliudze3
Academy of Military Sciences, Beijing, China 18513688908@163.com
East China Normal University, Shanghai, China
Univ. Lille, Inria, CNRS, Centrale Lille, CRIStal, UMR 9189, 59000 Lille, France, simon.bliudze@inria.fr
This paper presents a very similar approach to the one we introduce here in these pages. The main differences being that they propose BIP as a formal framework to model Behavior Trees. Yet, they use model checking (not D-Finder as the original BIP implementation did) to check for formal properties. Moreover, even if BIP comes with an engine, they do not yet propose a runtime engine to execute the behavior tree (as we do with Hippo).
Yet, it is interesting to compare the produced model and what can be achievd with both of them.
The authors propose an implementation of their tool: xml2bip
They also prvide some example with the synthesized BIP code mytree.bip which corresponds to the first example: mytree.xml (the mars rover which must avoid to have its panel unfolded during a storm).
<?xml version="1.0"?>
<root name="Depth">
<BehaviorTree ID="MainTree" name="maintree">
<Fallback name="root_fallback">
<Sequence name="sequences_1">
<Condition ID="lowpower" name="low_power" var="" guard=""/>
<Action ID="unfoldpanels" name="unfold_panels" var="" action=""/>
</Sequence>
<Sequence name="sequences_2">
<Condition ID="storm" name="in_storm" var="" guard=""/>
<Action ID="hibernate" name="in_hibernate" var="" action=""/>
</Sequence>
<Sequence name="sequences_3">
<Action ID="getdata" name="get_data" var="" action=""/>
<Action ID="send" name="send_data" var="" action=""/>
</Sequence>
</Fallback>
</BehaviorTree>
</root>and a property they want to prove:
property="INVARSPEC !( (in_storm_c.NuVstorm = TRUE) &(root_fallback_c.Nuplace = NuSls) )”
They want to show that there is a reachable state state where there is storm while the solar pannel are unfolded (which is a problem).
Although this cannot happen if you run the BT only once, but if it keeps running in a loop (which makes sense in this setup), then indeed, such a state can indeed be reached.
Using our formalism:
We get the Fiacre model in the file mars_rover2.fcr included, and the property can also be checked:
sift -stats mars_rover2.tts -rsd mars_rover2.tts/mars_rover2.ktz 417552 classe(s), 406584 marking(s), 88 domain(s), 2148949 transition(s) 11.957s
At the end of the Fiacre file we added:
prove absent ( mars_rover2/3/state Unfolded and mars_rover2/1/state Storm )
and indeed, when calling
scan mars_rover2.tts/mars_rover2.ktz -n "(sv__panel__automata_1_sUnfolded /\ sv__meteo__automata_1_sStorm)" -b -script
we get
never (sv__panel__automata_1_sUnfolded /\ sv__meteo__automata_1_sStorm) FALSE
Similarly, we looked at the second example (in mytree2.xml and mytree2.bip), which are slightly different from the one on figure 8 of the paper.
<?xml version="1.0"?>
<root name="example2">
<BehaviorTree ID="MainTree" name="maintree">
<Sequence name="root_sequence">
<Fallback name="fallback_1">
<Sequence name="sequence_1">
<Condition ID="speed" name="IsSpeedZero" var="speed" guard="speed==0"/>
<Action ID="stop" name="StopTrain" var="stop" action="stop=1"/>
</Sequence>
<Sequence name="sequence_2">
<Condition ID="stop" name="IsStopped" var="stop" guard="stop==1"/>
<Action ID="door" name="OpenDoor" var="door" action="door=1"/>
</Sequence>
</Fallback>
<Fallback name="fallback_2">
<Sequence name="sequence_3">
<Condition ID="door" name="IsDoorClosed" var="door" guard="door==0"/>
<Action ID="speed" name="Speedup" var="speed" action="speed=speed+1"/>
</Sequence>
<Sequence name="sequence_4">
<Condition ID="speed" name="IsSpeedPositive" var="speed" guard="speed>0"/>
<Action ID="speed" name="Speeddown" var="speed" action="speed=speed-1"/>
</Sequence>
</Fallback>
</Sequence>
</BehaviorTree>
</root>Again indeed, you can get from a satisfying state (d = false, v = 0, s = true) (door close, stopped and speed = 0, to a falsifying state (d =
true, v = 1, s = true), i.e. door open, train stopped and speed = 1 when the BT runs in a loop.
With our formalism, we get the Fiacre model in the file train.fcr included, and the property can also be checked.
If we add at the end of train.fcr file:
prove absent maintree/12/value (speed=1 and door_open=1 and stopped =1)
We compile (build the reachable space) it:
sift -stats train.tts -rsd train.tts/train.ktz 948 classe(s), 948 marking(s), 19 domain(s), 2326 transition(s) 0.019s
then checking the property:
scan train.tts/train.ktz -n "(maintree_1_vspeed = 1) /\ (maintree_1_vdoor__open = 1 /\ (maintree_1_vstopped = 1))" -b -script
we get:
never (maintree_1_vspeed = 1) /\ (maintree_1_vdoor__open = 1 /\ (maintree_1_vstopped = 1)) FALSE
which means that the state can be reached (it is not absent).
From a pure model and verification point of view, it is not clear which formalism is better. They both provide automata with guarded transition. BIP uses ports for automata transition synchronisation, and Fiacre provides also ports and shared variable. See section Combining BT nodes to build the complete BT which explains how the Fiacre processes are put together.
One clear advantage of Fiacre approach is the Hippo engine which allows C code execution starting on some transitions and sync on returned value, but also external events connected to C functions. Numerous examples show the execution of such BT and simulated drones, or with ROS2 navigation stack.
Other documentation pages to check on BT2Fiacre: