Input/Output (I/O) automata and the Temporal Logic of Actions (TLA) are two well-known techniques for the specification and verification of concurrent systems. Over the past few years, they have been extended to the so-called dynamic I/O automata and, respectively, Mobile TLA (MTLA) in order to be more appropriate for mobile agent systems. Dynamic I/O automata is just a mathematical model, whereas MTLA is a logic with a formally defined language. In this paper, therefore, we investigate how MTLA could be used as a formal language for the specification of dynamic I/O automata. We do this by writing an MTLA specification of a travel agent system which has been specified semi-formally in the literature on that model. In this specification, we deal with always existing agents as well as with an initially unknown number of dynamically created agents, with mobile and non-mobile agents, with I/O-automata-style communication, and with the changing communication capabilities of mobile agents. We have previously written a TLA specification of this system. This paper shows that an MTLA specification of such a system can be more elegant and faithful to the dynamic I/O automata definition because the agent existence and location can be expressed directly by using agent and location names instead of special variables as in TLA. It also shows how the reuse of names for dynamically created and destroyed agents within the dynamic I/O automata framework can be specified in MTLA.

This paper considers systems consisting of communicating processes which can move between specified locations. Mobile telephone systems and intelligent transport systems are examples of them. The processes can exchange data as well as channels (e.g. frequencies) to be used in further communication. It may happen that two processes (e.g. telephones or cars) in different locations could communicate directly because they share a communication channel, but they cannot as there is a physical obstacle between the locations. A possible solution is to allow one process to send a message to another one through other processes and locations. To see if this is possible, a notion of connectivity of processes has been devised in the literature. A process was defined to be connectable to another one if a message from the first one could reach the other one by using any existing communication actions, allowed locations, and process moves in the system. A process-algebraic approach for checking connectivity was proposed. In this paper, it is shown how the temporal logic of actions (TLA) can be employed for the same purpose. In both approaches, connectivity of a process with another one is basically checked as follows. The first process includes a marking message in all its sending actions. Every process that receives this message gets marked and includes it in its own sending actions. The first process is connectable to the second one if there exists such a system execution sequence that the latter gets marked in it. Since TLA is a linear-time temporal logic, it can generally not express such a property. This paper, however, shows that it can be expressed and verified for a given TLA system specification. It also shows how to specify the marking operations and provides an example of connectivity checking.