Content deleted Content added
→Gerth et al. algorithm: During Step 2. LGBA construction, the label of each state are atomic propositions, thus in the statement a ⊆ {p ∈ ''P'' | ¬p ∉ ''Now''(q) } } , p should be also an atomic proposition. |
m Robot - Moving category Automata theory to Category:Automata (computation) per CFD at Wikipedia:Categories for discussion/Log/2015 October 22. |
||
Line 251:
{{DEFAULTSORT:Linear temporal logic to Buchi automaton}}
[[Category:Automata
[[Category:Model checking]]
[[Category:Temporal logic]]
| |||