Actors -- A Process Algebra Based Approach

TL;DR

This paper models the actor system using truly concurrent process algebra, capturing key characteristics like concurrency, asynchrony, and persistence, providing a rigorous semantic foundation and proof capabilities for actor-based systems.

Contribution

It introduces a process algebra framework that accurately models actor characteristics and offers advantages over previous models in expressiveness and formal verification.

Findings

Rich expressive ability to model actor features

True concurrency models with solid semantics

Facilitates formal correctness proofs

Abstract

We model actors based on truly concurrent process algebra, and capture the actor model in the following characteristics: (1) Concurrency: all actors execute concurrently; (2) Asynchrony: an actor receives and sends messages asynchronously; (3) Uniqueness: an actor has a unique name and the associate unique mail box name; (4) Concentration: an actor focuses on the processing messages, including some local computations, creations of some new actors, and sending some messages to other actors; (5) Communication Dependency: the only way of affecting an actor is sending a message to it; (6) Abstraction: except for the receiving and sending message, and creating new actors, the local computations are abstracted; (7) Persistence: an actor does not disappear after processing a message. Truly concurrent process algebra has rich expressive ability to model the above characteristics of actors, and more importantly, they are models for true concurrency, Comparing with other models of actors, the truly concurrent process algebra based model has the following advantages: (1) The truly concurrent process algebra has rich expressive abilities to describe almost all characteristics of actors, especially for asynchronous communication, actor creation, recursion, abstraction, etc; (2) The truly concurrent process algebra and actors are all models for true concurrency, and have inborn intimacy; (3) The truly concurrent process algebra has a firm semantics foundation and a powerful proof theory, the correctness of an actor system can be proven easily.