technicalReports.bib
@TECHREPORT{GrohmannMiculan:2006:TRDirectedBigraphs,
AUTHOR = {Davide Grohmann and Marino Miculan},
TITLE = {Directed Bigraphs: Theory and Applications},
INSTITUTION = {University of Udine},
YEAR = 2006,
ABSTRACT = {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-Soboci{\'n}ski'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-
Soboci{\'n}ski 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.},
NUMBER = {UDMI/12/2006/RR},
ADDRESS = {},
MONTH = DEC,
PDF = {http://users.dimi.uniud.it/~marino.miculan/Papers/UDMI122006.pdf}
}
@TECHREPORT{Milner:2001:BRSBasicTheory,
AUTHOR = {Robin Milner},
TITLE = {Bigraphical reactive systems: basic theory},
INSTITUTION = {University of Cambridge, Computer Laboratory},
YEAR = 2001,
ABSTRACT = {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.},
NUMBER = 523,
ADDRESS = {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom},
MONTH = SEP,
PDF = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-523.pdf}
}
@TECHREPORT{Milner:2003:BigraphsMobileProcesses,
AUTHOR = {Ole H{\o}gh Jensen and Robin Milner},
TITLE = {Bigraphs and mobile processes (revised)},
INSTITUTION = {University of Cambridge, Computer Laboratory},
YEAR = 2003,
ABSTRACT = {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. },
NUMBER = 570,
ADDRESS = {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom},
MONTH = JUL,
PDF = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-570.pdf}
}
@TECHREPORT{Milner:2004:BigraphsRevised,
AUTHOR = {Ole H{\o}gh Jensen and Robin Milner},
TITLE = {Bigraphs and mobile processes (revised)},
INSTITUTION = {University of Cambridge, Computer Laboratory},
YEAR = 2004,
ABSTRACT = {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.},
NUMBER = 580,
ADDRESS = {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom},
MONTH = FEB,
PDF = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-580.pdf}
}
@TECHREPORT{Milner:2004:AxiomsForBigraphicalStruct,
AUTHOR = {Robin Milner},
TITLE = {Axioms for bigraphical structure},
INSTITUTION = {University of Cambridge, Computer Laboratory},
YEAR = 2004,
ABSTRACT = {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.},
NUMBER = 581,
ADDRESS = {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom},
MONTH = FEB,
PDF = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-581.pdf}
}
@TECHREPORT{Milner:2004:BigraphsNamesMultiLoc,
AUTHOR = {Robin Milner},
TITLE = {Bigraphs whose names have multiple locality},
INSTITUTION = {University of Cambridge, Computer Laboratory},
YEAR = 2004,
ABSTRACT = {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.},
NUMBER = 603,
ADDRESS = {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom},
MONTH = SEP,
PDF = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-603.pdf}
}
@TECHREPORT{Milner:2005:PureBigraphs,
AUTHOR = {Robin Milner},
TITLE = {Pure bigraphs},
INSTITUTION = {University of Cambridge, Computer Laboratory},
YEAR = 2005,
ABSTRACT = {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.},
NUMBER = 614,
ADDRESS = {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom},
MONTH = JAN,
PDF = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-614.pdf}
}
@TECHREPORT{Elsborg:2006:Thesis,
AUTHOR = {Ebbe Elsborg},
TITLE = {Bigraphical Location Models},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2006,
ABSTRACT = {In this progress report we begin evaluation of how
well-suited H{\o}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.},
NUMBER = 94,
ADDRESS = {Rued Langgaards Vej 7, DK-2300 Copenhagen V},
MONTH = SEP,
PDF = {http://www.itu.dk/people/elsborg/ITU-TR-2006-94.pdf}
}
@TECHREPORT{HildebrandtEtAl:2006:TRBPEL,
TITLE = {Formalising Business Process Execution with Bigraphs
and {R}eactive {XML}},
AUTHOR = {Thomas Hildebrandt and Henning Niss and Martin Olsen},
NUMBER = {TR-2006-85},
INSTITUTION = {IT University of Copenhagen},
MONTH = JUN,
YEAR = 2006,
PDF = {http://www.itu.dk/people/hniss/pubs/ITU-TR-2006-85.pdf},
ABSTRACT = {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.}
}
@TECHREPORT{BirkedalEtAl:2006:TRMatchingBigraphs,
AUTHOR = {Lars Birkedal and Troels Christoffer Damgaard and
Arne John Glenstrup and Robin Milner},
TITLE = {Matching of Bigraphs},
INSTITUTION = {IT University of Copenhagen},
NUMBER = {TR-2006-88},
YEAR = 2006,
MONTH = JUN,
PDF = {http://www.itu.dk/docadm/docs/1258.pdf.gz},
ABSTRACT = {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.}
}
@TECHREPORT{BirkedalEtAl:2006:TRsortings,
AUTHOR = {Lars Birkedal and S{\o}ren Debois and Thomas Hildebrandt},
TITLE = {Sortings for reactive systems},
INSTITUTION = {IT University of Copenhagen},
NUMBER = {TR-2006-84},
MONTH = MAR,
YEAR = 2006,
PDF = {http://www.itu.dk/people/debois/pubs/sortings.pdf},
ABSTRACT = {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.}
}
@TECHREPORT{BirkedalEtAl:2005:BigraphicalModels,
AUTHOR = {Lars Birkedal and S{\o}ren Debois and Ebbe Elsborg and Thomas
Hildebrandt and Henning Niss},
TITLE = {Bigraphical Models of Context-Aware Systems},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2005,
NUMBER = {TR-2005-74},
PDF = {http://www.itu.dk/docadm/docs/1069.pdf.gz},
ABSTRACT = {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.}
}
@TECHREPORT{BundgaardHildebrandt:2005:SemanticsHigherOrder,
AUTHOR = {Mikkel Bundgaard and Thomas Hildebrandt},
TITLE = {Bigraphical Semantics of Higher-Order Mobile Embedded
Resources with Local Names},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2005,
NUMBER = {TR-2005-70},
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/ITU-TR-2005-70.pdf},
ABSTRACT = {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.}
}
@TECHREPORT{DamgaardBirkedal:2005:TRAxiomatizingBindingBigraphs,
AUTHOR = {Troels Christoffer Damgaard and Lars Birkedal},
TITLE = {Axiomatizing Binding Bigraphs (revised)},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2005,
NUMBER = {TR-2005-71},
MONTH = NOV,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/ITU-TR-2005-71.pdf},
ABSTRACT = {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.}
}
@TECHREPORT{DeboisDamgaard:2005:BigraphsExample,
AUTHOR = {S{\o}ren Debois and Troels Christoffer Damgaard},
TITLE = {Bigraphs by Example},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2005,
NUMBER = {TR-2005-61},
MONTH = OCT,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/ITU-TR-2005-61.pdf},
ABSTRACT = {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.}
}
@TECHREPORT{GlenstrupEtAl:2006:BDNFBasedMatchingBigraphs,
AUTHOR = {Arne John Glenstrup and Troels Christoffer Damgaard
and Lars Birkedal and Martin Elsman},
TITLE = {{BDNF}-Based Matching of Bigraphs},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2006,
NUMBER = {TR-2006-93},
MONTH = OCT,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/ITU-TR-2006-93.pdf},
ABSTRACT = {We analyze the matching problem for bigraphs. In
particular, we present an axiomatization of the
static theory of \emph{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.}
}
@TECHREPORT{HildebrandtWinther:2005:BigraphsReactiveXML,
AUTHOR = {Thomas Hildebrandt and Jacob Wahl Winther},
TITLE = {Bigraphs and (Reactive) {XML}},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2005,
NUMBER = {TR-2005-56},
MONTH = JAN,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/ITU-TR-2005-56.pdf},
ABSTRACT = {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
\emph{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.}
}
@TECHREPORT{HildebrandtEtAl:2005:DistributedReactiveXMLCoordMiddleware,
AUTHOR = {Thomas Hildebrandt and Henning Niss and Martin Olsen
and Jacob Wahl Winter},
TITLE = {Distributed {R}eactive {XML}---an {XML}-centric
coordination middleware},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2005,
NUMBER = {TR-2005-62},
MONTH = FEB,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/ITU-TR-2005-62.pdf},
ABSTRACT = {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.}
}
@TECHREPORT{OConchuir:2006:LambdaSub,
AUTHOR = {\'{O} Conch\'{u}ir, Shane},
TITLE = {{$\Lambda$}-sub as an explicit substitution calculus},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2006,
NUMBER = {TR-2006-95},
MONTH = SEP,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/ITU-TR-2006-95.pdf},
ABSTRACT = {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 ($\Lambda$sub) 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
$\Lambda$sub and the calculus $\lambda$xgc of Bloo and Rose. The
notion of composition of substitutions in $\Lambda$sub and the
problems it raises when attempting to prove PSN are discussed.
We then exploit similarities between $\Lambda$sub and the
$lambda$lxr calculus of Kesner and Lengrand to present a translation
from $\Lambda$sub to a modified version of $\lambda$lxr. We show
that reduction in the former may be simulated in the latter which
leads to a clearer proof of PSN for $\Lambda$sub.}
}
@TECHREPORT{OConchuir:2005:KindBigraphs,
AUTHOR = {\'{O} Conch\'{u}ir, Shane},
TITLE = {Kind bigraphs - Static theory},
INSTITUTION = {Trinity College Dublin, Computer Science Department},
YEAR = 2005,
NUMBER = {TCD-CS-2005-36},
MONTH = MAY,
PDF = {http://www.cs.tcd.ie/Shane.OConchuir/kbgR.pdf},
ABSTRACT = {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.}
}
@TECHREPORT{LeiferMilner:2004:LinkGraphsPetriNets,
AUTHOR = {James J. Leifer and Robin Milner},
TITLE = {Transition systems, link graphs and Petri nets},
INSTITUTION = {University of Cambridge, Computer Laboratory},
YEAR = 2004,
ABSTRACT = {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.},
NUMBER = 598,
ADDRESS = {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom},
MONTH = AUG,
PDF = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-598.pdf}
}
@TECHREPORT{Leifer:2002:SynthesisingLTSPart1,
AUTHOR = {James J. Leifer},
TITLE = {Synthesising labelled transitions and operational
congruences in reactive systems, part 1},
INSTITUTION = {INRIA Rocquencourt},
YEAR = 2002,
NUMBER = {RR-4394},
OPTADDRESS = {},
ABSTRACT = {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.}
}
@TECHREPORT{Leifer:2002:SynthesisingLTSPart2,
AUTHOR = {James J. Leifer},
TITLE = {Synthesising labelled transitions and operational
congruences in reactive systems, part 2},
INSTITUTION = {INRIA Rocquencourt},
YEAR = {2002},
NUMBER = {RR-4395},
OPTADDRESS = {},
ABSTRACT = {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.}
}
@TECHREPORT{Elsborg:08:TypeSystemsForBigraphsTR,
AUTHOR = {Ebbe Elsborg and Thomas Hildebrandt and Davide Sangiorgi},
TITLE = {Type Systems for Bigraphs},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2008,
NUMBER = {TR-2008-110},
MONTH = OCT,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/2008/ITU-TR-2008-110.pdf},
ABSTRACT = {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. }
}
@TECHREPORT{Bundgaard:08:FormalizingWSBPELandHOinBPLTool,
AUTHOR = {Mikkel Bundgaard and Arne John Glenstrup and Thomas Hildebrandt and
Espen H\o{}jsgaard and Henning Niss},
TITLE = {Formalizing {WS-BPEL} and Higher Order Mobile Embedded Business
Processes in the Bigraphical Programming Languages ({BPL}) {Tool}},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2008,
NUMBER = {TR-2008-103},
MONTH = MAY,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/2008/ITU-TR-2008-103.pdf},
ABSTRACT = {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.}
}
@TECHREPORT{Birkedal:09:HOContextsViaGamesIntConstr,
AUTHOR = {Lars Birkedal and Mikkel Bundgaard and S{\o}ren Debois and Davide Grohmann and Thomas Hildebrandt},
TITLE = {Higher-order Contexts via Games and the {Int}-construction},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2009,
NUMBER = {TR-2009-117},
MONTH = JAN,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/2009/ITU-TR-2009-117.pdf},
ABSTRACT = {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.}
}
@TECHREPORT{Damgaard:08:ALanguageForTheCell,
AUTHOR = {Troels C. Damgaard and Vincent Danos and Jean Krivine},
TITLE = {A Language for the Cell},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2008,
NUMBER = {TR-2008-116},
MONTH = DEC,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/2008/ITU-TR-2008-116.pdf},
ABSTRACT = {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).}
}
@TECHREPORT{Damgaard:08:GenericLangBioSystBasedBigraphs,
AUTHOR = {Troels C. Damgaard and Jean Krivine},
TITLE = {A Generic Language for Biological Systems based on Bigraphs},
INSTITUTION = {IT University of Copenhagen},
YEAR = 2008,
NUMBER = {TR-2008-115},
MONTH = DEC,
PDF = {http://www1.itu.dk/graphics/ITU-library/Internet/Forskning/Technical_Reports/2008/ITU-TR-2008-115.pdf},
ABSTRACT = {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 \emph{bigraphical reactive systems}, due
to Milner et al., as a basis for developing
rule-based languages for molecular biology. We
describe a family of $\mathbf{B}^{\Sigma}_R$-calculi
sharing a small set of familiar operators and
operations, and provide them with a simple
operational semantics. We show that
$\mathbf{B}^{\Sigma}_R$-calculi and their reaction
semantics correspond to a version of bigraphical
reaction under \emph{non-aliasing} contexts and with
reaction rules extended to allow negative
side-conditions for the subset of bigraphs
corresponding to
$\mathbf{B}^{\Sigma}_R$-processes. Finally, to
illustrate the usage of $\mathbf{B}^{\Sigma}_R$, we
show that with non-aliasing semantics the
Kappa-calculus may be faithfully captured as a
$\mathbf{B}^{\Sigma}_R$-calculus. }
}
This file has been generated by
bibtex2html 1.52
Updated Mon Aug 31 11:31:24 CEST 2009