

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer

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.


share|cite|improve this question
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? – Pål GD Jan 16 '13 at 11:11
up vote 6 down vote accepted

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\}$.

share|cite|improve this answer

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$.

share|cite|improve this answer

Your Answer


