PERTIMO: A Model of Spatial Migration with Safe Access Permissions

We introduce a process algebra with processes able to migrate between different explicit locations of a distributed environment defined by a number of distinct locations. We use timing constraints over local clocks to control migration and communication, together with local maximal concurrency in the way actions are executed. Two processes may communicate if they are present at the same location and, in addition, they have appropriate access permissions to communicate over a shared channel. Access permissions can be acquired or lost while moving from one location to another. Timing constraints coordinate and control both communication between processes and migration between locations. We completely characterize the situations in which a process is guaranteed to possess safe access permissions in all possible environments. In this way, one can design systems in which processes are not blocked (deadlocked) due to the lack of dynamically changing access permissions.