theoretical computer science Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory. It is difficult to circumsc ...

, a stutter bisimulation''

Principles of Model Checking ''Principles of Model Checking'' is a textbook on model checking, an area of computer science that automates the problem of determining if a machine meets specification requirements. It was written by Christel Baier and Joost-Pieter Katoen, and ...

'', by

Christel Baier Christel Baier (born 26 September 1965) is a German theoretical computer scientist known for her work in model checking, temporal logic, and automata theory. She is a professor at TU Dresden, where she holds the chair for Algebraic and Logic Fou ...

and

Joost-Pieter Katoen Joost-Pieter Katoen (born October 6, 1964) is a Dutch theoretical computer scientist based in Germany. He is distinguished professor in Computer Science and head of the Software Modeling and Verification Group at RWTH Aachen University. Furthermor ...

, The MIT Press, Cambridge, Massachusetts. is defined in a

coinductive In 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. Coinductively defined types are known as codata and ...

manner, as is ''

bisimulation 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 ...

''.
Let TS=(S,Act,→,I,AP,L) be a

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 wi ...

. A stutter bisimulation for TS is
a

binary relation In mathematics, a binary relation associates elements of one set, called the ''domain'', with elements of another set, called the ''codomain''. A binary relation over Set (mathematics), sets and is a new set of ordered pairs consisting of ele ...

R on S such that for all (s₁,s₂) which is in R:
# L(s₁) = L(s₂). # If s₁^' is in Post(s₁) with (s₁^',s₂) is not in R,
then there exists a finite path fragment s₂u₁…u_ns₂^' with n≥0 and
(s₁,u_i) is in R, and (s₁^',s₂^') is in R. # If s₂^' is in Post(s₂) with (s₁,s₂^') is not in R,
then there exists a finite path fragment s₁v₁…v_ns₁^' with n≥0 and
(v_i,s₂) is in R, and (s₁^',s₂^') is in R.

References

{{reflist Transition systems