Time to construct a GNBA for LTL formula

Question

I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula:

Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ over alphabet $2^{AP}$ such that:

1. $\operatorname{Word}(\varphi)=L_{\omega}(G_{\varphi})$.

2. $G_{\varphi}$ can be costructed in time and space $2^{O(|\varphi|)}$, where $|\varphi|$ is the size of $\varphi$.

3. The number of accepting states of $G_{\varphi}$ is bounded above by $O(|\varphi|)$.

My problem lies in the proof of (2), that is, in the proof it says that the number of states in $G_{\varphi}$ is bounded by $2^{|\operatorname{subf}(\varphi)|}$ but since $|\operatorname{subf}(\varphi)| \leq 2\cdot|\varphi|$ (where $\operatorname{subf}(\varphi)$ is the set of all subformulae) the number of states is bounded by $2^{O(|\varphi|)}$.

But why does $|\operatorname{subf}(\varphi)| \leq 2\cdot|\varphi|$ hold?

Answer 1

In general, logical formulae can be thought of as trees; inner nodes are operators and leaves are atomic propositions. Therefore, every formula consists of as many direct subformulae (that is on the first level) as its top-most operator's arity. For example,

$\qquad \varphi \land \psi$

has two direct subformulae $\varphi$ and $\psi$. This can be continued recursively and we see that

$\qquad \displaystyle |\operatorname{subf}(\varphi)| \leq \sum_{\circ \in \operatorname{op}(\varphi)} \operatorname{arity}(\circ)$,

where $\operatorname{op}(\varphi)$ is the multi-set of operators occurring in $\varphi$. Informally speaking, every operator contributes its operands to the set of subformulae. Note that we have $\leq$ and not $=$ because a subformula might occur multiple times.

In LTL, all operators have at most arity two, so $|\operatorname{subf}(\varphi)| \leq 2|\varphi|$ provided that $|.|$ counts (at least) operator occurrences.