Brand and Zafiropulo's notion of Communicating Finite-State Machines (CFSMs) provides a succinct and powerful model of message-passing concurrency, based around channels. However, a major variant of message-passing concurrency is not readily captured by CFSMs: the actor model. In this work, we define a variant of CFSMs, called Communicating Actor Automata, to capture the actor model of concurrency as provided by Erlang: with mailboxes, from which messages are received according to repeated application of pattern matching. Furthermore, this variant of CFSMs supports dynamic process topologies, capturing common programming idioms in the context of actor-based message-passing concurrency. This gives a new basis for modelling, specifying, and verifying Erlang programs. We also consider a class of CAAs that give rise to freedom from race conditions.

翻译：Brand和Zafiropulo提出的通信有限状态机概念提供了基于通道的简洁而强大的消息传递并发模型。然而，消息传递并发的一个重要变体——Actor模型——却难以被通信有限状态机直接刻画。本研究定义了一种通信有限状态机的变体，称为通信Actor自动机，用以捕捉Erlang语言所提供的Actor并发模型：通过邮箱机制，消息依据模式匹配的重复应用进行接收。此外，该通信有限状态机变体支持动态进程拓扑，能够刻画基于Actor的消息传递并发中的常见编程惯用法，从而为Erlang程序的建模、规约与验证提供了新的基础。本文还考虑了一类能避免竞态条件的通信Actor自动机。