Communication, and concurrency with logic-based restriction inside a calculus of structures
Abstract
It is well known that we can use structural proof theory to refine, or generalize, existing paradigmatic computational primitives, or to discover new ones. Under such a point of view we keep developing a programme whose goal is establishing a correspondence between proof-search of a logical system and computations in a process algebra. We give a purely logical account of a process algebra operation which strictly includes the behavior of restriction on actions we find in Milner CCS. This is possible inside a logical system in the Calculus of Structures of Deep Inference endowed with a self-dual quantifier. Using proof-search of cut-free proofs of such a logical system we show how to solve reachability problems in a process algebra that subsumes a significant fragment of Milner CCS.
Cite
@article{arxiv.1212.4669,
title = {Communication, and concurrency with logic-based restriction inside a calculus of structures},
author = {Luca Roversi},
journal= {arXiv preprint arXiv:1212.4669},
year = {2012}
}
Comments
32 pages. Submitted