A theory of may testing for actors

Abstract

The Actor model and π-calculus have served as the basis of a large body of research on concurrency. We represent the Actor model as a typed asynchronous π-calculus, called Aπ. The type system imposes a certain discipline on the use of names to capture actor properties such as uniqueness and persistence. We investigate the notion of may testing in Aπ and give a trace based characterization of it. Such a characterization simplifies reasoning about actor configurations as it does not involve quantification over all environments. We compare our characterization with that of asynchronous π-calculus, and highlight the differences that arise due to actor properties.