Type-based spatial logic for concurrent processes.
Antonio Ravara
Abstract
We aim at the development of a general notion of type based on spatial
logic for concurrent processes, expressive enough to capture
properties of the kind already ensured by behavioral typing systems,
but also able to establish more ``intensional'' spatial / structural
properties. In fact, many interesting properties of distributed
systems are inherently spatial, for instance connectivity, stating
that there is always an access route between two different sites,
unique handling, stating that there is at most one server process
listening on a given channel name, or resource availability, stating
that a bound exists on the number of channels that can be allocated at
a given location. The challenge is the design a type system (and thus
a decidable proof system) able to assign an interesting class of
spatial / behavioral types to an interesting class of processes.