We analyze the matching problem for bigraphs. In particular, we present a sound and complete inductive characterization of matching in bigraphs with binding. Our results yield a specification for a provably correct matching algorithm, as needed by our prototype tool implementing bigraphical reactive systems.

This paper demonstrates that a wide range of the CSP operators, in particular parallel composition, hiding, general choice, interleaving, and the non deterministic OR, can be represented by confluent unfolding to a normal form. The relevant normal form is an enrichment of the CSP choice construction by the inclusion of non -determinism and silent actions. It is demonstrated that the majority of the equational laws presented by Hoare for these operators are valid not only for the failures equivalence but even for strong bisimilarity. This work is a prelude to embedding CSP in the bigraph model, a recent generic model for ubiquitous computing in which other process calculi have been faithfully embedded. The authors

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 optimize their behavior. 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 self-contained mathematically and is designed to be learned from: examples and exercises abound, solutions for the latter are provided.

This volume contains the proceedings of the 20th Conference on Concurrency Theory (CONCUR 2009), held in Bologna, September 1–4, 2009. The purpose of the CONCUR conference is to bring together researc

Computer science is no longer just a technology--for nearly all of us, it has become a way of life. Whether we spend our days surfing the Internet, or merely use an automatic teller machine on occasion, computers have affected our lives. This collection of sixteen original essays by distinguished computer scientists celebrates the achievements of computer science research, and speculates about the unsolved problems in the field. Various essays address artificial intelligence, parallel programming, global information systems, and a host of other relevant topics. The book shows that long-term research in computer science is crucial and must not be driven solely by commercial considerations. The authors expose the difficult aspects of their topics in clear terms, and illustrate that computer science is now a full-fledged and growing intellectual discipline.

The concept of process has become increasingly important in computer science in the last three decades and more. Yet we still don’t agree on what a process is . We probably agree that it should be an equivalence class of interactive agents, perhaps concur re t, perhaps non-deterministic. Whatever they are, processes play different roles; these range f rom specifying the interactive programs that we design, to discrete modelling of naturally occurrin g behaviour (as in biology). In between lie systems that we partially design but are embedded in a nat ural environment (e.g. ubiquitous systems) or in environments such as the internet or washing mach ines or cars, designed by engineers of varying disciplines. Thus informatic processes have become increasingly releva nt outside computer science as it was three decades ago, when both CSP and CCS were first launched. I n the preface to my book Communication and Concurrency (1989) I said

Software science has always dealt with models of computatio n that associate meaning with syntactical construction. The link between software science and software engineering has for many year s been tenuous. A recent initiative,model-driven engineering(MDE), has begun to emphasize the role of models in software construction. Hi therto, the notions of ’model’ entertained by software scientists and e gineers have differed, the former emphasizing meaning and the latter emp hasizing toolbased engineering practice. This essay finds the two approac hes consistent, and proposes to integrate them in a framework that allo ws one model to explainanother, in a sense that includes both implementation and va lidation. This essay is dedicated in admiration to the memory of Gilles Kahn, a friend and guide for thirty-five years. I have been struck by the confidence and warmth expressed towards him by the many French colleagues whom he guided. As a no n-Frenchman I can also testify that colleagues in other countries have fel t th same. I begin by recalling two events separated by thirty years; on e private to him and me, one public in the UK. I met Gilles in Stanford University in 19 72, when he was studying for the PhD degree—which, I came to believe, he found unnecess ary to acquire. His study was, I think, thwarted by the misunderstanding of othe rs. I was working on two different things: on computer-assisted reasoning in a logi c f Dana Scott based upon domain theory, which inspired me, and on models of interacti on—which I believed would grow steadily in importance (as indeed they have). The re was hope to unite the two. Yet it was hard to relate domain theory to the non-det erminism inherent in interactive processes. I remember, but not in detail, a disc ussion of this connection with Gilles. The main thing I remember is that he ignited. He h ad got the idea of the domain of streams which, developed jointly with David Ma cQueen, became one of the most famous papers in informatics; a model of determinis tic processes linked by streams of data. The public event, in 2002, was the launching workshop of the U K Exercise in Grand Challenges for Computing Research. It identified eigh t or so Grand Challenge topics that now act as a focus for collaborative research; pa rt of their effect is to unite researchers who would otherwise never have communicated. B efore the workshop we

Bigraphs are a candidate model that aims to provide a theoretical platform for ubiquitous computing systems. This short paper summarises the categories, and the functors between them, that represent the structure of that theory.

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.

I am delighted to be able to share in celebrating Ugo's birthday, if not with a formal paper then at least with some loosely-knit philosophical ideas.I have worked on ideas similar to Ugo's for most of our careers. Ugo had much to do with the stream of expert Italians, many now well-known, who travelled from the warmth of Pisa to the romantic but cooler climate of Edinburgh, often to launch their careers with a PhD there. Going further back, I remember with excitement the meeting on parallel processes at Pisa in 1973, organised I believe by Ugo, the first concurrency conference I ever attended.

How can you hope to understand a ubiquitous system, whether you are a user embedded in it, an engineer building it or a scientist analysing it? Never before have such huge systems been envisaged. We have to lift the scientific status of informatics to provide this understanding. It can only be done

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.

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.

article Free AccessElements of interaction: Turing award lecture Author: Robin Milner View Profile Authors Info & Claims Communications of the ACMVolume 36Issue 1Jan. 1993 pp 78–89https://doi.org/10.1145/151233.151240Published:01 January 1993Publication History 187citation5,616DownloadsMetricsTotal Citations187Total Downloads5,616Last 12 Months224Last 6 weeks18 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

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.