# Questions tagged [buchi-automata]

Büchi automata are finite-state automata used to specify languages of infinite strings.

26 questions
2answers
88 views

### Buchi automata in formal software verification

As I am studying the application of Buchi automata in formal software verification, I am interested in the computational complexity (or links to papers) for the algorithms used to solve the problem in ...
1answer
35 views

### Transformation of a Product Buchi Game to a Parity Game

Is there anyway to express a Product Buchi game as a parity game? There is no stochasticity in my original turn-based game and a Deterministic Buchi Automaton is constructed for LTL specifications.
1answer
46 views

### Acceptance conditions when translating LTL to Büchi automaton?

As an exercise in better understanding, I have been implementing the LTL to Generalized Büchi Automaton translation algorithm of Gerth, et al. (which is also discussed in Clarke, et al., Model ...
2answers
727 views

### Why are non-deterministic Buchi automata factorially succinct when compared to deterministic Rabin Automata?

I am trying to demonstrate the following idea without success. There are infinitely many $n \in \mathbb{N}$ such that: There is a non-deterministic Buchi automata of size $n$ such that a ...
1answer
164 views

### The set of all eventually periodic words is not Buchi Recognizable?

An $\omega$-word $s \in \Sigma^\omega$ is eventually periodic if it is of the form $s = uv^\omega$ for finite words $u, v \in \Sigma^*$. I want to show that the set of all eventually periodic words ...
1answer
41 views

### Given a regular language $U$, when does there exist $V$ such that $U^\omega$ = $\lim V$?

What I know is that $W = \lim V$ for some $V$ if and only if $W$ is the language of some deterministic buchi automata, namely that of $V$. So, to attack this problem I tried to come up with some ...
0answers
153 views

### How to draw a Non Deterministic Buchi Automaton (NBA) from the given property?

I'm new to LTL and Buchi automaton, and I have a hard time in constructing NBA from the given formula or the property. Could somebody please help me? The following property is given, P= "Whenever ...
1answer
87 views

1answer
83 views

### Which language is accepted by this Muller Automaton?

In my opinon the Language recognised is this: $(a + b)^* (ab)^ω$ but the solution provided is: $(a + b)^* (a + b)^ω$ Did I missunderstand the acceptance condition or is the solution wrong? My ...
1answer
60 views

### Efficient Algorithm Linear Temporal Logic to Deterministic Rabin Automata

I am trying to construct an equivalent Deterministic Rabin Automata (DRA) given a Linear Temporal Logic (LTL) Formula. One (expensive) way to do this would be to construct an equivalent Non-...
1answer
122 views

### What are the steps/tricks/tips to construct a Büchi automaton from a given language?

Let's say I have this language: $(a + bc)^∗((b + c)a^ω + (abb^∗)^ω)$ It seems pretty complicated, where should I begin with if I were to construct a Büchi automaton? I've been doing it the ...
3answers
1k views

### What is the difference between finite automata and Büchi automata?

as the title suggests, I was struggling to define the differences between finite and Büchi automata and how they are represented. From an assignment I'm working on, this automaton can be depicted as ...
1answer
120 views

3answers
371 views