Model Checking for Nominal Calculi

12 years 11 months ago
Model Checking for Nominal Calculi
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. 1 Summary Model checking has been shown very effective for proving properties of sys...
Gian Luigi Ferrari, Ugo Montanari, Emilio Tuosto
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Authors Gian Luigi Ferrari, Ugo Montanari, Emilio Tuosto
Comments (0)