Abstract 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.

Robin Milner; Discussant of Response to the Computer Journal Lecture by Morris Sloman, The Computer Journal, Volume 53, Issue 7, 1 September 2010, Pages 1128, h

Pervasive or ubiquitous computing has become an aspiration of the computing community in the last 15 years. Its vision, pioneered by Mark Weiser [1], is that populations of computing entities—hardware and software—will become an effective part of our environment, performing tasks that support our broad purposes without our continual direction, thus allowing us to be largely unaware of them. The vision arises because the technology begins to lie within our grasp. This simply stated aspiration arouses questions ranging across computer science and beyond. Here are a few of them. Social questions: what ubiquitous computing systems (UCSs) do people want or need, and how will they change people’s behaviour? Technological questions: how will the hardware entities—the sensors and effectors whose cooperation represents such a system—acquire power, and by what medium do they communicate? Engineering questions: for the populations and subpopulations—including software agents—that make up a system, what design principles should be adopted at each order of magnitude, to ensure dependable performance? Foundational questions: what concepts are needed to specify and describe pervasive systems, their subsystems and their interaction?

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.

What are the major research challenges that face the world of computing today? Are there any of them that match the grandeur of well-known challenges in other branches of science? This article is a report on an exercise by the Computing Research Community in the UK to answer these questions, and includes a summary of the outcomes of a BCS-sponsored conference held in Newcastle-upon-Tyne from 29 to 31 March this year.

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 -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.

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 λ-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 λ-calculus, this LTS and its bisimilarity agree closely with the standard.

Abstract. Action calculi, which generalise process calculi such as Petri nets, π-calculusand ambient calculus, have been presented in terms ofaction graphs. We here offerlinearaction graphs as a primitive basis for action calculi. This paper presents the category of embeddings of undirected linear action graphs without nesting, using a novel form of graphical reasoning which simplifies some otherwise complex manipulations in regular algebra. The results are adapted in a few lines to directed graphs. This work is part of a long-term search for a uniform behavioural theory for process calculi.

No abstract available.

'Action calculi' are a class of action structures with added structure. Each action calculus AC(/spl Kscr/) is determined by a set /spl Kscr/ of controls, equipped with reaction rules; calculi such as Petri nets, the typed /spl lambda/-calculus and the /spl pi/-calculus are obtained by varying /spl Kscr/. This paper defines for each /spl Kscr/ a category CS(/spl Kscr/), characterized by equational axioms, of action structures with added structure; they are called 'control structures' and provide models of the calculus AC(/spl Kscr/), which is initial in the category. The 'surface' of an action is defined; this is an abstract correlate of the syntactic notion of 'free name'. Three equational characterizations of the surface are found to be equivalent. This permits a non-syntactic treatment of the linkage among the components of an interactive system. Finally, control structures and their morphisms offer a means of classifying the variety of dynamic disciplines in models of concurrency, such as the mobility present in the /spl pi/-calculus but absent in other calculi.

We present a set of concurrency primitives for Standard ML. We define these by giving the transitional semantics of a simple language. We prove that our semantics preserves the expected behaviour of sequential programs. We also show that we can define stores as processes, such that the representation has the same behaviour as a direct definition. These proofs are the first steps towards integrating our semantics with the full definition of Standard ML.

This paper exhibits accurate encodings of the λ-calculus in the π-calculus. The former is canonical for calculation with functions, while the latter is a recent step (Milner et al. 1989) towards a canonical treatment of concurrent processes. With quite simple encodings, two λ-calculus reduction strategies are simulated very closely; each reduction in λ-calculus is mimicked by a short sequence of reductions in π-calculus. Abramsky's precongruence of applicative bisimulation (Abramsky 1989) over λ-calculus is compared with that induced by the encoding of the lazy λ-calculus into π-calculus; a similar comparison is made for call-by-value λ-calculus.

Since a nondeterministic and concurrent program may, in general, communicate repeatedly with its environment, its meaning cannot be presented naturally as an input/output function (as is often done in the denotational approach to semantics). In this paper, an alternative is put forth. First, a definition is given of what it is for two programs or program parts to be equivalent for all observers; then two program parts are said to be observation congruent if they are, in all program contexts, equivalent. The behavior of a program part, that is, its meaning, is defined to be its observation congruence class. The paper demonstrates, for a sequence of simple languages expressing finite (terminating) behaviors, that in each case observation congruence can be axiomatized algebraically. Moreover, with the addition of recursion and another simple extension, the algebraic language described here becomes a calculus for writing and specifying concurrent programs and for proving their properties.

An algebraic calculus of asynchronous parallel computation, called CCS (Calculus of Communicating Systems), was developed in [HM,Mil 1]. CCS can express both the semantics of parallel programming languages and the behaviour of data structures (mailbox, random access memory, buffer) which serve as interfaces between independent agents. The primitive notion is 'handshake' communication. The emphasis is upon (i) synthesis from components and (ii) extensionality (meaning = observable behaviour), in contrast with Petri's Net theory which emphasizes causal independence.

the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of its publication and date appear, and notice is given

A mathemaucal model of concurrent computaUon is presented Starting from synchronized com-mumcaUon as the only pnmitwe notion, a process is defined as a set of communication capabdmes The domain of processes is budt using the weak powerdomam construction of Smyth, which evolved from that of Plotkm A minimal set of operaUons for composing processes is defined These operations suggest a corresponding mmlmal syntax--the language offlowgraphs--m which to specify these composluons The concept offlow algebra is defined, processes and flowgraphs are examples of flow algebras Elsewhere it will be shown that flowgraphs are free (over a set of generators) in the category of flow algebras, here it is shown that processes are a flow algebra, and therefore constitute a suitable semantics for flowgraphs However, we emphasize that the nouon of flowgraph evolved from the notion of process and not the reverse

An algebra G offlowgraphs or nets is presented It is shown to be a free algebra of a simple equatmnal system F, which is called the laws of flow This holds both for the algebra of fimte nets, and for the algebra of fimte or mfimte nets m which certain mfimte nets may be described by recursmn equatmns To demonstrate this fact, some results concerning categories of continuous algebras, which are explicit or lmphctt m the work of the ADJ group, are presented m a self-contained form.It follows that the algebra of processes (presented m a compamon paper [10]), which satisfies the laws of flow F, is a statable semanUcs for flowgraphs There are, however, many other mterpretatmns of nets, some of wMch wdl be studied m subsequent papers.This paper concludes wtth some simple examples of mfimte nets and informally discusses their possible interpretation KEY WORDS AND PHRASES.concurrency, paraUehsm, process, semanttcs, mmal algebraic semantics, commumeating processes, flow dmgrams, nondetermmtsm CR CATEGORIES 4 22, 4 32, 5 21, 5 24 "You could get an mfimte number of wires m this junction box, but we don't usually go that far m practice" --Man from London Electricity Board, 1959

Article Free Access Share on A Metalanguage for interactive proof in LCF Authors: M. Gordon University of Edinburgh University of EdinburghView Profile , R. Milner University of Edinburgh University of EdinburghView Profile , L. Morris Syracuse University Syracuse UniversityView Profile , M. Newey Australian National University Australian National UniversityView Profile , C. Wadsworth University of Edinburgh University of EdinburghView Profile Authors Info & Claims POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1978Pages 119–130https://doi.org/10.1145/512760.512773Published:01 January 1978Publication History 55citation684DownloadsMetricsTotal Citations55Total Downloads684Last 12 Months96Last 6 weeks5 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

DASH (Dynamic ALGOL String Handling) is a set of procedures designed to extend ALGOL to the expression of non-numerical or partly non-numerical algorithms for which it is normally unsuited.