# Questions tagged [buchi-automata]

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

32 questions
Filter by
Sorted by
Tagged with
1 vote
42 views

### LTL Model Checking Worst Case size for NBA

I have a slide that gives the worst case time complexity of LTL model checking which uses a product construction of an LTS along with the NBA for the negation of the LTL formula. My question is, when ...
• 90
55 views

243 views

### LTL to GBA versus LTL to BA

Let's assume that I have an LTL formula and I want to convert it to a Buchi automaton. For which fragment of LTL, GBA is more succinct and for which fragment BA has the same size as GBA.
• 175
1 vote
225 views

### Generalized Büchi Automata - Formal definition of a state appearing infinitely often?

I am studying generalized Büchi automata and I don't really understand when a state is considered to appear infinitely often. The definition I have is: A state $s$ appears infinitely often if there ...
• 225
1 vote
168 views

### What kind of LTL formula can be represented by DBAs

I am looking for the portion of LTL formula that can be expressed by deterministic buchi automata. Is there any classification of this such?
• 175
121 views

### Buchi Automaton G(Xa->b)

I have a question regarding buchi automatons. The automata for the LTL formula, G(Xa->b) is as the attached picture. Why dosen't a have to be true in order to make the automaton correct? My ...
231 views

• 807
1 vote
129 views

### Complexity of recognizing whether two $\omega$-regular expressions represent the same language

If the complexity of recognizing whether two regular expressions represent different languages is EXPSPACE-complete, then what can be said for the complexity of recognizing whether two $\omega$-...
389 views

### Why do all non-empty ω-regular languages have periodic members?

I was learning about Büchi Automata and couldn't understand a part where they were describing "Non-empty $\omega$-regular languages contain periodic strings" Let $A$ be a Büchi automaton ...
• 21
102 views

### Omega-Language to Büchi automaton

I'm currently preparing a presentation about LTL and a book says that the language $L = (a(a \cup b))^\omega$ cannot be described by any LTL (or FO) formula which is understandable but how does the ...
• 227
320 views

106 views

### Büchi automaton with modified acceptance condition

Consider a Büchi automaton $\mathcal{A}$ with the modified acceptance condition, that an $\omega$-word $\mathcal{w}$ is accepted by $\mathcal{A}$ iff every run $\rho$ of $\mathcal{A}$ on $\mathcal{w}$ ...
• 173
1k views

### Equivalence of Büchi automata and linear $\mu$-calculus

It's a known fact that every LTL formula can be expressed by a Büchi $\omega$-automaton. But, apparently, Büchi automata are a more powerful, expressive model. I've heard somewhere that Büchi automata ...
• 2,197
Linear temporal logic and deterministic Büchi automata are incomparable: DBA cannot express $FGa$, and LTL cannot express "at least each odd letter is 'a'". But sometimes it is interesting to know ...