Simulation Preorder - Formal Definition

Formal Definition

Given a labelled state transition system (S, Λ, →), a simulation relation is a binary relation R over S (i.e. R ⊆ S × S) such that for every pair of elements p, q ∈ S, if (p,q)∈ R then for all α ∈ Λ, and for all p' ∈ S,

implies that there is a q' ∈ S such that

and (p',q') ∈ R.

Equivalently, in terms of relational composition:

Given two states p and q in S, q simulates p, written p ≤ q if there is a simulation R such that (p, q) ∈ R. The relation ≤ is a preorder, and is usually called the simulation preorder. It is the largest simulation relation over a given transition system.

Two states p and q are said to be similar, written p ≤≥ q, if p simulates q and q simulates p. Similarity is an equivalence relation, but it is coarser than bisimilarity.

Read more about this topic:  Simulation Preorder

Famous quotes containing the words formal and/or definition:

    The spiritual kinship between Lincoln and Whitman was founded upon their Americanism, their essential Westernism. Whitman had grown up without much formal education; Lincoln had scarcely any education. One had become the notable poet of the day; one the orator of the Gettsyburg Address. It was inevitable that Whitman as a poet should turn with a feeling of kinship to Lincoln, and even without any association or contact feel that Lincoln was his.
    Edgar Lee Masters (1869–1950)

    Was man made stupid to see his own stupidity?
    Is God by definition indifferent, beyond us all?
    Is the eternal truth man’s fighting soul
    Wherein the Beast ravens in its own avidity?
    Richard Eberhart (b. 1904)