Fair computational tree logic: Difference between revisions

Revision as of 09:39, 9 May 2009

Revision as of 08:37, 13 August 2009

Line 13:

Fair CTL model checking restricts the checks to only fair paths. There are two kinds: <br/>

1. M_f,s_i |= A<math>\phi</math> if and only if <math>\phi</math> holds in ALL fair paths. <br/>

2. M_f,s_i |= 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 at least one fair path originates. The is translatable to, M_f,s |= EGtrue <br />

==SCC-based approach==

Line 28:

==Emerson Lei algorithm==

The fix point characterization of Exist Globally is given by: <math>[EGφ] = νZ .([φ] ∩ [EXZ ])</math> , which is basically the limit applied according to Kleene's theorem. To fair paths, it becomes <math>[Ef Gφ] = νZ .([φ] ∩_{Fi ∈FT} [EX[E(Z U(Z ∧ Fi ))])</math> which means the formula holds in the current state and the next states and the next to next states until it meets all the members of the fair conditions. This means that, the condition is equivalent to a sort of accepting point where the accepting condition is the entire set of Fair conditions.

==References==

* {{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 | doi=10.1016/0022-0000(85)90001-7}}

* {{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 | doi=10.1145/5397.5399}}

[[Category:Logic in computer science]]

[[Category:Modal logic]]