Abstract
We present a meta-logic that contains a new quantifier ∇ (for encoding "generic judgments") and inference rules for reasoning within fixed points of a given specification. We then specify the operational semantics and bisimulation relations for the finite π-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The ∇ quantifier helps with the delicate issues surrounding the scope of variables within π-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation.
| Original language | English |
|---|---|
| Pages (from-to) | 79-101 |
| Number of pages | 23 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 138 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - 9 Sept 2005 |
| Externally published | Yes |
| Event | Proceedings of the Workshop on the Foundations of Global Ubiquitous Computing (FGUC 2004) - Duration: 3 Sept 2004 → 3 Sept 2004 |