5
votes
Why are non-deterministic Buchi automata factorially succinct when compared to deterministic Rabin Automata?
This is Theorem 1.30 in the chapter "Omega-Automata" in the book "Automata, Logics, and Infinite Games: A Guide to Current Research" edited by Erich Grädel, Wolfgang Thomas and Thomas Wilke. They have ...
- 2,797
5
votes
Büchi automata: accepting run vs. runs with arbitrarily many final states
Consider $\Sigma = \{0,1\}$ and $w = 1101001000100001\ldots$, i.e., there is an increasing number of zeros between two ones. Now consider the automaton with states $q_0, q_1$, and $q_A$ where $q_A$ is ...
- 441
4
votes
Accepted
Büchi automaton to Linear Temporal Logic
Since Büchi automata are strictly more expressive than LTL, such a translation is not possible in the general case.
For instance, the language $L = \{w_0 w_1 w_2 \ldots \in (2^{\{a\}})^\omega \mid \...
- 2,797
4
votes
Accepted
What kind of LTL formula can be represented by DBAs
You can define syntactic fragments of LTL that ensure that all properties expressible in these fragments are representable as DBAs. An example is given in the paper "A LTL Fragment for GR(1)-Synthesis"...
- 2,797
4
votes
Minimal Deterministic Buchi Automata Product
This is only a partial answer (as I believe that the state of the art is insufficient to answer your questions completely - I am happy to be proven wrong here), but I hope that it helps you anyway.
...
- 2,797
3
votes
Accepted
Efficient Algorithm Linear Temporal Logic to Deterministic Rabin Automata
There is a very recent tool to translate from LTL directly to deterministic Rabin automata. It can be obtained here:
https://www7.in.tum.de/~sickert/projects/ltl2dra/
The page not only contains a ...
- 2,797
3
votes
Accepted
The set of all eventually periodic words is not Buchi Recognizable?
Note that every non-empty Büchi recognizable language contains at least one eventually periodic word and that the class of all Büchi recognizable languages is closed under complement. Thus, if the ...
- 1,856
2
votes
Accepted
Which language is accepted by this Muller Automaton?
The solution given is incorrect.
The first clue that this might be the case is that $(a+b)^*(a+b)^\omega$ is a strange way to write anything: any finite number of $a$s and/or $b$s, followed by ...
- 82.2k
2
votes
Accepted
LTL to GBA versus LTL to BA
There is no precise answer to this.
The smallest GBA for a given language is never larger than the smallest BA for a given language, simply by the fact that BAs are a special case of GBAs.
It is easy ...
- 2,797
2
votes
Accepted
Generalized Büchi Automata - Formal definition of a state appearing infinitely often?
The definition and example are both correct.
If the automaton reads $a$ in state $2$ or reads $b$ in state $1$, then it rejects, because it has no state to go to. So, if the ...
- 82.2k
2
votes
Acceptance conditions when translating LTL to Büchi automaton?
I will start with the last question and then come to the question at the top of your post.
The construction assumes that the LTL formula is given in negation normal form, so that no temporal operator ...
- 2,797
2
votes
Why are non-deterministic Buchi automata factorially succinct when compared to deterministic Rabin Automata?
Usually, when defining the size of a Rabin automaton, we take into consideration the automaton's index (the number of Rabin pairs) and not only the number of states. What you asked for is well-known, ...
- 4,874
2
votes
Accepted
Buchi arithmetic meaning
The wedge sign means AND. The formula states that $\mathbf{A}x=c$ and for all $i \in I$, $V_p(x_i) = y_i$.
- 279k
1
vote
LTL Model Checking Worst Case size for NBA
For a lower-bound, for $n\geq 1$, consider the following language over $\{0, 1, \#, \text{$\\\$$}\}$: $$ L_n = \{ \{ 0, 1, \#\}^* \cdot \#\cdot w\cdot \# \cdot \{ 0, 1, \#\}^* \cdot $ \cdot w\cdot \#^\...
- 4,874
1
vote
Accepted
Is the language with at least as many 0 as 1 on any prefix $\omega$ regular?
As you suspected, $L$ is not büchi recognisable/$\omega$-regular. Here is a proof.
Towards a contradiction, suppose $L$ is $\omega$-regular. Then $$L= A_1B_1^\omega\cup A_2B_2^\omega\cup\cdots\cup ...
- 39.1k
1
vote
Accepted
Equivalence of states between two "quasi-deterministic" strongly connected Büchi automata accepting the same $\omega$-language
Your property does not hold.
Consider the following languages over $\Sigma = \{a,b\}$:
There are infinitely many $a$s at even positions in a word
There are infinitely many $a$s at odd positions in a ...
- 2,797
1
vote
Accepted
Buchi automata in formal software verification
A Buchi automaton has a non-empty language if and only if there is an accepting lasso, i.e., a path from an initial state to some lasso starting state $s$, and a loop from $s$ to itself along which an ...
- 2,797
1
vote
Buchi automata in formal software verification
The fastest theoretical algorithm to solve Büchi Games in game graphs is presented in [1] and runs in $O(n^2)$: The algorithm uses a hierarchical decomposition approach. An easier folklore algorithm ...
- 196
1
vote
Transformation of a Product Buchi Game to a Parity Game
I will assume that by "Product Buchi game", you mean the (synchronous) product of a deterministic Buchi automaton and some kind of plant or deterministic finite automaton that represents the rules of ...
- 2,797
1
vote
Accepted
Given a regular language $U$, when does there exist $V$ such that $U^\omega$ = $\lim V$?
Consider the language $$U = U_1 \mid U_2 = a\Sigma^* \mid (\Sigma \setminus \{c\})^* b$$ for the alphabet $\Sigma = \{a,b,c,d\}$.
Let $\mathcal{A}$ be a deterministic Büchi automaton for the language ...
- 2,797
1
vote
Buchi Automaton G(Xa->b)
The formula states that for all $n$, if $a$ holds at time $n+1$ then $b$ holds at time $n$. If $a$ never holds then the formula is trivially true.
- 279k
Only top scored, non community-wiki answers of a minimum length are eligible