A spatial equational logic for the applied π-calculus |
| |
Authors: | Étienne Lozes Jules Villard |
| |
Affiliation: | 1. LSV, ENS Cachan, CNRS – 61 av. du pdt Wilson, 94230, Cachan, France
|
| |
Abstract: | Spatial logics have been proposed to reason locally and modularly on algebraic models of distributed systems. In this paper
we define the spatial equational logic A
π
L whose models are processes of the applied π-calculus. This extension of the π-calculus allows term manipulation and records communications as aliases in a frame, thus augmenting the predefined underlying
equational theory. Our logic allows one to reason locally either on frames or on processes, thanks to static and dynamic spatial
operators. We study the logical equivalences induced by various relevant fragments of A
π
L, and show in particular that the whole logic induces a coarser equivalence than structural congruence. We give characteristic
formulae for some of these equivalences and for static equivalence. Going further into the exploration of A
π
L’s expressivity, we also show that it can eliminate standard term quantification. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|