This bibliography is a complete bibliography of papers published on bigraphs and closely related areas. The bibliography is currently maintained by Mikkel Bundgaard of the Programming, Logic, and Semantics group at the IT University of Copenhagen. So if you have any questions or comments on the bibliography or the way it is set up, or if you have references to published papers that is currently missing in the bibliography please contact him.
The world is increasingly populated with interactive agents distributed in space, real or abstract. These agents can be artificial, as in computing systems that manage and monitor traffic or health; or they can be natural, e.g. communicating humans, or biological cells. It is important to be able to model networks of agents in order to understand and optimise their behaviour. Robin Milner describes in this book just such a model, by presenting a unified and rigorous structural theory, based on bigraphs, for systems of interacting agents. This theory is a bridge between the existing theories of concurrent processes and the aspirations for ubiquitous systems, whose enormous size challenges our understanding. The book is reasonably self-contained mathematically, and is designed to be learned from: examples and exercises abound, solutions for the latter are provided. Like Milner's other work, this is destined to have far-reaching and profound significance.
We propose a novel and uniform approach to type systems for (process) calculi, which roughly pushes the challenge of designing type systems and proving properties about them to the meta-model of bigraphs. Concretely, we propose to define type systems for the term language for bigraphs, which is based on a fixed set of elementary bigraphs and operators on these. An essential elementary bigraph is an ion, to which a control can be attached modelling its kind (its ordered number of channels and whether it is a guard), e.g. an input prefix of pi-calculus. A model of a calculus is then a set of controls and a set of reaction rules, collectively a bigraphical reactive system (BRS). Possible advantages of developing bigraphical type systems include: a deeper understanding of a type system itself and its properties; transfer of the type systems to the concrete family of calculi that the BRS models; and the possibility of modularly adapting the type systems to extensions of the BRS (with new controls). As proof of concept we present a model of a pi-calculus, develop an i/o-type system with subtyping on this model, prove crucial properties (including subject reduction) for this type system, and transfer these properties to the (typed) pi-calculus.
We present a refinement, suggested by Jensen and Milner under the term kind, of pure bigraphs. We name the result kind bigraphs. This refinement generalises the notion of atomic and non-atomic controls, allowing a control to contain a subset of the set of controls. We show that this variation has relative pushouts and classify its idem pushouts. A canonical labelled transition system can be derived from this classification and we use known results to reason about bisimilarity on this transition system. We show how kind bigraphs can be used to describe Milner's homomorphic sortings and finally discuss the extra expressivity that parametric kind reaction rules allow.
Reactive systems, proposed by Leifer and Milner, represent a meta-framework aimed at deriving behavioral congruences for those specification formalisms whose operational semantics is provided by rewriting rules. Despite its applicability, reactive systems suffered so far from two main drawbacks. First of all, no technique was found for recovering a set of inference rules, e.g. in the so-called SOS style, for describing the distilled observational semantics. Most importantly, the efforts focused on strong bisimilarity, tackling neither weak nor barbed semantics. Our paper addresses both issues, instantiating them on a calculus whose semantics is still in a flux: Cardelli and Gordon's mobile ambients. While the solution to the first issue is tailored over our case study, we provide a general framework for recasting (weak) barbed equivalence in the reactive systems formalism. Moreover, we prove that our proposal captures the behavioural semantics for mobile ambients proposed by Rathke and Sobocinski and by Merro and Zappa Nardelli.
The paper presents a case study on the synthesis of labelled transition systems (LTSs) for process calculi, choosing as testbed Cardelli and Gordon's Mobile Ambients (MAs). The proposal is based on a graphical encoding: each process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence. Graphs with interfaces are amenable to the synthesis mechanism proposed by Ehrig and König and based on borrowed contexts (BCs), an instance of relative pushouts, introduced by Leifer and Milner. The BC mechanism allows the effective construction of a LTS that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. Our paper focuses on the analysis of a LTS over (processes as) graphs with interfaces, as distilled by exploiting the graphical encoding of MAs. In particular, we use the LTS on graphs to recover a suitable LTS directly defined over the structure of MAs processes.
We develop a theory of sorted bigraphical reactive systems. Every application of bigraphs in the literature has required an extension, a sorting, of pure bigraphs. In turn, every such application has required a redevelopment of the theory of pure bigraphical reactive systems for the sorting at hand. Here we present a general construction of sortings. The constructed sortings always sustain the behavioural theory of pure bigraphs (in a precise sense), thus obviating the need to redevelop that theory for each new application. As an example, we recover Milner's local bigraphs as a sorting on pure bigraphs.Technically, we give our construction for ordinary reactive systems, then lift it to bigraphical reactive systems. As such, we give also a construction of sortings for ordinary reactive systems. This construction is an improvement over previous attempts in that it produces smaller and much more natural sortings, as witnessed by our recovery of local bigraphs as a sorting.
We study the algebraic structure of directed bigraphs, a bigraphical model of computations with locations, connections and resources previously introduced as a unifying generalization of other variants of bigraphs. We give a sound and complete axiomatization of the (pre)category of directed bigraphs. Using this axiomatization, we give an adequate encoding of the Fusion calculus, showing the utility of the added directness.
Bigraphical reactive systems are an emerging graphical framework proposed by Milner and others [4,5,2,3] as a unifying theory of process models for distributed, concurrent and ubiquitous computing. A bigraphical reactive system consists of a category of bigraphs (usually generated over a given signature of controls) and a set of reaction rules. Bigraphs can be seen as representations of the possible configurations of the system, and the reaction rules specify how these configuration can evolve. The advantage of using bigraphical reactive systems is that they provide general results for deriving a labelled transition system automatically from the reaction rules, via the so-called IPO construction. Notably, the bisimulation on this transition system is always a congruence.
We study directed bigraph with negative ports, a bigraphical framework for representing models for distributed, concurrent and ubiquitous computing. With respect to previous versions, we add the possibility that components may govern the access to resources, like (web) servers control requests from clients. This framework encompasses many common computational aspects, such as name or channel creation, references, client/server connections, localities, etc, still allowing to derive systematically labelled transition systems whose bisimilarities are congruences.As application examples, we analyse the encodings of client/server communications through firewalls, of (compositional) Petri nets and of chemical reactions.
Bigraphs are a framework in which both existing process calculi and new models of behaviour can be formulated, yielding theory that is shared among these models. A short survey of the main features of bigraphs is presented, showing how they can be developed from standard graph theory using elementary category theory. The algebraic manipulation of bigraphs is outlined with the help of illustrations. The treatment of dynamics is then summarised. Finally, origins and some related work are discussed. The paper provides a motivating introduction to bigraphs.
Symbolic bisimulations were introduced as a mean to define value-passing process calculi using smaller, possibly finite labelled transition systems, equipped with symbolic actions. Similar ideas have been used for modeling with fewer transitions the input behavior of open and asynchronous pi-calculus. In this paper we generalize the symbolic technique and apply the resulting theory to these two cases, re-deriving existing results. We also apply our approach to a new setting, i.e. open Petri nets, with the usual result of reducing input transitions. Our theory generalizes Leifer and Milner reactive systems by adding observations.
We propose and formalize HomeBPEL, a higher-order WSBPEL-like business process execution language where processes are first-class values that can be stored in variables, passed as messages, and activated as embedded sub-instances. A sub-instance is similar to a WSBPEL scope, except that it can be dynamically frozen and stored as a process in a variable, and then subsequently be thawed when reactivated as a sub-instance. We motivate HomeBPEL by an example of pervasive health care where treatment guidelines are dynamically deployed as sub processes that may be delegated dynamically to other workflow engines and in particular stay available for disconnected operation on mobile devices. We provide a formal semantics based on binding bigraphical reactive systems implemented in the BPL Tool as part of the Bigraphical Programming Languages project at ITU. The semantics is an extension of a semantics given previously for a simplified subset of WS-BPEL and exploits the close correspondence between bigraphs and XML to provide a formalized run-time format very close to standard WS-BPEL syntax, which also constitutes the representation of frozen sub-instances.
With the spread of the Internet and software evolution in complex intensive systems, software architecture often need be reconfigured during runtime to adapt variable environ-ments and design objectives. To deal with reconfigurable software architectures, the formal method should be pre-sented to describe software architectures and express their changes so that these changes on the evolutions of software architectures could be reasoned about. However, current formal methods for reconfigurable software architectures are difficult to represent hierarchy and model context-aware systems. In this paper, we use and extend Bigraph as a formal method to describe reconfigurable software archi-tecture. By providing graphic elements and term languages, extended bigraphs can survey static and dynamic architec-tures easily. Then we represent basic architectural opera-tions based on extended bigraphs, through a case describe reconfigurations with constraints and context-aware infor-mation by reaction rules, and illustrate how to check the properties to satisfy design requirements by BiLog.
In this paper, we give a bigraphical model for web services composition. We investigate how to represent scope-based compensation handing mechanism by means of Bigraphical Reactive Systems (BRSs for short), which have been proposed to provide a uniform way to model spatially distributed systems that both compute and communicate. The service composition language we focus on is WSBPEL, which is the standard of web service composition and orchestration. This bigraphical model can be regarded as a unifying semantics of BPEL-like languages with the key concepts related to compensation handling. The rationality of the model is discussed by investigating the relationship between BPEL language and BRSs. Based on the bigraphical model, the algebraic laws for BPEL are proved as well.
In this paper we present a stochastic semantics for Bigraphical Reactive Systems. A reduction and a labelled stochastic semantics for bigraphs are defined. As a sanity check, we prove that the two semantics are consistent with each other. We illustrate the expressiveness of the framework with an example of membrane budding in a biological system.
We analyze the matching problem for bigraphs. In particular, we present a sound and complete inductive characterization of matching of binding bigraphs. Our results pave the way for a provably correct matching algorithm, as needed for an implementation of bigraphical reactive systems.
We study the construction of labelled transition systems from reactive systems defined over directed bigraphs, a computational meta-model which subsumes other variants of bigraphs. First we consider wide transition systems whose labels are all those generated by the IPO construction; the corresponding bisimulation is always a congruence. Then, we show that these LTSs can be simplified further by restricting to a subclass of labels, which can be characterized syntactically.We apply this theory to the Fusion calculus: we give an encoding of Fusion in directed bigraphs, and describe its simplified wide transition system and corresponding bisimulation.
We introduce directed bigraphs, a bigraphical meta-model for describing computational paradigms dealing with locations and resource communications. Directed bigraphs subsume and generalize both original Milner's and Sassone-Sobocinski's variants of bigraphs. The key novelty is that directed bigraphs take account of the ``resource request flow'' inside link graphs, from controls to edges (through names), by means of the new notion of directed link graph. We give RPO and IPO constructions for this model, generalizing and unifying the constructions independently given by Jensen-Milner and Sassone-Sobocinski in their respective variants. Moreover, the very same construction can be used for calculating RPBs as well, and hence also luxes (when these exist). Therefore, directed bigraphs can be used as a general theory for deriving labelled transition systems (and congruence bisimulations) from (possibly open) reactive systems.
With the spread of the Internet and software evolution in complex intensive systems, software architecture often need be reconfigured during run time in dynamic, heterogeneous environments in order to satisfy design objectives, which poses new problems such as, does the architecture of a system conform to the given architectural style? Existing formal methods for the conformance check are either obscure to be understood, or inadequate to express parameters, global conditions, and so on. In this paper, we present an approach to check architectural instance conforming to its style based on bigraphical reactive systems (BRSs). We extend bigraph and Omega-sorted BRS to describe architectural instance and architectural style respectively, and provide an approach to support the conformance check. The approach not only provides a visual and formal mechanism to specify architectural instances and styles, but also enriches the capability to model evolving systems and deal with parametric reaction rules, which are excellent over other existing formal methods naturally. An important theorem the changing bigraphs always preserve the constraints defined by Omega-sorted BRS if the initial bigraph and reaction rules do is proved and a conformance algorithm is presented. Two cases are studied in order to illustrate the effectiveness of our approach.
Reactive Systems ŕ la Leifer and Milner allow to derive from a reaction semantics definition an LTS equipped with a bisimilarity relation which is a congruence. This theory has been extended by the authors (together with Barbara König) in order to handle saturated bisimilarity, a coarser equivalence that is more adequate for some interesting formalisms, such as logic programming and open pi-calculus. In this paper we recast the theory of Reactive Systems inside Universal Coalgebra. This construction is particularly useful for saturated bisimilarity, which can be seen as final semantics of Normalized Coalgebras. These are structured coalgebras (not bialgebras) where the sets of transitions are minimized rather than maximized as in saturated LTS, still yielding the same semantics. We give evidence the effectiveness of our approach minimizing an Open Petri net in a category of Normalized Coalgebras.
Aiming at a unified view of the logics describing spatial structures, we introduce a general framework, BiLog, whose formulae characterise monoidal categories. As a first instance of the framework we consider bigraphs, which are emerging as a an interesting (meta-)model for spatial structures and distributed calculi. Since bigraphs are built orthogonally on two structures, a hierarchical place graph for locations and a link (hyper-)graph for connections, we obtain a logic that is a natural composition of other two instances of BiLog: a Place Graph Logic and a Link Graph Logic. We prove that these instances generalise the spatial logics for trees, for graphs and for tree contexts. We also explore the concepts of separation and sharing in these logics. We note that both the operator * of Separation Logic and the operator | of spatial logics do not completely separate the underlying structures. These two different forms of separation can be naturally derived as instances of BiLog by using the complete separation induced by the tensor product of monoidal categories along with some form of sharing.
The notion of confluence is studied on the context of bigraphs. Confluence will be important in modelling real-world systems, both natural (as in biology) and artificial (as in pervasive computing). The paper uses bigraphs in which names have multiple locality; this enables a formulation of the lambda calculus with explicit substitutions. The paper reports work in progress, seeking conditions on a bigraphical reactive system that are sufficient to ensure confluence; the conditions must deal with the way that bigraphical redexes can be intricately intertwined. The conditions should also be satisfied by the lambda calculus. After discussion of these issues, two conjectures are put forward.
We investigate sorting or typing for Leifer and Milner's reactive systems. We focus on transferring congruence properties for bisimulations from unsorted tosorted systems. Technically, we give a general definition of sorting; we adapt Jensen's work on the transfer of congruence properties to this general definition; we construct a predicate sorting, which, for any decomposible predicate P filters out agents not satisfying P; we prove that the predicatesorting preserves congruence properties and that it suitably retains dynamics; and finally, we show how the predicate sortings can be used to achieve context-aware reaction.
The Bigraphical Programming Language project at IT University of Copenhagen contributes to the UKCRC Ubiquitous Computing Grand Challenge by researching the use of bigraphical reactive systems as a general framework in which to combine theories for design and analysis with techniques, tools and methodologies for engineering and systems building. Initial work has been addressing Context-awareness, business processes and Reactive XML, axiomatisation and matching, and higher-order mobile embedded resources.
As part of ongoing work on evaluating Milner's bigraphical reactive systems, we investigate bigraphical models of context-aware systems, a facet of ubiquitous computing. We nd that naively encoding such systems in bigraphs is somewhat awkward; and we propose a more sophisticated modeling technique, introducing Plato-graphical models, alleviating this awkwardness. We argue that such models are useful for simulation and point out that for reasoning about such bigraphical models, the bisimilarity inherent to bigraphical reactive systems is not enough in itself; an equivalence between the bigraphical reactive systems themselves is also needed.
Bigraphical Reactive Systems have been proposed as a meta model for global ubiquitous computing generalising process calculi for mobility such as the pi-calculus and the Mobile Ambients calculus as well as graphical models for concurrency such as Petri Nets. We investigate in this paper how Bigraphical Reactive Systems represented as Reactive XML can be used to provide a formal semantics as well as an extensible and mobile platform independent execution format for XML based business process and workflow description languages such as WS-BPEL and XPDL. We propose to extend the formalism with primitives for XPath evaluation and higher-order reaction rules to allow for a very direct and succinct semantics.
We axiomatize the congruence relation for binding bigraphs and prove that the generated theory is complete. In doing so, we define a normal form for binding bigraphs, and prove that it is unique up to certain isomorphisms. Our work builds on Milner's axioms for pure bigraphs. We have extended the set of axioms with five new axioms concerned with binding, and we have altered some of Milner's axioms for ions, because ions in binding bigraphs have names on both their inner and outer faces. The resulting theory is a conservative extension of Milner's for pure bigraphs.
Bigraphs have been introduced with the aim to provide a topographical meta-model for mobile, distributed agents that can manipulate their own linkages and nested locations, generalising both characteristics of the pi-calculus and the Mobile Ambients calculus. We give the rst bigraphical presentation of a non-linear, higher-order process calculus with nested locations, non-linear active process mobility, and local names, the calculus of Higher-Order Mobile Embedded Resources (Homer). The presentation is based on Milner's recent presentation of the lambda-calculus in local bigraphs. The combination of non-linear active process mobility and local names requires a new denition of parametric reaction rules and a representation of the location of names. We suggest localised bigraphs as a generalisation of local bigraphs in which links can be further localised.
Bigraphs have been introduced with the aim to provide a topographical meta-model for mobile, distributed agents that can manipulate their own communication links and nested locations. In this paper we examine a presentation of type systems on bigraphical systems using the notion of sorting. We focus our attention on the typed polyadic pi-calculus with capability types ŕ la Pierce and Sangiorgi, which we represent using a novel kind of link sorting called subsorting. Using the theory of relative pushouts we derive a labelled transition system which yield a coinductive characterisation of a behavioural congruence for the calculus. The results obtained in this paper constitute a promising foundation for the presentation of various type systems for the (polyadic) pi-calculus as sortings in the setting of bigraphs.
A framework is defined within which reactive systems can be studied formally. The framework is based on s-categories, which are a new variety of categories within which reactive systems can be set up in such a way that labelled transition systems can be uniformly extracted. These lead in turn to behavioural preorders and equivalences, such as the failures preorder (treated elsewhere) and bisimilarity, which are guaranteed to be congruential. The theory rests on the notion of relative pushout, which was previously introduced by the authors.The framework is applied to a particular graphical model, known as link graphs, which encompasses a variety of calculi for mobile distributed processes. The specific theory of link graphs is developed. It is then applied to an established calculus, namely condition-event Petri nets.
In particular, a labelled transition system is derived for condition-event nets, corresponding to a natural notion of observable actions in Petri-net theory. The transition system yields a congruential bisimilarity coinciding with one derived directly from the observable actions. This yields a calibration of the general theory of reactive systems and link graphs against known specific theories.
The semantics of process calculi has traditionally been specified by labelled transition systems (LTS), but with the development of name calculi it turned out that reaction rules (i.e., unlabelled transition rules) are often more natural. This leads to the question of how behavioural equivalences (bisimilarity, trace equivalence, etc.) defined for LTS can be transferred to unlabelled transition systems. Recently, in order to answer this question, several proposals have been made with the aim of automatically deriving an LTS from reaction rules in such a way that the resulting equivalences are congruences. Furthermore these equivalences should agree with the standard semantics, whenever one exists.In this paper we propose saturated semantics, based on a weaker notion of observation and orthogonal to all the previous proposals, and we demonstrate the appropriateness of our semantics by means of two examples: logic programming and a subset of the open pi-calculus. Indeed, we prove that our equivalences are congruences and that they coincide with logical equivalence and open bisimilarity respectively, while equivalences studied in previous works are strictly finer.
The paper presents a case study on the synthesis of labelled transition systems (LTSS) for process calculi, choosing as testbed Milner's Calculus of Communicating System (CCS). The proposal is based on a graphical encoding: each CCS process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence.Graphs with interfaces are amenable to the synthesis mechanism based on borrowed contexts (BCS), proposed by Ehrig and König (which are an instance of relative pushouts, originally introduced by Milner and Leifer). The BC mechanism allows the effective construction of an LTS that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence.
Our paper focuses on the analysis of the LTS distilled by exploiting the encoding of ccs processes: besides offering some technical contributions towards the simplification of the BC mechanism, the key result of our work is the proof that the bisimilarity on processes obtained via BCS coincides with the standard strong bisimilarity for CCS.
Bigraphs are graphs whose nodes may be nested, representing locality, independently of the edges connecting them. They may be equipped with reaction rules, forming a bigraphical reactive system (Brs) in which bigraphs can reconfigure themselves. Following an earlier paper describing link graphs, a constituent of bigraphs, this paper is a devoted to pure bigraphs, which in turn underlie various more refined forms. Elsewhere it is shown that behavioural analysis for Petri nets, pi-calculus and mobile ambients can all be recovered in the uniform framework of bigraphs. The paper first develops the dynamic theory of an abstract structure, a wide reactive system (Wrs), of which a Brs is an instance. In this context, labelled transitions are defined in such a way that the induced bisimilarity is a congruence. This work is then specialised to Brss, whose graphical structure allows many refinements of the theory. The latter part of the paper emphasizes bigraphical theory that is relevant to the treatment of dynamics via labelled transitions. As a running example, the theory is applied to finite pure CCS, whose resulting transition system and bisimilarity are analysed in detail. The paper also mentions briefly the use of bigraphs to model pervasive computing and biological systems.
The rho-calculus generalises both term rewriting and the lambda-calculus in a uniform framework. Interaction nets are a form of graph rewriting which proved most successful in understanding the dynamics of the lambda-calculus, the prime example being the implementation of optimal beta-reduction. It is thus natural to study interaction net encodings of the rho-calculus as a first step towards the definition of efficient reduction strategies. We give two interaction net encodings which bring a new understanding to the operational semantics of the rho-calculus; however, these encodings have some drawbacks and to overcome them we introduce bigraphical nets - a new paradigm of computation inspired by Lafont's interactions nets and Milner's bigraphs.
XML-centric models of computation have been proposed as an answer to the demand for interoperability, heterogeneity and openness in coordination models. We present a prototype implementation of an open XML-centric coordination middleware called Distributed Reactive XML. The middleware has as theoretical foundation a general distributed extensible process calculus inspired by the theory of Bigraphical Reactive Systems. The calculus is extensible just as XML is extensible, in that its signature and reaction rules are not fixed. It is distributed by allowing both the state of processes as well as the set of reaction rules to be distributed (or partly shared) between different clients. The calculus is implemented by representing process terms as XML documents stored in a value-oriented, peer-to-peer XML Store and reaction rules as XML transformations performed by the clients. The formalism does not require that only process terms are stored-inside process terms one may store application specific data as well. XML Store provides transparent sharing of process terms between all participating peers. Conflicts between concurrent reaction rules are handled by an optimistic concurrency control. The implementation thus provides an open XML-based coordination middleware with a formal foundation that encompasses both the shared data, processes and reaction rules.
Graph-rewriting has been a growing discipline for over three decades. It grew out of the study of graph grammars, in which - analogously to string and tree grammars - a principal interest was to describe the families of graphs that could be generated from a given set of productions. A fundamental contribution was, of course, the double-pushout construction of Ehrig and his colleagues [4]; it made precise how the left-hand side of a production, or rewriting rule, could be found to occur in a host graph, and how it should then be replaced by the right-hand side. This break-through led to many theoretical developments and many applications. It relies firmly upon the treatment of graphs as objects in a category whose arrows are embedding maps.
Groupoidal relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. In this paper, we develop the theory of GRPOs further, proving that well-known equivalences, other than bisimulation, are congruences. To demonstrate the type of category theoretic arguments which are inherent in the 2-categorical approach, we construct GRPOs in a category of ``bunches and wirings.'' Finally, we prove that the 2-categorical theory of GRPOs is a generalisation of the approaches based on Milner's precategories and Leifer's functorial reactive systems.
We introduce a way of viewing Petri nets as open systems. This is done by considering a bicategory of cospans over a category of p/t nets and embeddings. We derive a labelled transition system (LTS) semantics for such nets using GIPOs and characterise the resulting congruence. Technically, our results are similar to the recent work by Milner on applying the theory of bigraphs to Petri Nets. The two main differences are that we treat p/t nets instead of c/e nets and we deal directly with a category of nets instead of encoding them into bigraphs.
The theory of reactive systems, introduced by Leifer and Milner and previously extended by the authors, allows the derivation of well-behaved labelled transition systems (LTS) for semantic models with an underlying reduction semantics. The derivation procedure requires the presence of certain colimits (or, more usually and generally, bicolimits) which need to be constructed separately within each model. In this paper, we offer a general construction of such bicolimits in a class of bicategones of cospans. The construction sheds light on as well as extends Ehrig and Konig's rewriting via borrowed contexts and opens the way to a unified treatment of several applications.
The focus of process calculi is interaction rather than computation, and for this very reason: (i) their operational semantics is conveniently expressed by labelled transition systems (LTSs) whose labels model the possible interactions with the environment; (ii) their abstract semantics is conveniently expressed by observational congruences. However, many current-day process calculi are more easily equipped with reduction semantics, where the notion of observable action is missing. Recent techniques attempted to bridge this gap by synthesising LTSs whose labels are process contexts that enable reactions and for which bisimulation is a congruence. Starting from Sewell's set-theoretic construction, category-theoretic techniques were defined and based on Leifer and Milner's relative pushouts, later refined by Sassone and the fourth author to deal with structural congruences given as groupoidal 2-categories. Building on recent works concerning observational equivalences for tile logic, the paper demonstrates that double categories provide an elegant setting in which the aforementioned contributions can be studied. Moreover, the formalism allows for a straightforward and natural definition of weak observational congruence.
We consider open terms and parametric rules in the context of the systematic derivation of labelled transitions from reduction systems.
Bigraphs are emerging as an interesting model that can represent both the picalculus and the ambient calculus. Bigraphs are built orthogonally on two structures: a hierarchical `place' graph for locations and a `link' (hyper-)graph for connections. In a previous work (submitted elsewhere and yet unpublished), we introduced a logic for bigraphical structures as a natural composition of a place graph logic and a link graph logic. Here we show that fragments of BiLogic can be used to describe XML data (with ID and IDREFs) and to reason about programs that manipulate tree-structures with query-oriented update operators.
Bigraphs are emerging as an interesting model for concurrent calculi, like CCS, pi-calculus, and Petri nets. Bigraphs are built orthogonally on two structures: a hierarchical place graph for locations and a link (hyper-)graph for connections. With the aim of describing bigraphical structures, we introduce a general framework for logics whose terms represent arrows in monoidal categories. We then instantiate the framework to bigraphical structures and obtain a logic that is a natural composition of a place graph logic and a link graph logic. We explore the concepts of separation and sharing in these logics and we prove that they generalise some known spatial logics for trees, graphs and tree contexts.
This paper axiomatises the structure of bigraphs, and proves that the resulting theory is complete. Bigraphs are graphs with double structure, representing locality and connectivity. They have been shown to represent dynamic theories for the pi-calculus, mobile ambients and Petri nets in a way that is faithful to each of those models of discrete behaviour. While the main purpose of bigraphs is to understand mobile systems, a prerequisite for this understanding is a well-behaved theory of the structure of states in such systems. The algebra of bigraph structure is surprisingly simple, as this paper demonstrates; this is because bigraphs treat locality and connectivity orthogonally.
This article is an overview of the recent developments of a theory originally introduced by Leifer and Milner: given a formalism with a reduction semantics, a canonical labelled transition system is derived on which bisimilarity as well as other other equivalences are congruences, provided that the contexts of the formalism form the arrows of a category which has certain colimits. We shall also attempt to provide a context for these developments by offering a review of related work.
A bigraphical reactive system (BRS) involves bigraphs, in which the nesting of nodes represents locality, independently of the edges connecting them. BRSs represent a wide variety of calculi for mobility, including pi-calculus and ambient calculus. A labelled transition system (LTS) for each BRS is here derived uniformly, adapting previous work of Leifer and Milner, so that under certain conditions the resulting bisimilarity is automatically a congruence. For an asynchronous pi-calculus, this LTS and its bisimilarity agree closely with the standard.
A simple example is given of the use of bigraphical reactive systems (BRSs). It provides a behavioural semantics for condition-event Petri nets whose interfaces are named condition nodes, using a simple form of BRS equipped with a labelled transition system and its associated bisimilarity equivalence. Both of the latter are derived from the standard net firing rules by a uniform technique in bigraphs, which also ensures that the bisimilarity is a congruence. Furthermore, this bisimilarity is shown to coincide with one induced by a natural notion of experiment on condition-event nets, defined independently of bigraphs. The paper is intended as a bridge between Petri net theory and bigraphs, as well as a pedagogical exercise in the latter.
We introduce G-relative-pushouts (GRPO) which are a 2-categorical generalisation of relative-pushouts (RPO). They are suitable for deriving labelled transition systems (LTS) for process calculi where terms are viewed modulo structural congruence. We develop their basic properties and show that bisimulation on the LTS derived via GRPOs is a congruence, provided that sufficiently many GRPOs exist. The theory is applied to a simple subset of CCS and the resulting LTS is compared to one derived using a procedure proposed by Sewell.
G-relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. This paper develops the theory of GRPOs further, arguing that they provide a simple and powerful basis towards a comprehensive solution. As an example, we construct GRPOs in a category of `bunches and wirings.' We then examine the approach based on Milner's precategories and Leifer's functorial reactive systems, and show that it can be recast in a much simpler way into the 2-categorical theory of GRPOs.
We introduce G-relative-pushouts (GRPO) which are a 2-categorical generalisation of relative-pushouts (RPO). They are suitable for deriving labelled transition systems (LTS) for process calculi where terms are viewed modulo structural congruence. We develop their basic properties and show that bisimulation on the LTS derived via GRPOs is a congruence, provided that sufficiently many GRPOs exist. The theory is applied to a simple subset of CCS and the resulting LTS is compared to one derived using a procedure proposed by Sewell.
A notion of bigraph is introduced as a model of mobile interaction. A bigraph consists of two independent structures: a topograph representing locality and an edge net representing connectivity. Bigraphs are equipped with reaction rules to form bigraphical reactive systems (BRSs), which include versions of the -calculus and the ambient calculus. A behavioural theory is established, using the categorical notion of relative pushout; itallows labelled transition systems to be derived uniformly for a wide variety of BRSs, in such a way that familiar behavioural preorders and equivalences, in particular bisimilarity, are congruential. An example of the derivation is discussed.
A notion of bigraph is introduced as a model of mobile interaction. A bigraph consists of two independent structures: a topograph representing locality and an edge net representing connectivity. Bigraphs are equipped with reaction rules to form bigraphical reactive systems (BRSs), which include versions of the pi-calculus and the ambient calculus. A behavioural theory is established, using the categorical notion of relative pushout; it allows labelled transition systems to be derived uniformly for a wide variety of BRSs, in such a way that familiar behavioural preorders and equivalences, in particular bisimilarity, are congruential. An example of the derivation is discussed.
The dynamics of reactive systems, e.g. CCS, has often been defined using a labelled transition system (LTS). More recently it has become natural in defining dynamics to use reaction rules - i.e. unlabelled transition rules - together with a structural congruence. But LTSs lead more naturally to behavioural equivalences. so one would like to derive from reaction rules a suitable LTS.This paper shows how to derive an LTS for a wide range of reactive systems. A label for an agent a is defined to be any context F which intuitively is just large enough so that the agent Fa ($a$ in context $F$) is able to perform a reaction. The key contribution of this paper is a precise definition of just large enough, in terms of the categorical notion of relative pushout (RPO), which ensures that bisimilarity is a congruence when sufficient RPOs exist. Two examples - a simplified form of action calculi and term-rewriting - are given, for which it is shown that sufficient RPOs indeed exist. The thrust of this paper is, therefore, towards a general method for achieving useful behavioural congruence relations.
The dynamics of reactive systems, e.g. CCS, has often been defined using a labelled transition system (LTS). More recently it has become natural in defining dynamics to use reaction rules - i.e. unlabelled transition rules - together with a structural congruence. But LTSs lead more naturally to behavioural equivalences. So one would like to derive from reaction rules a suitable LTS. This paper shows how to derive an LTS for a wide range of reactive systems. A label for an agent a is defined to be any context F which intuitively is just large enough so that the agent Fa (``a in context F'') is able to perform a reaction. The key contribution of this paper is a precise definition of, , in terms of the categorical notion of relative pushout (RPO), which ensures that bisimilarity is a congruence when sufficient RPOs exist. Two examples - a simplified form of action calculi and term-rewriting - are given, for which it is shown that sufficient RPOs indeed exist. The thrust of this paper is, therefore, towards a general method for achieving useful behavioural congruence relations.
Monoidal categories of acyclic graphs capture the notion of multi-hole context, pervasive in syntax and semantics. Milner's bigraphs is a recent example. We give a method for generalising such categories to monoidal closed categories of acyclic graphs. The method combines the Int-construction, lifting traced monoidal categories to compact closed ones; the recent formulation of sortings for reactive systems; and games for multiplicative linear logic. The closed categories obtained by our construction captures a notion of higher-order contexts. These encompass extensions to the traditional notion of context found in recent work on Milner's reactive systems and bigraphs. We demonstrate how technical devices employed in these extensions are in fact intrinsic to higher-order contexts. Finally, we use the method to construct higher-order bigraphs, recovering directed bigraphs as a limited instance.
We introduce a formal language, the C-calculus, for modelling low-level interaction inside and among cells, the basic building blocks of all known life. We focus on two main actors of cells, proteins and membranes. Proteins are represented as clusters of domains sharing a common hidden name; domain-domain bonds are also represented via name-sharing. Compartments are formed by formal membranes. We treat also channels between membranes allowing transport of proteins, allowing us to capture an observable intermediate state in cell fusion or division, regulated by diffusion. We illustrate the calculus by giving two example models. We exemplify the basic constituents of the calculus, by developing a model of simple cross-membrane signalling via a G-protein coupled receptor protein. We continue by developing a model illustrating part of the endocytic pathway - the formation of clathrin-coated cytoplasmic vesicles, through budding from the plasma membrane (the cell-wall).
Several efforts have shown that process calculi developed for reasoning about concurrent and mobile systems may be employed for modelling biological systems at the molecular level. In this paper, we initiate investigation of the meta-language framework bigraphical reactive systems, due to Milner et al., as a basis for developing rule-based languages for molecular biology. We describe a family of B^{Sigma}_{R}-calculi sharing a small set of familiar operators and operations, and provide them with a simple operational semantics. We show that B^{Sigma}_{R}-calculi and their reaction semantics correspond to a version of bigraphical reaction under non-aliasing contexts and with reaction rules extended to allow negative side-conditions for the subset of bigraphs corresponding to B^{Sigma}_{R}-processes. Finally, to illustrate the usage of B^{Sigma}_{R}, we show that with non-aliasing semantics the Kappa-calculus may be faithfully captured as a B^{Sigma}_{R}-calculus.
We propose a novel and uniform approach to type systems for (process) calculi, which roughly pushes the challenge of designing type systems and proving properties about them to the meta-model of bigraphs. Concretely, we propose to define type systems for the term language for bigraphs, which is based on a fixed set of elementary bigraphs and operators on these. An essential elementary bigraph is an ion, to which a control can be attached modelling its kind (its ordered number of channels and whether it is a guard), e.g. an input prefix of pi-calculus. A model of a calculus is then a set of controls and a set of reaction rules, collectively a bigraphical reactive system (BRS). Possible advantages of developing bigraphical type systems include: a deeper understanding of a type system itself and its properties; transfer of the type systems to the concrete family of calculi that the BRS models; and the possibility of modularly adapting the type systems to extensions of the BRS (with new controls). As proof of concept we present a model of a pi-calculus, develop an i/o-type system with subtyping on this model, prove crucial properties (including subject reduction) for this type system, and transfer these properties to the (typed) pi-calculus.
Bigraphical Reactive Systems (BRSs) have been proposed as a formal meta-model for global ubiquitous computing that encompasses process calculi for mobility, notably the pi-calculus and the Mobile Ambients calculus, as well as graphical models for concurrency such as Petri Nets. In this paper we demonstrate that BRSs also allow natural formalizations of programming languages used in practice. We do so by providing a direct and extensible formalization of a subset of WS-BPEL as a binding bigraphical reactive system using the BPL Tool developed in the Bigraphical Programming Languages (BPL) project. The tool allows for compositional definition, visualization and simulation of the execution of bigraphical reactive systems. The formalization exploits the close correspondence between bigraphs and XML to provide a formalized run-time format very close to standard WS-BPEL syntax.The formalization is the starting point of an endeavor to provide a completely formalized and extensible business process engine within the Computer Supported Mobile Adaptive Business Processes (CosmoBiz) research project at the IT University of Copenhagen. Building upon the formalization of WS-BPEL we propose and formalize HomeBPEL, a higher-order WS-BPEL-like business process execution language where processes are first-class values that can be stored in variables, passed as messages, and activated as embedded sub-instances. A sub-instance is similar to a WS-BPEL scope, except that it can be dynamically frozen and stored as a process in a variable, and then subsequently be thawed when reactivated as a sub-instance. We motivate HomeBPEL by an example of pervasive health care where treatment guidelines are dynamically deployed as sub processes that may be delegated dynamically to other workflow engines and in particular stay available for disconnected operation on mobile devices.
We introduce directed bigraphs, a bigraphical meta-model for describing computational paradigms dealing with locations and resource communications. Directed bigraphs subsume and generalize both original Milner's and Sassone-Sobocinski's variants of bigraphs. The key novelty is that directed bigraphs take account of the ``resource request flow'' inside link graphs, from controls to edges (through names), by means of the new notion of directed link graph.For this model we give RPO and IPO constructions, generalizing and unifying the constructions independently given by Jensen-Milner and Sassone- Sobocinski in their respective variants. Moreover, the very same construction can be used for calculating RPBs as well, and hence also luxes (when these exist). Therefore, directed bigraphs can be used as a general theory for deriving labelled transition systems (and congruence bisimulations) from (possibly open) reactive systems.
We study also the algebraic structure of directed bigraphs: we give a sound and complete axiomatization of the (pre)category of directed bigraphs. Moreover, we use this axiomatization for encoding the lambda-calculus, both in call-by-name and call-by-value variants.
We analyze the matching problem for bigraphs. In particular, we present an axiomatization of the static theory of binding bigraphs, a non-trivial extension of the axiomatization of pure bigraphs developed by Milner. Based directly on the term language resulting from the axiomatization we present a sound and complete inductive characterization of matching of binding bigraphs. Our results pave the way for an actual matching algorithm, as needed for an implementation of bigraphical reactive systems.
In this progress report we begin evaluation of how well-suited Høgh Jensen and Milner's bigraphical reactive systems (BRSs) [JM04] are for modelling context-aware computing in ubiquitous systems. In this work we concentrate on the location aspect of context. First, we intro- duce the setting, motivate our work, and state our hypothesis. Then we present a digest of the research literature on location models forming a knowledge base for the rest of the report. We continue by developing bigraphical models of context-awareness and argue that these so-called Plato-graphical models constitute a proper foundation for modelling and simulating context-aware systems. A feature is that different cal- culi or programming languages can be combined in one model. Subsequently we define and analyse an encoding of a MiniML-like calculus with references in bigraphs (BRSs). This is needed for our implementation of a representative, minimalistic location model as a Plato-graphical model. Finally, we compare our approach to related work within context calculi, give directions for future work, and conclusions.
This work explores confluence and termination in Milner's encoding of the lambda-calculus as a bigraphical reactive system. In that work, the lambda-calculus was extended with explicit subsitutions and the extension (Lambdasub) was encoded as a bigraphical reactive system.We prove that the reduction relation of the extension is confluent on ground terms and preserves strong normalisation (PSN) of beta- reduction. This gives us corresponding proofs for the bigraphical encoding. The proofs are based on the strong relationship between Lambdasub and the calculus lambdaxgc of Bloo and Rose. The notion of composition of substitutions in Lambdasub and the problems it raises when attempting to prove PSN are discussed.
We then exploit similarities between Lambdasub and the lambdalxr calculus of Kesner and Lengrand to present a translation from Lambdasub to a modified version of lambdalxr. We show that reduction in the former may be simulated in the latter which leads to a clearer proof of PSN for Lambdasub.
Bigraphical Reactive Systems have been proposed as a meta model for global ubiquitous computing generalising process calculi for mobility such as the pi-calculus and the Mobile Ambients calculus as well as graphical models for concurrency such as Petri Nets. We investigate in this paper how Bigraphical Reactive Systems represented as Reactive XML can be used to provide a formal semantics as well as an extensible and mobile platform independent execution format for XML based business process and workflow description languages such as BPEL and XPDL. We propose to extend the formalism with primitives for XPath evaluation and higher-order reaction rules to allow for a very direct and succinct semantics.
We analyze the matching problem for bigraphs. In particular, we present a sound and complete inductive characterization of matching of binding bigraphs. Our results pave the way for a provably correct matching algorithm, as needed for an implementation of bigraphical reactive systems.
We investigate sorting or typing for Leifer and Milner's reactive systems. We focus on transferring congruence properties for bisimulations from unsorted tosorted systems. Technically, we give a general definition of sorting; we adapt Jensen's work on the transfer of congruence properties to this general definition; we construct a predicate sorting, which, for any decomposible predicate P filters out agents not satisfying P; we prove that the predicatesorting preserves congruence properties and that it suitably retains dynamics; and finally, we show how the predicate sortings can be used to achieve context-aware reaction.
Extending Milners work on pure bigraphs, we axiomatize static congruence for binding bigraphs and prove that the theory generated is complete. In doing so, we also define a normal form for binding bigraphs, and prove that the four forms are unique up to certain isomorphisms. Compared with the axioms stated by Milner for pure bigraphs, we have extended the set with 5 axioms concerned with binding; and as our ions have names on both faces, we have two axioms - handling inner and outer renaming. The remaining axioms are transfered straightforwardly.
To gain familiarity with bigraphs and to investigate their modeling capabilities, we model a switch, finite automata, the game of ``life'', combinatory logic, term unification and an event-driven system as bigraphical reactive systems.
We present a refinement, suggested by Jensen and Milner under the term kind, on the pure place graphs in bigraph theory. We duly name the result kind place graphs. This refinement generalises the notion of atomic and non-atomic controls, allowing a control to contain a subset of the set of controls. We show that this variation has relative pushouts. We classify its idem pushouts and define the static theory for the variation. We then combine kind place graphs with pure link graphs in the usual way to achieve kind bigraphs and we reason about their static theory. Next, we develop a new useful link-sorting, named tile-sorting, for our purposes. Finally, we represent a sub-s-category of kind bigraphs, the fitting kind bigraphs, as a useful place-sorting and use known results to derive a dynamic behaviour for these bigraphs.
XML-centric models of computation have been proposed as an answer to the demand for interoperability, heterogeneity and openness in coordination models. We present a prototype implementation of an open XML-centric coordination middleware called Distributed Reactive XML. The middleware has as theoretical foundation a general extendable, distributed process calculus inspired by the theory of Bigraphical Reactive Systems. The calculus is extendable just as XML is extendable, in that its signature and reaction rules are not fixed. It is distributed by allowing both the state of processes as well as the set of eaction rules to be distributed (or partly shared) between different clients. The calculus is implemented by representing process terms as XML documents stored in a value-oriented, peer-to-peer XML Store and reaction rules as XML transformations performed by the clients. The formalism does not require that only process terms are stored-inside process terms one may store application specific data as well. XML Store provides transparent sharing of process terms between all participating peers. Conflicts between concurrent reaction rules are handled by an optimistic concurrency control. The implementation thus provides an open XML-based coordination middleware with a formal foundation that encompasses both the shared data, processes and reaction rules.
Bigraphs are graphs whose nodes may be nested, representing locality, independently of the edges connecting them. They may be equipped with reaction rules, forming a bigraphical reactive system (Brs) in which bigraphs can reconfigure themselves. Brss aim to unify process calculi, and to model applications -such as pervasive computing- where locality and mobility are prominent. The paper is devoted to the theory of pure bigraphs, which underlie various more refined forms. It begins by developing a more abstract structure, a wide reactive system Wrs, of which a Brs is an instance; in this context, labelled transitions are defined in such a way that the induced bisimilarity is a congruence.This work is then specialised to Brss, whose graphical structure allows many refinements of the dynamic theory. Elsewhere it is shown that behavioural analysis for Petri nets, pi-calculus and mobile ambients can all be recovered in the uniform framework of bigraphs. The latter part of the paper emphasizes the parts of bigraphical theory that are common to these applications, especially the treatment of dynamics via labelled transitions. As a running example, the theory is applied to finite pure CCS, whose resulting transition system and bisimilarity are analysed in detail.
The paper also discusses briefly the use of bigraphs to model both pervasive computing and biological systems.
As part of ongoing work on evaluating Milner's bigraphical reactive systems, we investigate bigraphical models of context-aware systems, a facet of ubiquitous computing. We find that naively encoding such systems in bigraphs is somewhat awkward; and we propose a more sophisticated modeling technique, introducing plato-graphical models, alleviating this awkwardness. We argue that such models are useful for simulation and point out that for reasoning about such bigraphical models, the bisimilarity inherent to bigraphical reactive systems is not enough in itself; an equivalence between the bigraphical reactive systems themselves is also needed.
Bigraphs have been introduced with the aim to provide a topographical meta-model for mobile, distributed agents that can manipulate their own linkages and nested locations, generalising both characteristics of the pi-calculus and the Mobile Ambients calculus. We give the first bigraphical presentation of a non-linear, higher-order process calculus with nested locations, non-linear active process mobility, and local names, the calculus of Higher-Order Mobile Embedded Resources (Homer). The presentation is based on Milner's recent presentation of the lambda-calculus in local bigraphs. The combination of non-linear active process mobility and local names requires a new definition of parametric reaction rules and a representation of the location of names. We suggest localised bigraphs as a generalisation of local bigraphs in which links can be further localised.
XML-centric models of computation have been proposed as an answer to the demand for interoperability, heterogeneity and openness in coordination models.Recently, Bigraphical reactive systems has been introduced as a theoretical meta-model for reactive systems with semi-structured state. We present an XML representation of bigraphical reactive systems called Reactive XML. It may be seen as an open, XML-centric model of computation with a solid theoretical foundation given by the theory of bigraphical reactive systems. In particular, the theory provides a formal denotation of composition and general transformations of XML documents with links. On the other hand, Reactive XML provides a concrete understanding of the theoretical model of bigraphical reactive systems. We report on a prototype for Reactive XML, describing how Reactive XML reactions can be carried out in praxis. In particular, we describe how the abstract notion of evaluation contexts may be represented concretely (and generalised) by XPath expressions. The prototype is currently being extended to a distributed setting, ultimately allowing distributed XML-centric applications to coordinate through computations on shared XML data.
The previous definition of binding bigraphs is generalised so that local names may be located in more than one region, allowing more succinct and flexible presentation of bigraphical reactive systems. This report defines the generalisation, verifies that it retains relative pushouts, and introduces a new notion of bigraph extension; this admits a wider class of parametric reaction rules. Extension is shown to be well-behaved algebraically; one consequence is that, as in the original definition of bigraphs, discrete parameters are sufficient to generate all reactions.
A framework is defined within which reactive systems can be studied formally. The framework is based upon s-categories, a new variety of categories, within which reactive systems can be set up in such a way that labelled transition systems can be uniformly extracted. These lead in turn to behavioural preorders and equivalences, such as the failures preorder (treated elsewhere) and bisimilarity, which are guaranteed to be congruential. The theory rests upon the notion of relative pushout previously introduced by the authors. The framework is applied to a particular graphical model known as link graphs, which encompasses a variety of calculi for mobile distributed processes. The specific theory of link graphs is developed. It is then applied to an established calculus, namely condition-event Petri nets. In particular, a labelled transition system is derived for condition-event nets, corresponding to a natural notion of observable actions in Petri net theory. The transition system yields a congruential bisimilarity coinciding with one derived directly from the observable actions. This yields a calibration of the general theory of reactive systems and link graphs against known specific theories.
A bigraphical reactive system (BRS) involves bigraphs, in which the nesting of nodes represents locality, independently of the edges connecting them; it also allows bigraphs to reconfigure themselves. BRSs aim to provide a uniform way to model spatially distributed systems that both compute and communicate. In this memorandum we develop their static and dynamic theory.In Part I we illustrate bigraphs in action, and show how they correspond to to process calculi. We then develop the abstract (non-graphical) notion of wide reactive system (WRS), of which BRSs are an instance. Starting from reaction rules -often called rewriting rules- we use the RPO theory of Leifer and Milner to derive (labelled) transition systems for WRSs, in a way that leads automatically to behavioural congruences.
In Part II we develop bigraphs and BRSs formally. The theory is based directly on graphs, not on syntax. Key results in the static theory are that sufficient RPOs exist (enabling the results of Part I to be applied), that parallel combinators familiar from process calculi may be defined, and that a complete algebraic theory exists at least for pure bigraphs (those without binding). Key aspects in the dynamic theory -the BRSs- are the definition of parametric reaction rules that may replicate or discard parameters, and the full application of the behavioural theory of Part I.
In Part III we introduce a special class: the simple BRSs. These admit encodings of many process calculi, including the pi-calculus and the ambient calculus. A still narrower class, the basic BRSs, admits an easy characterisation of our derived transition systems. We exploit this in a case study for an asynchronous pi- calculus. We show that structural congruence of process terms corresponds to equality of the representing bigraphs, and that classical strong bisimilarity corresponds to bisimilarity of bigraphs. At the end, we explore several directions for further work.
This paper axiomatises the structure of bigraphs, and proves that the resulting theory is complete. Bigraphs are graphs with double structure, representing locality and connectivity. They have been shown to represent dynamic theories for the pi-calculus, mobile ambients and Petri nets, in a way that is faithful to each of those models of discrete behaviour. While the main purpose of bigraphs is to understand mobile systems, a prerequisite for this understanding is a well-behaved theory of the structure of states in such systems. The algebra of bigraph structure is surprisingly simple, as the paper demonstrates; this is because bigraphs treat locality and connectivity orthogonally.
A bigraphical reactive system (BRS) involves bigraphs, in which the nesting of nodes represents locality, independently of the edges connecting them; it also allows bigraphs to reconfigure themselves. BRSs aim to provide a uniform way to model spatially distributed systems that both compute and communicate. In this memorandum we develop their static and dynamic theory.In Part I we illustrate bigraphs in action, and show how they correspond to to process calculi. We then develop the abstract (non-graphical) notion of wide reactive system (WRS), of which BRSs are an instance. Starting from reaction rules -often called rewriting rules- we use the RPO theory of Leifer and Milner to derive (labelled) transition systems for WRSs, in a way that leads automatically to behavioural congruences.
In Part II we develop bigraphs and BRSs formally. The theory is based directly on graphs, not on syntax. Key results in the static theory are that sufficient RPOs exist (enabling the results of Part I to be applied), that parallel combinators familiar from process calculi may be defined, and that a complete algebraic theory exists at least for pure bigraphs (those without binding). Key aspects in the dynamic theory -the BRSs- are the definition of parametric reaction rules that may replicate or discard parameters, and the full application of the behavioural theory of Part I.
In Part III we introduce a special class: the simple BRSs. These admit encodings of many process calculi, including the pi-calculus and the ambient calculus. A still narrower class, the basic BRSs, admits an easy characterisation of our derived transition systems. We exploit this in a case study for an asynchronous pi- calculus. We show that structural congruence of process terms corresponds to equality of the representing bigraphs, and that classical strong bisimilarity corresponds to bisimilarity of bigraphs. At the end, we explore several directions for further work.
The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics to use reaction rules -i.e. unlabelled transition rules- together with a structural congruence. This form, which I call a reactive system, is highly expressive but is limited in an important way: LTSs lead more naturally to operational equivalences and preorders. This paper shows how to synthesise an LTS for a wide range of reactive systems. A label for an agent (process) `a' is defined to be any context `F' which intuitively is just large enough so that the agent `Fa' (`a' in context `F') is able to perform a reaction step. The key contribution of my work is the precise definition of ``just large enough'' in terms of the categorical notion of relative pushout (RPO). I then prove that several operational equivalences and preorders (strong bisimulation, weak bisimulation, the traces preorder, and the failures preorder) are congruences when sufficient RPOs exist.
This paper is the second in a series of two. It relies on its companion, Part 1, to motivate the central problem addressed by the series, namely: how to synthesise labelled transitions for reactive systems and how to prove congruence results for operational equivalences and preorders defined above those transitions. The purpose of this paper is (i) to show that the hypotheses required of functorial reactive systems from Part 1, for example the sliding properties of IPO (idem pushout) squares, are indeed satisfied for functors of a general form; (ii) to illustrate an example of a functorial reactive system based on Milner's action calculi, which satisfy the RPO (relative pushout) hypothesis required in the proofs of congruence from Part 1.
A notion of bigraph is proposed as the basis for a model of mobile interaction. A bigraph consists of two independent structures: a topograph representing locality and a monograph representing connectivity. Bigraphs are equipped with reaction rules to form bigraphical reactive systems (BRSs), which include versions of the pi-calculus and the ambient calculus. Bigraphs are shown to be a special case of a more abstract notion, wide reactive systems (WRSs), not assuming any particular graphical or other structure but equipped with a notion of width, which expresses that agents, contexts and reactions may all be widely distributed entities.A behavioural theory is established for WRSs using the categorical notion of relative pushout; it allows labelled transition systems to be derived uniformly, in such a way that familiar behavioural preorders and equivalences, in particular bisimilarity, are congruential under certain conditions. Then the theory of bigraphs is developed, and they are shown to meet these conditions. It is shown that, using certain functors, other WRSs which meet the conditions may also be derived; these may, for example, be forms of BRS with additional structure.
Simple examples of bigraphical systems are discussed; the theory is developed in a number of ways in preparation for deeper application studies.