Questions tagged [buchi-automata]
Büchi automata are finite-state automata used to specify languages of infinite strings.
32
questions
1
vote
1
answer
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
2
votes
1
answer
55
views
Is the language with at least as many 0 as 1 on any prefix $\omega$ regular?
Let $L$ be the language of infinite words in $\{0,1\}^\omega$ such that any finite prefix of a word in $L$ has at least as many $0$'s as $1$'s. Is $L$ büchi recognisable?
I think that $L$ is not $\...
- 23
4
votes
1
answer
118
views
Are deterministic Büchi automata omega-closed?
As in, given a regular language $V$, does there exist a deterministic Büchi automaton $\mathcal{A}$, or equivalently a regular language $W$ such that $\mathcal{L}(\mathcal{A})=\vec{W}=V^\omega$?
For ...
- 195
1
vote
1
answer
35
views
Buchi arithmetic meaning
I am studying this article. But I have trouble with understanding the Buchi arithmetic. It says in section IV:
... Formulas in this fragment generalise classical integer programming and are of the ...
- 113
3
votes
1
answer
86
views
Equivalence of states between two "quasi-deterministic" strongly connected Büchi automata accepting the same $\omega$-language
Hope someone can point me to the right direction to solve this problem.
Premise.
I call quasi-deterministic Büchi automaton (qDBA) a Büchi automaton $B = \langle S, \Sigma, S_0, \delta, F \rangle$, ...
- 33
2
votes
1
answer
202
views
Büchi automaton to Linear Temporal Logic
Given a Büchi automaton what is the procedure to build an equivalent LTL formula? And what is its size?
I'm looking for references but I haven't found them so far.
- 401
1
vote
2
answers
330
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 ...
- 247
2
votes
1
answer
138
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.
- 21
2
votes
1
answer
239
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 ...
3
votes
3
answers
810
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
1
answer
358
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
1
answer
88
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
0
answers
583
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 ...
- 1
4
votes
1
answer
263
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
1
answer
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
1
answer
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
1
answer
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
0
votes
1
answer
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 ...
- 1
6
votes
1
answer
231
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=...
- 61
0
votes
1
answer
168
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 ...
- 155
5
votes
1
answer
95
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-...
2
votes
1
answer
290
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 ...
- 219
5
votes
3
answers
4k
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 ...
- 219
7
votes
1
answer
291
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{...
- 807
1
vote
1
answer
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$-...
2
votes
3
answers
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
2
votes
1
answer
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
2
votes
1
answer
320
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^\...
- 123
3
votes
3
answers
681
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^\...
- 69
2
votes
1
answer
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
33
votes
2
answers
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
10
votes
1
answer
897
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 ...
- 1,085