On CSP Refinement Tests That Run Multiple Copies of a Process
Gavin Lowe · Electronic Notes in Theoretical Computer Science · 2009
In this paper we consider CSP stable failures refinement checks, where the right hand side of the refinement contains n copies of a process P. We show that such refinement checks capture precisely those predicates of the form ∀f1,…,fn∈failures(P)⋅R(f1,…,fn) for some n-ary relation R. The construction of the refinement test is, in general, infinitary; however, we show how, given R, one can often calculate a finite state refinement check.