Equivalences on Observable Processes

The aim of this paper is to find the finest `observable' and `implementable' equivalence on concurrent processes. This is a part of a larger programme to develop a theory of observable processes where semantics of processes are based on locally and finitely observable process behaviour, and all process constructs are allowed, provided their operational meaning is defined by realistically implementable transition rules. Process behaviour which can be established by so-called local testing but not global testing is called locally and finitely observable. We define copy+refusal testing equivalence as indistinguishability by copy+refusal tests consisting of traces, refusals and copying, all of which are local. It is argued that copy+refusal tests are sufficient for local testing-adding any other local tests to copy+refusal tests does not increase their testing power. Hence, copy+refusal equivalence is the finest observable equivalence. By examining the structure of transition ru...

• Type: Conference
• Year: 1992
• Where: LICS
• Authors: Irek Ulidowski
• Keywords: Automated Reasoning, Copy+refusal Equivalence, Copy+refusal Tests, Finest Observable Equivalence, LICS 1992