In the paper Fast LTL to Buchi Automata Translation (2001, Gastin and Oddoux) the authors, while defining co-Buchi alternating automata define $\Sigma’= 2^\Sigma$ where $\Sigma$ is the alphabet. They say that because of this the transitions that differ only by action can be gathered.

What does this statement exactly mean? Any pointers will be helpful.


  • $\begingroup$ Can you restate your question, it's slightly hard to understand what you mean. You understand that $2^\Sigma$ means the powerset of $\Sigma$? And that if you take the new alphabet $\Sigma'$ to be the powerset of the original, then you can branch on subsets of the alphabet? $\endgroup$
    – Pål GD
    Commented Jan 16, 2013 at 11:11

2 Answers 2


Expanding on Markus' answer a bit, note that the alphabet $\Sigma$ is in turn the powerset $2^{Prop}$ of the set $Prop=\{p_1,\dots,p_k\}$ of atomic propositions, i.e. it represents the set of valuations $a:Prop\to\{T,F\}$ of the $p_i$.

In the LTL formula, most boolean subformulas involve only a few of the propositions. In the translation, any such subformula corresponds to the set of all valuations $a\in\Sigma$ satisfying it, which is typically large. Using $\Sigma'$, you still only have one transition.

For example, Figure 1 in the paper shows an automaton with transitions labelled simply by $p$ or $q\wedge\neg r$ (where $p,q,r$ are the propositions from the formula). Using $\Sigma$, for the first you would instead have four transitions labelled $\{p\},\{p,q\},\{p,r\},$ and $\{p,q,r\}$.


I only had a quick look at the paper, but it sounds as if they mean the following. If there are two transitions from state $s_1$ to state $s_2$ with different labels $a$ and $b$, they "group" them into one transition with label $\{a,b\}$. However, they write that they interpret the set in such a way that the resulting automaton still accepts the same words in $\Sigma^{\omega}$. The sets of actions are represented as boolean expressions about the actions, e.g. $a\vee b$. That is, they simply choose a more efficient datat structure than listing the possible transitions from $s_1$ to $s_2$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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