Fair Computational tree logic

Fair Computational tree logic

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 Pi, then the condition becomes: igwedge GFP_{i}

trong fairness / compassion

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

Model checking for fair CTL

If you consider a Kripke Model, the fair Kripke Model has a set of States F. A path pi = so, s1 dots 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. Mf,si |= Aphi if and only if phi holds in ALL fair paths. 2. Mf,si |= Ephi if and only if phi holds in one ore more fair paths.

A fair state is one from which at least one fair path originates. The is translatable to, Mf,s |= EGtrue

CC-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

*
*


Wikimedia Foundation. 2010.

Игры ⚽ Нужна курсовая?

Look at other dictionaries:

  • Computational tree logic — Computation tree logic (CTL) is a branching time logic, meaning that its model of time is a tree like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is… …   Wikipedia

  • Computation tree logic — Computation tree logic (CTL) is a branching time logic, meaning that its model of time is a tree like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is… …   Wikipedia

  • Red-black tree — A red black tree is a type of self balancing binary search tree, a data structure used in computer science, typically used to implement associative arrays. The original structure was invented in 1972 by Rudolf Bayer who called them symmetric… …   Wikipedia

  • List of mathematics articles (C) — NOTOC C C closed subgroup C minimal theory C normal subgroup C number C semiring C space C symmetry C* algebra C0 semigroup CA group Cabal (set theory) Cabibbo Kobayashi Maskawa matrix Cabinet projection Cable knot Cabri Geometry Cabtaxi number… …   Wikipedia

  • Unbounded nondeterminism — In computer science, unbounded nondeterminism or unbounded indeterminacy is a property of concurrency by which the amount of delay in servicing a request can become unbounded as a result of arbitration of contention for shared resources while… …   Wikipedia

  • Discrete mathematics — For the mathematics journal, see Discrete Mathematics (journal). Graphs like this are among the objects studied by discrete mathematics, for their interesting mathematical properties, their usefulness as models of real world problems, and their… …   Wikipedia

  • linguistics — /ling gwis tiks/, n. (used with a sing. v.) the science of language, including phonetics, phonology, morphology, syntax, semantics, pragmatics, and historical linguistics. [1850 55; see LINGUISTIC, ICS] * * * Study of the nature and structure of… …   Universalium

  • computer — computerlike, adj. /keuhm pyooh teuhr/, n. 1. Also called processor. an electronic device designed to accept data, perform prescribed mathematical and logical operations at high speed, and display the results of these operations. Cf. analog… …   Universalium

  • education — /ej oo kay sheuhn/, n. 1. the act or process of imparting or acquiring general knowledge, developing the powers of reasoning and judgment, and generally of preparing oneself or others intellectually for mature life. 2. the act or process of… …   Universalium

  • Prolog — infobox programming language paradigm = Logic programming year = 1972 designer = Alain Colmerauer implementations = BProlog, ECLiPSe, Ciao Prolog, GNU Prolog, Quintus, SICStus, Strawberry, SWI Prolog, YAP Prolog, tuProlog dialects = ISO Prolog,… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”