Bisimulation and effectiveness (Q1118393)

The author shows that the quotient of an algorithmic transition system by its greatest bisimulation equivalence is usually not algorithmic (reducibility to the halting problem). For the relevance of the notion of bisimulation see \textit{R. Milner}, Communication and concurrency, Prentice Hall International Series in Computer Science, New York, London, Toronto, Sydney, Tokyo (1989).