A spatial logic consists of four groups of operators: standard prepositional connectives; spatial operators; a temporal modality; calculus-specific operators. The calculus-specific operators talk about the capabilities of the processes of the calculus, that is, the process constructors through which a process can interact with its environment. We prove some minimality results for spatial logics. The main results show that in the logics for π-calculus and asynchronous π-calculus the calculus-specific operators can be eliminated. The results are presented under both the strong and the weak interpretations of the temporal modality. Our proof techniques are applicable to other spatial logics, so to eliminate some of - if not all - the calculus-specific operators. As an example of this, we consider the logic for the Ambient calculus, with the strong semantics.
展开▼
