after k levels if BSi|= ℓ
∗ k
(f). Since we only have labels for literals, we substitute the labels of literals for the literals in a formula to get the extended label of the formula. The extended label of a propositional formula f at level k, is defined:

ℓ
∗ k
(f ∧ f
′) = ℓ
∗ k
(f) ∧ ℓ
∗ k
(f
′),
ℓ
∗ k
(f ∨ f
′) = ℓ
∗ k
(f) ∨ ℓ
∗ k
(f
′),
ℓ
∗ k
(¬(f ∧ f
′**)) =** ℓ
∗ k
(¬f ∨ ¬f
′),
ℓ
∗ k
(¬(f ∨ f
′**)) =** ℓ
∗ k
(¬f ∧ ¬f
′),
ℓ
∗ k
(⊤) = BSP ,
ℓ
∗
$$\begin{array}{c}{{\epsilon_{k}(-)}}\\ {{\ell_{k}^{*}(l)}}\end{array}$$
(⊥) =⊥,
(l) = ℓk(l)
The zeroth action layer for CBTC is:
A0 = {Flush, inP1p,¬inP2p, inP2p,¬inP1p, clogp
, armp}
ℓ0(Flush) = BSP ,
ℓ0(inP1p) = ℓ0(¬inP2p**) = (**arm ∧ clog ∧ inP1 ∧ ¬inP2),
ℓ0(inP2p) = ℓ0(¬inP1p**) = (**arm ∧ clog ∧ ¬inP1 ∧ inP2),
ℓ0(clogp
) = ℓ0(armp) = BSP
Each literal persistence has a label identical to the label of the corresponding literal from the previous literal layer. The Flush action has BSP as its label because it is always applicable.

Effect Layer: The effect layer Ek depends both on the literal layer Lk and action layer Ak. Ek contains an effect ϕ j(a) if the effect has a non false label (i.e. ℓk(ϕ j(a)) 6=⊥). Because both the action and an effect must be applicable in the same world, the label of the effect at level k is the conjunction of the label of the associated action with the extended label of the antecedent ℓk(ϕ j(a**)) =** ℓk(a) ∧ ℓ
∗ k
(ρ j(a))
The zeroth effect layer for CBTC is:
E0 = {ϕ 0(Flush), ϕ0(inP1p), ϕ0(¬inP2p), ϕ0(inP2p),
ϕ 0(¬inP1p), ϕ0(clogp
), ϕ0(armp)}
ℓ0(ϕ 0(Flush**)) =** BSP
ℓ0(ϕ 0(inP1p**)) =** ℓ0(ϕ 0(¬inP2p**)) = (**arm ∧ clog ∧ inP1 ∧ ¬inP2),
ℓ0(ϕ 0(inP2p**)) =** ℓ0(ϕ 0(¬inP1p**)) = (**arm ∧ clog ∧ ¬inP1 ∧ inP2),
ℓ0(ϕ 0(clogp
)) = ℓ0(ϕ 0(armp**)) =** BSP
Again, like the action layer, the unconditional effect of each literal persistence has a label identical to the corresponding literal in the previous literal layer. The unconditional effect of Flush has a label identical to the label of Flush.

Literal Layer: The literal layer Lk depends on the previous effect layer Ek−1, and contains only literals with non false labels (i.e. ℓk(l) 6=⊥). An effect ϕ j(a) ∈ Ek−1 contributes to the label of a literal l when the effect consequent contains the literal l. The label of a literal is the disjunction of the labels of each effect from the previous effect layer that gives the literal:

$$\ell_{k}(l)=\bigvee_{\begin{array}{c}{{\varphi^{j}(a):l\in\varepsilon^{j}(a),}}\\ {{\varphi^{j}(a)\in\mathcal{E}_{k-1}}}\end{array}}\ell_{k-1}(\varphi^{j}(a))$$
