Towards a proof-theoretic foundation for actor specification and verification

Actors has been regarded as a promising model for open distributed systems. Although the operational semantics of actor programs has already been studied in some recent work, means of reasoning about the behaviour of communities of interconnected actors at a high abstraction level are still lacking. In this paper we argue that a proof-theoretic semantics would be better suited to this purpose. We present an abstract data type like axiomatisation of the kernel primitives of Actors, showing how to reason from specifications of actor communities and how to compose them within the framework of temporal logics of objects.