Revision as of 15:10, 3 September 2016 edit Csfv (talk \| contribs) 6 edits m →Gerth et al. algorithm ← Previous edit		Revision as of 15:38, 3 September 2016 edit undo Csfv (talk \| contribs) 6 edits m →Gerth et al. algorithm Next edit →
Line 113: ===Gerth et al. algorithm=== The following algorithm is due to Gerth, Peled, [[Moshe Y. Vardi\|Vardi]], and Wolper.<ref name=GPVW93/>; a verified construction mechanism of this by Schimpf, Merz and Smaus <ref name=TPHOLS2009/> is also available. The previous construction creates exponentially many states upfront and many of those states may be unreachable. The following algorithm avoids this upfront construction and has two steps. Line 240 ⟶ 241: * Δ = {(q,q')\| q,q' ∈ Nodes and q ∈ Incoming(q') } * ''Q''<sub>0</sub> = { q ∈ Nodes \| init ∈ ''Incoming''(q) } * For each sub-formula g = fg<sub>1</sub> '''U''' fg<sub>2</sub>, let F<sub>g</sub> = { q ∈ Nodes \| fg<sub>2</sub> ∈ ''Now''(q) or g ∉ ''Now''(q) }, then '''F''' = { F<sub>g</sub> \| g ∈ ''cl''( f ) } Note that node labels in the algorithmic construction does not not contain negation of sub-formulas of f. In the declarative construction a node has the set of formulas that are expected to be true. The algorithmic construction ensures the correctness without the need of all the true formulas to be present in a node label.

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