scholarly journals A Categorical Axiomatics for Bisimulation

1998 ◽  
Vol 5 (22) ◽  
Author(s):  
Gian Luca Cattani ◽  
John Power ◽  
Glynn Winskel
Keyword(s):  
Higher Order ◽  
Parallel Composition ◽  
Process Algebras ◽  
Process Calculi ◽  
Open Map ◽  
Kleisli Category ◽  
Open Maps

We give an axiomatic category theoretic account of bisimulation in process algebras based on the idea of functional bisimulations as open maps. We work with 2-monads, T, on Cat. Operations on processes, such as nondeterministic sum, prexing and parallel composition are modelled using functors in the Kleisli category for the 2-monad T. We may define the notion of open map for any such 2-monad; in examples of interest, that agrees exactly with the usual notion of functional bisimulation. Under a condition on T, namely that it be a dense KZ-monad, which we define, it follows that functors in Kl(T) preserve open maps, i.e., they respect functional bisimulation. We further<br />investigate structures on Kl(T) that exist for axiomatic reasons,<br />primarily because T is a dense KZ-monad, and we study how those structures help to model operations on processes. We outline how this analysis gives ideas for modelling higher order processes. We conclude by making comparison with the use of presheaves and profunctors to model process calculi.

scholarly journals Presheaf Models for CCS-like Languages

1999 ◽  
Vol 6 (36) ◽  
Author(s):  
Gian Luca Cattani ◽  
Glynn Winskel
Keyword(s):  
General Definition ◽  
General Process ◽  
Process Calculi ◽  
Event Structures ◽  
Open Map ◽  
Process Operations ◽  
Definition Of ◽  
Refinement Operator ◽  
Congruence Properties ◽  
Open Maps

The aim of this paper is to harness the mathematical machinery around<br />presheaves for the purposes of process calculi. Joyal, Nielsen and Winskel<br />proposed a general definition of bisimulation from open maps. Here we show<br />that open-map bisimulations within a range of presheaf models are congruences<br /> for a general process language, in which CCS and related languages<br />are easily encoded. The results are then transferred to traditional models<br /> for processes. By first establishing the congruence results for presheaf<br />models, abstract, general proofs of congruence properties can be provided<br />and the awkwardness caused through traditional models not always possessing<br /> the cartesian liftings, used in the break-down of process operations,<br />are side-stepped. The abstract results are applied to show that hereditary<br />history-preserving bisimulation is a congruence for CCS-like languages to<br />which is added a refinement operator on event structures as proposed by<br />van Glabbeek and Goltz.

scholarly journals A Presheaf Semantics of Value-Passing Processes

1996 ◽  
Vol 3 (44) ◽  
Author(s):  
Glynn Winskel
Keyword(s):  
Operational Semantics ◽  
Denotational Semantics ◽  
Domain Theory ◽  
Process Calculi ◽  
Traditional Definition ◽  
Open Maps

This paper investigates presheaf models for process calculi with<br />value passing. Denotational semantics in presheaf models are shown<br />to correspond to operational semantics in that bisimulation obtained<br />from open maps is proved to coincide with bisimulation as defined<br />traditionally from the operational semantics. Both "early" and "late"<br />semantics are considered, though the more interesting "late" semantics<br />is emphasised. A presheaf model and denotational semantics is proposed<br />for a language allowing process passing, though there remains<br />the problem of relating the notion of bisimulation obtained from open<br />maps to a more traditional definition from the operational semantics.<br />A tentative beginning is made of a "domain theory" supporting<br />presheaf models.

scholarly journals Bisimulation for Higher-Order Process Calculi

1996 ◽  
Vol 131 (2) ◽  
pp. 141-178 ◽  
Author(s):  
Davide Sangiorgi
Keyword(s):  
Higher Order ◽  
Order Process ◽  
Process Calculi

scholarly journals Light logics and higher-order processes

2014 ◽  
Vol 26 (6) ◽  
pp. 969-992 ◽  
Author(s):  
UGO DAL LAGO ◽  
SIMONE MARTINI ◽  
DAVIDE SANGIORGI
Keyword(s):  
Polynomial Time ◽  
Linear Logic ◽  
Higher Order ◽  
Resource Control ◽  
Process Algebras ◽  
Π Calculus ◽  
Soft Processes

We show that the techniques for resource control that have been developed by the so-calledlight logicscan be fruitfully applied also to process algebras. In particular, we present a restriction of higher-order π-calculus inspired by soft linear logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.

scholarly journals Recursive equations in higher-order process calculi

2001 ◽  
Vol 266 (1-2) ◽  
pp. 839-852 ◽  
Author(s):  
Mingsheng Ying ◽  
Martin Wirsing
Keyword(s):  
Higher Order ◽  
Order Process ◽  
Process Calculi ◽  
Recursive Equations

scholarly journals New-HOPLA--A Higher-Order Process Language with Name Generation

2004 ◽  
Vol 11 (21) ◽  
Author(s):  
Glynn Winskel ◽  
Francesco Zappa Nardelli
Keyword(s):  
Operational Semantics ◽  
Expressive Power ◽  
Higher Order ◽  
Domain Theory ◽  
Process Algebras ◽  
Order Process ◽  
Pi Calculus ◽  
Mobile Ambients ◽  
Congruence Properties

This paper introduces new-HOPLA, a concise but powerful language for higher-order nondeterministic processes with name generation. Its origins as a metalanguage for domain theory are sketched but for the most part the paper concentrates on its operational semantics. The language is typed, the type of a process describing the shape of the computation paths it can perform. Its transition semantics, bisimulation, congruence properties and expressive power are explored. Encodings are given of well-known process algebras, including pi-calculus, Higher-Order pi-calculus and Mobile Ambients.

scholarly journals Presheaf Models for Concurrency

1996 ◽  
Vol 3 (35) ◽  
Author(s):  
Gian Luca Cattani ◽  
Glynn Winskel
Keyword(s):  
Broad Class ◽  
General Nature ◽  
General Process ◽  
Process Calculi ◽  
Event Structures ◽  
Wide Range ◽  
Concurrent Computation ◽  
Kan Extensions ◽  
Modelling Process ◽  
Open Maps

This paper studies presheaf models for concurrent computation. An aim is to harness the general machinery around presheaves for the purposes of process calculi. Traditional models like synchronisation trees and event structures have been shown to embed fully and faithfully in particular<br />presheaf models in such a way that bisimulation, expressed through the presence of a span of open maps, is conserved. As is shown in the work of Joyal and Moerdijk, presheaves are rich in constructions which preserve open<br />maps, and so bisimulation, by arguments of a very general nature. This paper contributes similar results but biased towards questions of bisimulation in process calculi. It is concerned with modelling process constructions on presheaves, showing these preserve open maps, and with transferring such<br />results to traditional models for processes. One new result here is that a wide range of left Kan extensions, between categories of presheaves, preserve open maps. As a corollary, this also implies that any colimit-preserving functor between presheaf categories preserves open maps. A particular left Kan extension is shown to coincide with a refinement operation on event structures. A broad class of presheaf models is proposed for a general process calculus. General arguments are given for why the operations of a presheaf model preserve open maps and why for specic presheaf models the operations coincide with those of traditional models.

Typing and subtyping for mobile processes

1996 ◽  
Vol 6 (5) ◽  
pp. 409-453 ◽  
Author(s):  
Benjamin Pierce ◽  
Davide Sangiorgi
Keyword(s):  
Process Algebra ◽  
Operational Semantics ◽  
Type System ◽  
Higher Order ◽  
Order Process ◽  
Process Calculi ◽  
Mobile Processes

The π-calculus is a process algebra that supports mobility by focusing on the communication of channels. Milner's presentation of the π-calculus includes a type system assigning arities to channels and enforcing a corresponding discipline in their use. We extend Milner's language of types by distinguishing between the ability to read from a channel, the ability to write to a channel, and the ability both to read and to write. This refinement gives rise to a natural subtype relation similar to those studied in typed λ-calculi. The greater precision of our type discipline yields stronger versions of standard theorems on the π-calculus. These can be used, for example, to obtain the validity of β-reduction for the more efficient of Milner's encodings of the call-by-value λ-calculus, which fails in the ordinary π-calculus. We define the syntax, typing, subtyping, and operational semantics of our calculus, prove that the typing rules are sound, apply the system to Milner's λ-calculus encodings, and sketch extensions to higher-order process calculi and polymorphic typing.

scholarly journals Expressiveness modulo bisimilarity of regular expressions with parallel composition

2015 ◽  
Vol 26 (6) ◽  
pp. 933-968 ◽  
Author(s):  
JOS C. M. BAETEN ◽  
BAS LUTTIK ◽  
TIM MULLER ◽  
PAUL VAN TILBURG
Keyword(s):  
Finite Automata ◽  
Regular Expressions ◽  
Parallel Composition ◽  
Process Algebras ◽  
Star Operation

The languages accepted by finite automata are precisely the languages denoted by regular expressions. In contrast, finite automata may exhibit behaviours that cannot be described by regular expressions up to bisimilarity. In this paper, we consider extensions of the theory of regular expressions with various forms of parallel composition and study the effect on expressiveness. First we prove that adding pure interleaving to the theory of regular expressions strictly increases its expressiveness modulo bisimilarity. Then, we prove that replacing the operation for pure interleaving by ACP-style parallel composition gives a further increase in expressiveness, still insufficient, however, to facilitate the expression of all finite automata up to bisimilarity. Finally, we prove that the theory of regular expressions with ACP-style parallel composition and encapsulation is expressive enough to express all finite automata up to bisimilarity. Our results extend the expressiveness results obtained by Bergstra, Bethke and Ponse for process algebras with (the binary variant of) Kleene's star operation.

Sign in / Sign up

Export Citation Format

Share Document