In [19] it was observed that a theory like the π-calculus, dependent on a theory of names, can be closed, through a mechanism of quoting, so that (quoted) processes provide the necessary notion of names. Here we expand on this theme by examining a construction for a Hennessy-Milner logic corresponding to an asynchronous message-passing calculus built on a notion of quoting. Like standard Hennessy-Milner logics, the logic exhibits formulae corresponding to sets of processes, but a new class of formulae, corresponding to sets of names, also emerges. This feature provides for a number of interesting possible applications from security to data manipulation. Specifically, we illustrate formulae for controlling process response on ranges of names reminiscent of a (static) constraint on port access in a firewall configuration. Likewise, we exhibit formulae in a names-as-data paradigm corresponding to validation for fragment of XML Schema. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Meredith, L. G., & Radestock, M. (2005). Namespace logic: A logic for a reflective higher-order calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3705 LNCS, pp. 353–369). https://doi.org/10.1007/11580850_19
Mendeley helps you to discover research relevant for your work.