TLA-style specification of a mobile network

In mobile communication networks, some nodes change location and must therefore be connected to different other nodes at different times in order to be able to communicate continuously. The mobility of nodes can elegantly be specified using the /spl pi/ calculus, an algebraic formalism that allows sending of channel names to be used for further communication as parameters in communication events. The paper shows how mobility can be specified in a temporal logic of actions using a state based approach. A simplified handover procedure for controlling the dynamic topology of a mobile telephone network is precisely specified as an illustration.