The tag has no wiki summary.

learn more… | top users | synonyms

2
votes
1answer
30 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
64 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
200 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
64 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}$ ...
20
votes
2answers
531 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 ...
7
votes
1answer
232 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 ...