patternMinor
Time to construct a GNBA for LTL formula
Viewed 0 times
ltltimeforconstructgnbaformula
Problem
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:
-
$\operatorname{Word}(\varphi)=L_{\omega}(G_{\varphi})$.
-
$G_{\varphi}$ can be costructed in time and space $2^{O(|\varphi|)}$, where $|\varphi|$ is the size of $\varphi$.
-
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?
Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ over alphabet $2^{AP}$ such that:
-
$\operatorname{Word}(\varphi)=L_{\omega}(G_{\varphi})$.
-
$G_{\varphi}$ can be costructed in time and space $2^{O(|\varphi|)}$, where $|\varphi|$ is the size of $\varphi$.
-
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?
Solution
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.
$\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.
Context
StackExchange Computer Science Q#2531, answer score: 3
Revisions (0)
No revisions yet.