Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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

share|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
add comment

2 Answers

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|improve this answer
add comment

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|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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