Process algebras represent mathematical formalisms for modeling distributed systems whose behavior may be subsequently analyzed by automatic tools that investigate all possible system executions.

This paper develops an executable semantics of the process algebra timed mobility (TiMo) that describes the timed behavior of mobile systems whose processes are subject to time constraints and may move from one location to another. The core idea is to describe the operational semantics of TiMo in rewriting logic (RL) where a system state is modeled by an algebraic term and state transitions are described by conditional rewriting rules. Subsequently, rewriting strategies may be applied to capture maximal concurrency, where independent transitions are performed simultaneously. The RL model is implemented in the term rewriting system Elan, which may thus simulate the execution of a system and answer whether it is it possible to reach a certain state in a given number of steps. The idea is subsequently generalized to the process algebra permissions, timers, and mobility (PerTiMo), which also models security aspects of a system by associating communication permissions with processes.

The core of the paper is the development of the RL models of TiMo and PerTiMo, and the proof of their soundness and completeness. Several examples demonstrate the usefulness of analyzing systems by executing their RL models in Elan; these examples make the results accessible to the more casual reader. Indeed, the approach shows great flexibility and extensibility and may be used for the rapid prototyping of many similar formalisms.