Determining asynchronous test equivalence for probabilistic processes

Abstract

Each probabilistic process exhibits a kind of input-output behaviour when subjected to asynchronous testing. This behaviour is called the asynchronous test behaviour of the process. When the system under test is comprised of multiple probabilistic processes, the asynchronous test behaviour of the system is equal to the union of the asynchronous test behaviours of the constituent processes. In this paper, we first formalize the notion of asynchronous test behaviour of a process, and then address the following decision problem: Given a system comprising multiple processes, and a reference process, determine whether the two are equivalent in terms of their asynchronous test behaviour or not. We prove this problem to be undecidable.