Linear temporal logic to Büchi automaton: Difference between revisions

Content deleted Content added
Line 59:
* f<sub>1</sub> ∨ f<sub>2</sub> ∈ M iff f<sub>1</sub> ∈ M or f<sub>2</sub> ∈ M
|}
Let ''cs''( f ) be the set of maximally consistent subsets of ''cl''( f ).
We are going to use only ''cs''( f ) as the states of GBA.
;GBA construction