TY - GEN
T1 - The π-calculus as a theory in linear logic
T2 - 3rd International Workshop on Extensions of Logic Programming, ELP 1992
AU - Miller, Dale
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1993.
PY - 1993/1/1
Y1 - 1993/1/1
N2 - The agent expressions of the π-calculus can be translated into a theory of linear logic in such a way that the reflective and transitive closure of π-calculus (unlabeled) reduction is identified with “entailedby”. Under this translation, parallel composition is mapped to the multiplicative disjunct (“par”) and restriction is mapped to universal quantification. Prefixing, non-deterministic choice (+), replication (!), and the match guard are all represented using non-logical constants, which are specified using a simple form of axiom, called here a process clause. These process clauses resemble Horn clauses except that they may have multiple conclusions; that is, their heads may be the par of atomic formulas. Such multiple conclusion clauses are used to axiomatize communications among agents. Given this translation, it is nature to ask to what extent proof theory can be used to understand the meta-theory of the π-calculus. We present some preliminary results along this line for π0, the “propositional” fragment of the π-calculus, which lacks restriction and value passing (π0 is a subset of CCS). Using ideas from proof-theory, we introduce co-agents and show that they can specify some testing equivalences for π0. If negation-as-failure-to-prove is permitted as a co-agent combinator, then testing equivalence based on co-agents yields observational equivalence for π0. This latter result follows from observing that co-agents directly represent formulas in the Hennessy-Milner modal logic.
AB - The agent expressions of the π-calculus can be translated into a theory of linear logic in such a way that the reflective and transitive closure of π-calculus (unlabeled) reduction is identified with “entailedby”. Under this translation, parallel composition is mapped to the multiplicative disjunct (“par”) and restriction is mapped to universal quantification. Prefixing, non-deterministic choice (+), replication (!), and the match guard are all represented using non-logical constants, which are specified using a simple form of axiom, called here a process clause. These process clauses resemble Horn clauses except that they may have multiple conclusions; that is, their heads may be the par of atomic formulas. Such multiple conclusion clauses are used to axiomatize communications among agents. Given this translation, it is nature to ask to what extent proof theory can be used to understand the meta-theory of the π-calculus. We present some preliminary results along this line for π0, the “propositional” fragment of the π-calculus, which lacks restriction and value passing (π0 is a subset of CCS). Using ideas from proof-theory, we introduce co-agents and show that they can specify some testing equivalences for π0. If negation-as-failure-to-prove is permitted as a co-agent combinator, then testing equivalence based on co-agents yields observational equivalence for π0. This latter result follows from observing that co-agents directly represent formulas in the Hennessy-Milner modal logic.
U2 - 10.1007/3-540-56454-3_13
DO - 10.1007/3-540-56454-3_13
M3 - Conference contribution
AN - SCOPUS:84913004277
SN - 9783540564546
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 242
EP - 264
BT - Extensions of Logic Programming - 3rd International Workshop, ELP 1992, Proceedings
A2 - Lamina, Evelina
A2 - Mello, Paola
PB - Springer Verlag
Y2 - 26 February 1992 through 28 February 1992
ER -