

![0_image_0.png](0_image_0.png)

The LUG for CBTC, shown in Figure 7 (without labels), using BSP =BSI has the initial literal
layer:
L0 = {inP1,¬inP2, inP2,¬inP1, clog, arm}
$$\begin{array}{l}{{{\cal L}_{0}=\{\mathtt{inP1},\neg\mathtt{inP2},\mathtt{inP2},\neg\mathtt{inP1},\mathtt{clip},\mathtt{dim}\}}}\\ {{\ell_{0}(\mathtt{inP1})=\ell_{0}(\neg\mathtt{inP2})=(\mathtt{arm}\wedge\mathtt{clog}\wedge\mathtt{inP1}\wedge\neg\mathtt{inP2}),}}\\ {{\ell_{0}(\mathtt{inP2})=\ell_{0}(\neg\mathtt{inP1})=(\mathtt{arm}\wedge\mathtt{clog}\wedge\neg\mathtt{inP1}\wedge\mathtt{inP2}),}}\\ {{\ell_{0}(\mathtt{clog})=\ell_{0}(\mathtt{arm})=B S_{P}}}\end{array}$$
Notice that inP1 and inP2 have labels indicating the respective initial states in which they hold,
and clog and arm have BSP as their label because they hold in all states in BSP .

Action Layer: Once the previous literal layer Lk is computed, we construct and label the action layer Ak. Ak contains causative actions from the action set A, plus literal persistence. An action is included in Ak if its label is not false (i.e. ℓk(a) 6=⊥). The label of an action at level k, is equivalent to the extended label of its execution precondition:

$$\ell_{k}(a)=\ell_{k}^{*}(\rho^{e}(a))$$

Above, we introduce the notation for extended labels ℓ
∗ k
(f) of a formula f to denote the worlds of BSP that can reach f at level k. We say that any propositional formula f is reachable from BS