Bisimulation through probabilistic testing

We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm can distinguish, with a probability arbitrarily close to one, between processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2 3 -bisimulation —which lies strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify a new process relation called probabilistic bisimulation—which is strictly stronger than bisimulation.

Authors

• Kim G. Larsen
• Arne Skou

Keywords

No keywords are indexed for this paper.