In
theoretical computer science
Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation.
It is difficult to circumscribe the theoretical areas precisely. The Associati ...
a bisimulation is a
binary relation
In mathematics, a binary relation associates some elements of one Set (mathematics), set called the ''domain'' with some elements of another set called the ''codomain''. Precisely, a binary relation over sets X and Y is a set of ordered pairs ...
between state
transition systems, associating systems that behave in the same way in that one system simulates the other and vice versa.
Intuitively two systems are bisimilar if they, assuming we view them as playing a ''game'' according to some rules, match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer.
Formal definition
Given a
labeled state transition system ,
where is a set of states,
is a set of labels and → is a set of labelled transitions (i.e., a subset of
),
a bisimulation is a
binary relation
In mathematics, a binary relation associates some elements of one Set (mathematics), set called the ''domain'' with some elements of another set called the ''codomain''. Precisely, a binary relation over sets X and Y is a set of ordered pairs ...
,
such that both and its
converse are
simulation
A simulation is an imitative representation of a process or system that could exist in the real world. In this broad sense, simulation can often be used interchangeably with model. Sometimes a clear distinction between the two terms is made, in ...
s. From this follows that the
symmetric closure of a bisimulation is a bisimulation, and that each symmetric simulation is a bisimulation. Thus some authors define bisimulation as a symmetric simulation.
Equivalently, is a bisimulation if and only if for every pair of states
in and all labels ''λ'' in
:
* if
, then there is
such that
;
* if
, then there is
such that
.
Given two states and in , is bisimilar to , written
, if and only if there is a bisimulation such that
. This means that the bisimilarity relation is the union of all bisimulations:
precisely when
for some bisimulation .
The set of bisimulations is closed under union;
[Meaning the union of two bisimulations is a bisimulation.] therefore, the bisimilarity relation is itself a bisimulation. Since it is the union of all bisimulations, it is the unique largest bisimulation. Bisimulations are also closed under reflexive, symmetric, and
transitive closure
In mathematics, the transitive closure of a homogeneous binary relation on a set (mathematics), set is the smallest Relation (mathematics), relation on that contains and is Transitive relation, transitive. For finite sets, "smallest" can be ...
; therefore, the largest bisimulation must be reflexive, symmetric, and transitive. From this follows that the largest bisimulation—bisimilarity—is an
equivalence relation.
Alternative definitions
Relational definition
Bisimulation can be defined in terms of
composition of relations
In the mathematics of binary relations, the composition of relations is the forming of a new binary relation from two given binary relations ''R'' and ''S''. In the calculus of relations, the composition of relations is called relative multiplica ...
as follows.
Given a
labelled state transition system , a ''bisimulation''
relation is a
binary relation
In mathematics, a binary relation associates some elements of one Set (mathematics), set called the ''domain'' with some elements of another set called the ''codomain''. Precisely, a binary relation over sets X and Y is a set of ordered pairs ...
over (i.e., ) such that
and
From the monotonicity and continuity of relation composition, it follows immediately that the set of bisimulations is closed under unions (
joins in the
poset
In mathematics, especially order theory, a partial order on a Set (mathematics), set is an arrangement such that, for certain pairs of elements, one precedes the other. The word ''partial'' is used to indicate that not every pair of elements need ...
of relations), and a simple algebraic calculation shows that the relation of bisimilarity—the join of all bisimulations—is an equivalence relation. This definition, and the associated treatment of bisimilarity, can be interpreted in any involutive
quantale.
Fixpoint definition
Bisimilarity can also be defined in
order-theoretical fashion, in terms of
fixpoint theory, more precisely as the greatest fixed point of a certain function defined below.
Given a
labelled state transition system (
, Λ, →), define
to be a function from binary relations over
to binary relations over
, as follows:
Let
be any binary relation over
.
is defined to be the set of all pairs
in
×
such that:
and
Bisimilarity is then defined to be the
greatest fixed point of
.
Ehrenfeucht–Fraïssé game definition
Bisimulation can also be thought of in terms of a game between two players: attacker and defender.
"Attacker" goes first and may choose any valid transition,
, from
. That is,
or
The "Defender" must then attempt to match that transition,
from either
or
depending on the attacker's move.
I.e., they must find an
such that:
or
Attacker and defender continue to take alternating turns until:
* The defender is unable to find any valid transitions to match the attacker's move. In this case the attacker wins.
* The game reaches states
that are both 'dead' (i.e., there are no transitions from either state) In this case the defender wins
* The game goes on forever, in which case the defender wins.
* The game reaches states
, which have already been visited. This is equivalent to an infinite play and counts as a win for the defender.
By the above definition the system is a bisimulation if and only if there exists a winning strategy for the defender.
Coalgebraic definition
A bisimulation for state transition systems is a special case of
coalgebraic bisimulation for the type of covariant powerset
functor
In mathematics, specifically category theory, a functor is a Map (mathematics), mapping between Category (mathematics), categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) ar ...
.
Note that every state transition system
can be mapped
bijectively to a function
from
to the
powerset
In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is po ...
of
indexed by
written as
, defined by
Let
be
-th
projection, mapping
to
and
respectively for
; and
the forward image of
defined by dropping the third component
where
is a subset of
. Similarly for
.
Using the above notations, a relation
is a bisimulation on a transition system
if and only if there exists a transition system
on the relation
such that the
diagram
A diagram is a symbolic Depiction, representation of information using Visualization (graphics), visualization techniques. Diagrams have been used since prehistoric times on Cave painting, walls of caves, but became more prevalent during the Age o ...
commutes, i.e. for
, the equations
hold
where
is the functional representation of
.
Variants of bisimulation
In special contexts the notion of bisimulation is sometimes refined by adding additional requirements or constraints. An example is that of
stutter bisimulation, in which one transition of one system may be matched with multiple transitions of the other, provided that the intermediate states are equivalent to the starting state ("stutters").
A different variant applies if the state transition system includes a notion of ''silent'' (or ''internal'') action, often denoted with
, i.e. actions that are not visible by external observers, then bisimulation can be relaxed to be ''weak bisimulation'', in which if two states
and
are bisimilar and there is some number of internal actions leading from
to some state
then there must exist state
such that there is some number (possibly zero) of internal actions leading from
to
. A relation
on processes is a weak bisimulation if the following holds (with
, and
being an observable and mute transition respectively):
This is closely related to the notion of bisimulation "
up to Two Mathematical object, mathematical objects and are called "equal up to an equivalence relation "
* if and are related by , that is,
* if holds, that is,
* if the equivalence classes of and with respect to are equal.
This figure of speech ...
" a relation.
Typically, if the
state transition system gives the
operational semantics
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its exec ...
of a
programming language
A programming language is a system of notation for writing computer programs.
Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
, then the precise definition of bisimulation will be specific to the restrictions of the programming language. Therefore, in general, there may be more than one kind of bisimulation (respectively bisimilarity) relationship depending on the context.
Bisimulation and modal logic
Since
Kripke models are a special case of (labelled) state transition systems, bisimulation is also a topic in
modal logic
Modal logic is a kind of logic used to represent statements about Modality (natural language), necessity and possibility. In philosophy and related fields
it is used as a tool for understanding concepts such as knowledge, obligation, and causality ...
. In fact, modal logic is the fragment of
first-order logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
invariant under bisimulation (
van Benthem's theorem).
Algorithm
Checking that two finite transition systems are bisimilar can be done in
polynomial time. The fastest algorithms are
quasilinear time using
partition refinement through a reduction to the coarsest
partition problem.
See also
*
Simulation preorder
*
Congruence relation
In abstract algebra, a congruence relation (or simply congruence) is an equivalence relation on an algebraic structure (such as a group (mathematics), group, ring (mathematics), ring, or vector space) that is compatible with the structure in the ...
*
Probabilistic bisimulation
Notes
References
Further reading
*
*
*
External links
Software tools
*
CADPtools to minimize and compare finite-state systems according to various bisimulations*
mCRL2: tools to minimize and compare finite-state systems according to various bisimulations
The Bisimulation Game Game
{{Authority control
Theoretical computer science
Formal methods
Logic in computer science
Transition systems