Decidability Problems for Actor Systems

TL;DR

This paper explores the computational power of actor systems, showing how features like fields influence decidability and Turing completeness, with results on when properties like termination are decidable.

Contribution

It introduces a nominal actor language and characterizes the impact of fields and states on system decidability and expressiveness.

Findings

Presence of fields leads to Turing completeness.

Stateless actors have decidable properties like termination.

Bounded and read-only states preserve decidability.

Abstract

We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a crucial feature: the dynamic creation of names in combination with fields gives rise to Turing completeness. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination are decidable. This decidability result still holds for actors with states when the number of actors is bounded and the state is read-only.