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?


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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.