Please use this identifier to cite or link to this item:
|Title:||Model Checking for Nominal Calculi|
|Authors:||Ferrari, Gian Luigi|
|Citation:||Foundations of Software Science and Computational Structures 8th International Conference, FOSSACS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings. Lecture Notes in Computer Science, 2005, 3441, pp. 1-24|
|Abstract:||Nominal calculi have been shown very effective to formally model a variety of computational phenomena. The models of nominal calculi have often infinite states, thus making model checking a difficult task. In this note we survey some of the approaches for model checking nominal calculi. Then, we focus on History-Dependent automata, a syntax-free automaton-based model of mobility. History-Dependent automata have provided the formal basis to design and implement some existing verification toolkits. We then introduce a novel syntax-free setting to model the symbolic semantics of a nominal calculus. Our approach relies on the notions of reactive systems and observed borrowed contexts introduced by Leifer and Milner, and further developed by Sassone, Lack and Sobocinski. We argue that the symbolic semantics model based on borrowed contexts can be conveniently applied to web service discovery and binding.|
|Appears in Collections:||Conference Papers & Presentations, Dept. of Computer Science|
Files in This Item:
There are no files associated with this item.
Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.