Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Bisimulation
Summary
In theoretical computer science a bisimulation is a binary relation 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.
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 ,
such that both and its converse are simulations. 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; 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; therefore, the largest bisimulation must be reflexive, symmetric, and transitive. From this follows that the largest bisimulation — bisimilarity — is an equivalence relation.
Bisimulation can be defined in terms of composition of relations as follows.
Given a labelled state transition system , a bisimulation relation is a binary relation 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 of relations), and a simple algebraic calculation shows that the relation of bisimilarity—the join of all bisimulations—is an equivalence relation.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Related publications (2)
Deciding Conditional Termination
We address the problem of conditional termination, which is that of defining the set of initial configurations from which a given program always terminates. First we define the dual set, of initial configurations from which a non-terminating execution exis ...
Tech Univ Braunschweig2014Efficient static analysis of XML paths and types
We present an algorithm to solve XPath decision problems under regular tree type constraints and show its use to statically type-check XPath queries. To this end, we prove the decidability of a logic with converse for finite ordered trees whose time comple ...
2007Related concepts (2)
Transition system
In theoretical computer science, a transition system is a concept used in the study of computation. It is used to describe the potential behavior of discrete systems. It consists 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. If the label set is a singleton, the system is essentially unlabeled, and a simpler definition that omits the labels is possible.
Coinduction
In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects. Coinduction is the mathematical to structural induction. Coinductively defined types are known as codata and are typically infinite data structures, such as streams. As a definition or specification, coinduction describes how an object may be "observed", "broken down" or "destructed" into simpler objects. As a proof technique, it may be used to show that an equation is satisfied by all possible implementations of such a specification.