Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [buchi-automata]

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

1
vote
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 ...
1
vote
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.
2
votes
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 ...
1
vote
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 ...
1
vote
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 ...
0
votes
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 ...
0
votes
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 ...
3
votes
1answer
87 views

Minimal Deterministic Buchi Automata Product

Problem: Let $\varphi = \varphi_1 \land \varphi_2$ be Deterministic Buchi Automata (DBA) expressible LTL formulas. Let $A$, $A_1$ and $A_2$ be translated DBAs such that ${\cal{L}}(A) = {\cal{L}}(A_1)...
0
votes
1answer
85 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.
1
vote
1answer
90 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 ...
1
vote
1answer
81 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?
0
votes
1answer
88 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 ...
6
votes
1answer
150 views

Büchi automata: accepting run vs. runs with arbitrarily many final states

I am currently learning about Büchi automata and have a combinatorial question about the acceptance condition. Let $A=(Q,\Sigma,\delta,q_0,F)$ be a (nondeterministic finite) Büchi automaton and $w=...
0
votes
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 ...
5
votes
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-...
1
vote
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 ...
5
votes
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 ...
7
votes
1answer
120 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 \text{...
1
vote
1answer
75 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$-...
2
votes
3answers
297 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
75 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
154 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 $L^\...
3
votes
3answers
371 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 {E_1.(F^\omega)+E_2.(F^\...
2
votes
1answer
78 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}$ ...
29
votes
2answers
912 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 ...
10
votes
1answer
674 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 ...