Talk:Weak Büchi automaton

Weak non-deterministic Büchi automata are more expressive than weak deterministic Büchi automata

The text "Weak Büchi automata are equivalent to deterministic Weak Büchi automata." is actually wrong, as the property F G p0 (Finally Globally p0) can be expressed by a weak non-deterministic Büchi automaton (the standard automaton for F G p0 does the trick), whereas weak deterministic automata cannot express this property (as already deterministic Büchi automata cannot express this property). As a proof, the following automaton given in the HOA format (see https://adl.github.io/hoaf/) is weak and non-deterministic and accepts F G p0:

name: "FGp0"
States: 3
Start: 0
AP: 1 "p0"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: stutter-invariant very-weak
--BODY--
State: 0
[t] 0
[0] 1
State: 1 {0}
[0] 1
[!0] 2
State: 2
[t] 2
--END--

That deterministic Büchi automata and therefore also weak deterministic Büchi automata cannot express F G p0 is commonly known, see e.g. Principles of Model Checking from Christel Baier and Joost-Pieter Katoen. 141.76.60.172 (talk) 14:19, 4 March 2019 (UTC)

 My bad. I wrote the mistake. I really don't understand why I ever thought the article I quote stated this. I added a source for the statement which are now in the article. The minimization is indeed in the article, so I added it back. Arthur MILCHIOR (talk) 18:19, 1 April 2019 (UTC)