• concurrency
• HD-automata
• logic
• mobility
• modal
• model checking
• pi-calculus
• temporal

Due to the broad diffusion of every kind of network and mobile device in the last few years, computing is rapidly evolving towards what is now called "global computing". With this term we refer to a new field of research and development in computer science, with innovative features with respects to standard development processes and software architectures: computing is distributed and mobile, programs are heterogeneous, systems are open-ended, computational entities are autonomous. To completely meet these goals in software production, work is required from the theoretical point of view, both to develop new models of computation that satisfy the given requirements, and to learn how to reason about the behavior, and check properties, of such systems.

In this thesis, we will concentrate on a particular operational model called history dependent automata, an enriched version of labeled transition systems that can represent name generation and name passing, and is particularly adapt to model in a compact way finite state, concurrent mobile systems. We develop a temporal logic for pi calculus and HD-automata, provide proofs of adequacy, soundness and completeness, and describe the model checking algorithm. Case studies are provided which reveal the expressive power of the logic.