ETD

Archivio digitale delle tesi discusse presso l'Università di Pisa

Tesi etd-03262004-144607


Tipo di tesi
Tesi di laurea specialistica
Autore
Ciancia, Vincenzo
Indirizzo email
ciancia@di.unipi.it
URN
etd-03262004-144607
Titolo
A temporal logic for HD-automata
Dipartimento
SCIENZE MATEMATICHE, FISICHE E NATURALI
Corso di studi
INFORMATICA
Relatori
relatore Prof. Montanari, Ugo
Parole chiave
  • model checking
  • HD-automata
  • mobility
  • concurrency
  • pi-calculus
  • temporal
  • modal
  • logic
Data inizio appello
23/04/2004
Consultabilità
Completa
Riassunto
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.
File