Revision as of 16:22, 22 March 2007 edit Resurgent insurgent (talk \| contribs) 5,999 edits add categories and clean up formatting ← Previous edit		Revision as of 17:44, 18 April 2007 edit undo Sintaku (talk \| contribs) Extended confirmed users, Rollbackers 12,039 edits Typo fixing, Typos fixed: atleast → at least (2), using AWB Next edit →
Line 14: 2. M<sub>f</sub>,s<sub>i</sub> \|= E<math>\phi</math> if and only if <math>\phi</math> holds in one ore more fair paths. <br/> A fair state is one from which ~~atleast~~at least one fair path originates. The is translatable to, M<sub>f</sub>,s \|= EGtrue <br /> ==SCC-based approach== The [[strongly connected component]] (SCC) of a directed graph is a maximally connected graph - all the nodes are reachable from each other. A fair SCC is one that has an edge into ~~atleast~~at least one node for each of the fair conditions. To check for fair EG for any formula, Line 32: * {{cite journal \| author=Emerson, E. A. and Halpern, J. Y. \| title=Decision procedures and expressiveness in the temporal logic of branching time \| journal=Journal of Computer and System Sciences\| year=1985\| volume=30 \| issue=1 \| pages=1-24}} * {{cite journal \| author=Clarke, E. M., Emerson, E. A., and Sistla, A. P. \| title=Automatic verification of finite-state concurrent systems using temporal logic specifications \| journal=ACM Transactions on Programming Languages and Systems\| year=1986\| volume=8 \| issue=2 \| pages=244-263}} [[Category:Logic in computer science]] [[Category:Modal logic]]

Fair computational tree logic: Difference between revisions