Simulation preorder
Encyclopedia
In theoretical computer science
a simulation preorder is a relation
between state transition system
s associating systems which behave in the same way in the sense that one system simulates the other.
Intuitively, a system simulates another system if it can match all of its moves.
The basic definition relates states within one transition system, but this is easily adapted to relate two separate transition systems by building a system consisting of the disjoint union of the corresponding components.
(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 if p simulates q and q simulates p. Similarity is an equivalence relation
, but it is coarser than bisimilarity.
operator between sets.
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
a simulation preorder is a relation
Relation (mathematics)
In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple...
between state transition system
State transition system
In theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition...
s associating systems which behave in the same way in the sense that one system simulates the other.
Intuitively, a system simulates another system if it can match all of its moves.
The basic definition relates states within one transition system, but this is easily adapted to relate two separate transition systems by building a system consisting of the disjoint union of the corresponding components.
Formal definition
Given a labelled state transition systemState transition system
In theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition...
(S, Λ, →), a simulation relation is a binary relation
Binary relation
In mathematics, a binary relation on a set A is a collection of ordered pairs of elements of A. In other words, it is a subset of the Cartesian product A2 = . More generally, a binary relation between two sets A and B is a subset of...
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
Preorder
In mathematics, especially in order theory, preorders are binary relations that are reflexive and transitive.For example, all partial orders and equivalence relations are preorders...
, 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 if p simulates q and q simulates p. Similarity is an equivalence relation
Equivalence relation
In mathematics, an equivalence relation is a relation that, loosely speaking, partitions a set so that every element of the set is a member of one and only one cell of the partition. Two elements of the set are considered equivalent if and only if they are elements of the same cell...
, but it is coarser than bisimilarity.
Similarity of separate transition systems
When comparing two different transition systems (S', Λ', →') and (S' ', Λ' ', →' '), the basic notions of simulation and similarity can be used by forming the disjoint composition of the two machines, (S, Λ, →) with S = S' ∐ S' ', Λ = Λ' ∪ Λ' ' and → = →' ∪ →' ', where ∐ is the disjoint unionDisjoint union
In mathematics, the term disjoint union may refer to one of two different concepts:* In set theory, a disjoint union is a modified union operation that indexes the elements according to which set they originated in; disjoint sets have no element in common.* In probability theory , a disjoint union...
operator between sets.
See also
- State transition systemState transition systemIn theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition...
s - BisimulationBisimulationIn theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
- CoinductionCoinductionIn computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects.Coinduction is the mathematical dual to structural induction...
- Operational semanticsOperational semanticsIn computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...