Model checking a mobile telephone system

In this paper we present a logic verification environment for mobile system specified by p-calculus terms. Properties of mobile system espressed by using an action-based temporal logic. Exploting a feature of the environment, we can generate finite state automata for a wide class of p-calculus agents, by preserving a notion of bisimulation equivalence. Hence, the formulae can be verified by applying a classical model check-in approach. In particular, we present as casa study, the verification of some propeties of a GSM protocol for mobile telephones, specified using a p-calculus.