Fair computational tree logic: Difference between revisions

Revision as of 06:34, 29 January 2007

Latest revision as of 06:51, 15 August 2023

(29 intermediate revisions by 22 users not shown)

Line 1:

{{No footnotes|date=April 2023}}

'''Fair Computationalcomputational tree logic''' is conventional [http://en.wikipedia.org/wiki/Computational_tree_logic Computational[computational tree logic]] studied with explicit fairness constraints.

==Weak fairness / Justicejustice==

This declares conditions such as all processes areexecute executing infiniteinfinitely often. If you consider the processes to be P_i, then the condition becomes <br /><math>\bigwedge GFP_{i}</math> :

:<math>\bigwedge( GFR \longrightarrow GFC)GFP_{i}</math>

==Strong fairness / Compassion==

Here, if a process is requesting a resource infinitely often (T), it should be allowed to get the resource (C)infinitely often <br />

<math>\bigwedge( GFR \longrightarrow GFC)</math>

==Strong fairness / Compassioncompassion==

Here, if a process is requesting a resource infinitely often (TR), it should be allowed to get the resource (C) infinitely often <br />:

:<math>\bigwedge( GFR \longrightarrow GFC)</math>

==Model checking for fair CTL==

If you considerConsider a [[Kripke Model,model]] the fair Kripke Model has awith set of Statesstates ''F''. A path <math>\pi = sos_o, s1s_1 \dots</math> is considered a '''fair path''', if and

only if the path includes all members of ''F'' infinitely often. <br/>

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

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

2:1. M_f, s_i |= EA<math>\phi</math> if and only if <math>\phi</math> holds in one ore more''all'' fair paths. <br/>

1: 2. M_f, s_i |= AE<math>\phi</math> if and only if <math>\phi</math> holds in ALL''one or more'' fair paths. <br/>

A '''fair state''' is one from which atleastat least one fair path originates. TheThis is translatabletranslates to, M_f, s |= EGtrue <br />.

==SCC -based approach==

A [http://en.wikipedia.org/wiki/Strongly_connected_component Strongly[strongly connected component]] (SCC) of a directed graph is a maximallymaximal strongly connected graph - allsubgraph—all the nodes are reachable from each other. A fair SCC is one that has an edge into atleastat least one node for each of the fair conditions.

<br /><br />

To check for fair EG for any formula - <br/>

1. Compute what is called the denotation of the formula. Basically all the states such that M, s |= formula. <br />

2. restrict the Model to the denotation. <br />

3. Find the fair SCC <br />

4. Obtain the union of all 3(above). <br />

5. Compute the states that can reach the union. <br/>

To check for fair EG for any formula - <br/>,

1.# Compute what is called the ''denotation'' of the formula. Basically all''&phi;'': the set of states such that M, s |= formula''&phi;''. <br />

==Emersion Lei Algorithm==

2.# restrictRestrict the Modelmodel to the denotation. <br />

The fix point characterization of Exist Globally is given by:- <br/>

3.# Find the fair SCC <br />.

[EGφ] = νZ .([φ] ∩ [EXZ ]) , which is basically the limit applied according to Kleene's theorem. <br/>

4.# Obtain the union of all 3 (above). <br />

To fair paths, it becomes - <br/>

5.# Compute the states that can reach the union. <br/>

[Ef Gφ] = νZ .([φ] ∩_{Fi ∈FT} [EX[E(Z U(Z ∧ Fi ))])<br/>

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.

==Emerson Lei algorithm==

The fix point characterization of Exist Globally is given by: [EGφ] = &nu;Z .([φ] ∩ [EXZ ]), which is basically the limit applied according to [[Kleene's theorem]]. To fair paths, it becomes [Ef Gφ] = &nu;Z .([φ] ∩_{Fi ∈FT} [EX[E(Z U(Z ∧ Fi ))]), 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 | authorauthor1=Emerson, E. A. and |author2=Halpern, J. Y. |author2link = Joseph Halpern| 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=11–24 | doi=10.1016/0022-240000(85)90001-7| doi-access=free}}

* {{cite journal | authorauthor1=Clarke, E. M., |author1link = Edmund M. Clarke|author2=Emerson, E. A., and|author3= Sistla, A. P. |name-list-style=amp | 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=244244–263 | doi=10.1145/5397.5399| s2cid=52853200 | doi-263access=free }}

[[Category:Temporal logic]]

* {{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}}

{{Uncategorized|January 2007}}