Testing Equivalence for Mobile Processes

The impact of applying the testing approach to a calculus of processes with dynamic communication topology is investigated. A proof system is introduced that consists of two groups of laws: those for strong observational equivalence and those needed to deal with invisible actions. Soundness and completeness of this proof system w. r. t. a testing preorder are shown. A fully abstract denotational model for the language is presented that takes advantage of reductions of processes to normal forms.

Authors

• M. Boreale
• R. Denicola

Keywords

No keywords are indexed for this paper.