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

learn more… | top users | synonyms

0
votes
1answer
24 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 ...
2
votes
2answers
35 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 ...
7
votes
1answer
53 views

Proving that a (tree) language is not Buchi recognizable

I'm reviewing some notes about tree automata and I'm trying to conclude a proof that the professor left incomplete. The statement is: Let $A = \{a,b\}$ and $T = \{t \in T_A^{\omega} \mid ...
0
votes
0answers
14 views

Simulation Relation Between Two Büchi Automata

Suppose you have two Büchi Automata: $A=(Q_A,\Sigma,I_A,\delta_A,F_A)$ $B=(Q_B,\Sigma,I_B,\delta_B,F_B)$ where: $Q_A$ and $Q_B$ are finite sets of states $\Sigma$ is the input alphabet ...
1
vote
1answer
52 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 ...
2
votes
3answers
248 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 ...
2
votes
1answer
47 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 ...
2
votes
1answer
85 views

Proving that the continuation of a non-regular language is not ω-regular

I want to prove that a language is not $\omega$-regular. The language I'm working with can be defined as: $$L = \{ a_1 \dots a_n x^\omega ~ | ~ n > 0, a_1 \dots a_n \in L^\prime \}$$ where ...
3
votes
3answers
261 views

Distributivity of $\omega$-regular expressions

Recall that a language is $\omega$-regular if and only if it is recognized by a Büchi automaton. How can I prove that $\qquad (E_1 + E_2).F^\omega$ is equivalent to $\qquad ...
2
votes
1answer
67 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}$ ...
23
votes
2answers
634 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 ...
8
votes
1answer
358 views

Algorithm to translate a deterministic Büchi automaton to LTL (when possible)

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