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

<p>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.</p>

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

CC BY-SA 3.0
2013-01-16T11:58:39.687Z
2013-01-16T11:58:39.687Z
Klaus Draeger
<p>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$. </p>

CC BY-SA 3.0
2013-01-16T11:14:49.147Z
2013-01-16T11:22:12.767Z
2013-01-16T11:22:12.767Z
Markus
<p>In the paper <em>Fast LTL to Buchi Automata Translation</em> (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. </p>

<p>What does this statement exactly mean? Any pointers will be helpful.</p>

<p>thanks</p>

CC BY-SA 3.0
2013-01-16T11:11:33.663Z
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?
John K.
<automata-theory><temporal-logic>
Alternating automata
pratibha sawhney
# Alternating automata

(Asked by: username_0 on 2013-01-16)

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.

thanks

**Tags:** automata-theory, temporal-logic
> **Comments:**
> **username_1**: 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?  

---

## 2 answers

### Answer by username_2 on 2013-01-16. Score: 6 | Accepted answer

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


---

### Answer by username_3 on 2013-01-16. Score: 4

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


---

