Revision as of 07:26, 14 February 2014 edit Ashutosh y0078 (talk \| contribs) 2,179 edits →Gerth et al. algorithm ← Previous edit		Revision as of 07:29, 14 February 2014 edit undo Ashutosh y0078 (talk \| contribs) 2,179 edits →Gerth et al. algorithm Next edit →
Line 114: ===Gerth et al. algorithm=== The following algorithm is due to Gerth, Peled, [[Moshe Y. Vardi\|Vardi]], and Wolper.<ref name=GPVW93/> The ~~above~~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. In ~~step~~the ~~one~~first step, it incrementally constructs a directed graph. In ~~step~~the ~~two~~second step, it builds a [[labeled generalized Büchi automaton]] (LGBA) by defining nodes of the graph as states and directed edges as transitions. This algorithm takes reachability into account and may produce a smaller automaton but the worst-case complexity remains the same.

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