“Fair computational tree logic”的意思、由来-开放百科全书

词条

Fair computational tree logic

释义

Weak fairness / justice
Strong fairness / compassion
Model checking for fair CTL
SCC-based approach
Emerson Lei algorithm
References

Fair computational tree logic is conventional computational tree logic studied with explicit fairness constraints.

Weak fairness / justice

This declares conditions such as all processes are executing infinitely often. If you consider the processes to be P_i, then the condition becomes:

Strong fairness / compassion

Here, if a process is requesting a resource infinitely often (R), it should be allowed to get the resource (C) infinitely often:

Model checking for fair CTL

If you consider a Kripke Model, the fair Kripke Model has a set of States F. A path is considered a fair path, if and

only if the path includes all members of F infinitely often.

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

1. M_f,s_i |= A if and only if holds in ALL fair paths.

2. M_f,s_i |= E if and only if holds in one or more fair paths.

A fair state is one from which at least one fair path originates. This translates to M_f,s |= EGtrue.

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 at least one node for each of the fair conditions.

To check for fair EG for any formula,

Compute what is called the denotation of the formula. Basically all the states such that M, s |= formula.
restrict the model to the denotation.
Find the fair SCC.
Obtain the union of all 3(above).
Compute the states that can reach the union.

Emerson Lei algorithm

The fix point characterization of Exist Globally is given by: [EGφ] = νZ .([φ] ∩ [EXZ ]), which is basically the limit applied according to Kleene's theorem. To fair paths, it becomes [Ef Gφ] = ν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 |author1=Emerson, E. A. |author2=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 |author1=Clarke, E. M. |author2=Emerson, E. A. |author3= Sistla, A. P. |last-author-amp=yes | 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}}

1 : Temporal logic

随便看

开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。