Talk:Linear temporal logic to Büchi automaton

There are several errors on the algorithm

I tried to write the code from the figure (code) and the code was not working. When I checked the paper, there was several differences which may heavily affect the behavior. But anyway, thanks to contributors, it was a good starting point. — Preceding unsigned comment added by 151.16.163.204 (talk) 22:13, 21 January 2013 (UTC)[reply]

I tried to simplify their presentation. Can you report exact error? Ashutosh Gupta (talk) 21:42, 2 September 2013 (UTC)[reply]

I implemented the second algorithm in a toy language named Egel and can confirm it seems correct. (The github link that might change at any moment, sorry: https://github.com/egel-lang/vlo/blob/main/src/buechi.eg )

What? Please have mercy on the ignorant...

I am sure that this article is informative, well-sourced, and very useful to those who know what the heck it is about. Can I ask, for the benefit of those who happen on this page by chance, that the lede be expanded a little to give at least some indication of why whatever it is is done to is done to whatever it is done to? The joy of an encyclopaedia is that one can open a page at random, and learn something new. All I've learned on this one is that I am hopelessly ignorant about a subject that I didn't even know existed, and if I want to understand it, I won't find out how to here ;) AndyTheGrump (talk) 00:38, 4 May 2011 (UTC)[reply]

Not everything can be explained in few words. This article is about an important algorithm used in verification of computer systems. To understand this article, one has to read many other articles in the background. I admit that it can be improved significantly. But, I am not a fluent writer. I just wrote what I knew as clearly as possible. I hope someone will straight up this article.Ashutosh Gupta (talk) 08:26, 4 May 2011 (UTC)[reply]

Thanks - I hope you haven't taken my comments too seriously - I didn't intend them as anything other than a light-hearted remark from a passing ignoramus, though there is a serious point too regarding making articles a little more transparent to outsiders where possible. Perhaps someone from WikiProject Computer science could help flesh out the lede a little? I'd have a go myself, but my knowledge of computer science is almost entirely the result of years of amateur programming, and in practice apparently revolves around trying every possible combination of code until I find some that seems to work - not exactly the best way to do things, evidently a little formal analysis and verification might help me too. AndyTheGrump (talk) 13:10, 4 May 2011 (UTC)[reply]

Simplification?

For the action labels 'a' on the Büchi automaton, the requirement currently given is "( M' ∩ AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M' }". But M' is chosen from cs(f), so we should have f₁ ∈ M' iff ¬f₁ ∉ M', and therefore {p ∈ AP | ¬p ∉ M' } = {p ∈ AP | p ∈ M' } = M' ∩ AP. If there is no good reason to keep it this way, I suggest to simplify the requirement to "a = M' ∩ AP". Scranen (talk) 09:10, 22 August 2013 (UTC)[reply]

There can be atomic predicates in AP that do not appear in f. That is why this complication. If we assume that f refers to all predicates from AP then your suggestion is a good choice. Most of the books/papers use your presentation.Ashutosh Gupta (talk) 21:16, 2 September 2013 (UTC)[reply]

Acceptance condition for R (release) in simple algorithm

The section "Transformation from LTL to GBA" has R as part of the GBA construction, but does not have any acceptance condition involving R. I believe this is incorrect, is there a source for this?

To see why the missing acceptance condition is a problem, consider the formula ¬(¬true R true). This formula should be unsatisified, since (¬true R true) always holds. However, when applying the construction presented in the article, we obtain:

Since the acceptance set is empty (no U in the formula), all cycles in this automaton are accepting, so this automaton accepts every word, which is wrong (it should accept nothing, as the formula is unsatisfiable). Bennofs (talk) 11:03, 3 March 2020 (UTC)[reply]

Ah, this case cannot happen since the input formula must be in negation normal form. Nevermind. Still, a source for this particular construction would be nice. Bennofs (talk) 11:07, 3 March 2020 (UTC)[reply]