Behavioural Equivalences over Reconfigurable Systems
摘要
We introduced and studied previously a process calculus that uses timeouts to describe the migration and communication taking place in distributed real-time systems. This calculus allows spatial reconfiguration regarding the mobility of agents, and reconfiguration of connectivity through communication of channel names. In this paper, we go further and study various behaviours of these distributed real-time systems, aiming to identify the most appropriate one (closer to a desired behaviour). For this, we describe an example consisting of a driver moving between locations, and define some behavioural equivalences involving multisets of actions, communicated resources and migration between locations.