bigraphsbib.bib
@BOOK{Milner:09:SpaceAndMotionOfCommunicatingAgents,
AUTHOR = {Robin Milner},
TITLE = {The Space and Motion of Communicating Agents},
PUBLISHER = {Cambridge University Press},
YEAR = 2009,
ABSTRACT = {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.}
}
@INPROCEEDINGS{Grohmann:08:SecurityCryptAndDirectedBigraphs,
AUTHOR = {Davide Grohmann},
TITLE = {Security, Cryptography and Directed Bigraphs},
BOOKTITLE = {Proceedings of the 4th International Conference on
Graph Transformations (ICGT'08)},
PAGES = {487--489},
YEAR = 2008,
EDITOR = {Hartmut Ehrig and
Reiko Heckel and
Grzegorz Rozenberg and
Gabriele Taentzer},
VOLUME = {5214},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {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.}
}
@INPROCEEDINGS{GrohmannMiculan:2007:ReactSysOverDirectedBig,
AUTHOR = {Davide Grohmann and Marino Miculan},
TITLE = {Reactive Systems over Directed Bigraphs},
BOOKTITLE = {Proceedings of the 18th International Conference
on Concurrency Theory (CONCUR'07)},
EDITOR = {Lu\'{\i}s Caires and Vasco Thudichum Vasconcelos},
YEAR = 2007,
VOLUME = 4703,
PAGES = {380--394},
SERIES = {Lecture Notes in Computer Science},
OPTMONTH = {},
PUBLISHER = {Springer-Verlag},
PDF = {http://users.dimi.uniud.it/~marino.miculan/data/downloads/CONCUR07.pdf},
ABSTRACT = {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.}
}
@INPROCEEDINGS{GrohmannMiculan:2007:DirectedBigraphs,
AUTHOR = {Davide Grohmann and Marino Miculan},
TITLE = {Directed Bigraphs},
BOOKTITLE = {Proceedings of the 23rd Conference on the Mathematical
Foundations of Programming Semantics (MFPS'07)},
YEAR = 2007,
VOLUME = 173,
PAGES = {121--137},
SERIES = {Electronic Notes in Theoretical Computer Science},
OPTMONTH = {},
PUBLISHER = {Elsevier},
PDF = {http://users.dimi.uniud.it/~marino.miculan/data/downloads/MFPS07.pdf},
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. We give RPO and IPO
constructions for this model, 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.}
}
@INPROCEEDINGS{BirkedalEtAl:2006:MatchingBigraphs,
AUTHOR = {Lars Birkedal and Troels Christoffer Damgaard and
Arne John Glenstrup and Robin Milner},
TITLE = {Matching of Bigraphs},
BOOKTITLE = {Proceedings of Graph Transformation for
Verification and Concurrency Workshop (GT-VC'06)},
PAGES = {3--19},
YEAR = 2007,
VOLUME = 175,
NUMBER = 4,
SERIES = {Electronic Notes in Theoretical Computer Science},
MONTH = AUG,
PUBLISHER = {Elsevier},
PDF = {http://www.itu.dk/people/panic/Papers/BirkedalEtAl-2006-MatchingBigraphs.pdf},
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.}
}
@INPROCEEDINGS{BirkedalEtAl:2006:Sortings,
AUTHOR = {Lars Birkedal and S{\o}ren Debois and Thomas Hildebrandt},
TITLE = {Sortings for reactive systems},
BOOKTITLE = {Proceedings of the 17th International Conference
on Concurrency Theory (CONCUR'06)},
EDITOR = {Christel Baier and Holger Hermanns},
PAGES = {248--262},
YEAR = 2006,
SERIES = {Lecture Notes in Computer Science},
VOLUME = 4137,
MONTH = AUG,
PUBLISHER = {Springer-Verlag},
PDF = {http://www.itu.dk/people/birkedal/papers/sorrs-conf.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.}
}
@INPROCEEDINGS{HildeBrandtEtAl:2006:BPEL,
TITLE = {Formalising Business Process Execution with Bigraphs
and {R}eactive {XML}},
AUTHOR = {Thomas Hildebrandt and Henning Niss and Martin Olsen},
BOOKTITLE = {Proceedings of the 8th International
Conference on Coordination Models and Languages
(COORDINATION'06)},
SERIES = {Lecture Notes in Computer Science},
EDITOR = {Paolo Ciancarini and Herbert Wiklicky},
PUBLISHER = {Springer-Verlag},
MONTH = JAN,
VOLUME = 4038,
YEAR = 2006,
PAGES = {113--129},
PDF = {http://www.itu.dk/people/hniss/pubs/coordination2006.pdf},
URL = {http://dx.doi.org/10.1007/11767954_8},
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 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.}
}
@INPROCEEDINGS{BirkedalEtAl:2006:BigraphicalProgrammingLanguagesPervasiveComputing,
AUTHOR = {Lars Birkedal and Mikkel Bundgaard and Troels
Christoffer Damgaard and S{\o}ren Debois and Ebbe
Elsborg and Arne John Glenstrup and Thomas Troels
Hildebrandt and Robin Milner and Henning Niss},
TITLE = {Bigraphical Programming Languages for Pervasive
Computing},
BOOKTITLE = {Proceedings of Pervasive 2006 International
Workshop on Combining Theory and Systems Building in
Pervasive Computing (CTSB'06)},
PAGES = {653--658},
YEAR = 2006,
EDITOR = {Thomas Strang and Vinny Cahill and Aaron Quigley},
MONTH = MAY,
PDF = {http://www.itu.dk/~panic/Papers/BirkedalEtAl-2006-BPL4PervasiveComp.pdf},
ABSTRACT = {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
\emph{Context-awareness}, \emph{business processes
and Reactive XML}, \emph{axiomatisation and
matching}, and \emph{higher-order mobile embedded
resources}.}
}
@ARTICLE{DamgaardBirkedal:2005:AxiomatizingBindingBigraphs,
AUTHOR = {Troels Christoffer Damgaard and Lars Birkedal},
TITLE = {Axiomatizing Binding Bigraphs},
JOURNAL = {Nordic Journal of Computing},
YEAR = 2006,
PAGES = {58--77},
VOLUME = 13,
NUMBER = {1--2},
PDF = {http://www.itu.dk/people/birkedal/papers/axb-njc.pdf},
ABSTRACT = {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.}
}
@INPROCEEDINGS{BirkedalEtAl:2006:BigraphicalModelsContextSystems,
AUTHOR = {Lars Birkedal and S{\o}ren Debois and Ebbe Elsborg
and Thomas Hildebrandt and Henning Niss},
TITLE = {Bigraphical Models of Context-Aware Systems},
BOOKTITLE = {Proceedings of the 9th International
Conference on Foundations of Software Science and
Computation Structure (FoSSaCS'06)},
EDITOR = {Luca Aceto and Anna Ing\'{o}lfsd\'{o}ttir},
PAGES = {187--201},
YEAR = 2006,
VOLUME = 3921,
SERIES = {Lecture Notes in Computer Science},
MONTH = MAR,
PUBLISHER = {Springer-Verlag},
PDF = {http://www.itu.dk/people/elsborg/fossacs06.pdf},
ABSTRACT = {As part of ongoing work on evaluating Milner's
bigraphical reactive systems, we investigate bigraphical
models of \emph{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
\emph{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.}
}
@INPROCEEDINGS{BundgaardHildebrandt:2005:BigraphicalSemanticsHigher,
AUTHOR = {Mikkel Bundgaard and Thomas Hildebrandt},
TITLE = {Bigraphical Semantics of Higher-Order Mobile
Embedded Resources with Local Names},
BOOKTITLE = {Proceedings of Graph Transformation for
Verification and Concurrency Workshop (GT-VC'05)},
PAGES = {7--29},
YEAR = 2006,
EDITOR = {Rensink, Arend and Heckel, Reiko and K{\"o}nig, Barbara},
VOLUME = 154,
SERIES = {Electronic Notes in Theoretical Computer Science},
PUBLISHER = {Elsevier},
PDF = {http://www.itu.dk/people/mikkelbu/papers/gt-vc05.pdf},
ABSTRACT = {\emph{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
\emph{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
\emph{localised bigraphs} as a generalisation of
local bigraphs in which links can be further
localised.}
}
@INPROCEEDINGS{BundgaardSassone:2006:TypedPolyadicPiCalculusInBigraphs,
AUTHOR = {Bundgaard, Mikkel and Sassone, Vladimiro},
TITLE = {Typed Polyadic Pi-calculus in Bigraphs},
BOOKTITLE = {Proceedings of the 8th ACM SIGPLAN
international conference on Principles and Practice
of Declarative Programming (PPDP'06)},
PAGES = {1--12},
YEAR = 2006,
PDF = {http://www.itu.dk/people/mikkelbu/papers/ppdp06.pdf},
ABSTRACT = {\emph{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 \emph{typed polyadic $\pi$-calculus} with
capability types \`a la Pierce and Sangiorgi, which we
represent using a novel kind of link sorting called
\emph{subsorting}. Using the theory of \textit{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.}
}
@INPROCEEDINGS{HildebrandtEtAl:2005:DistributedReactiveXML,
AUTHOR = {Thomas Hildebrandt and Henning Niss and Martin
Olsen and Jacob Wahl Winter},
TITLE = {Distributed {R}eactive {XML}},
YEAR = 2005,
BOOKTITLE = {Proceedings of 1st International Workshop
on Methods and Tools for Coordinating Concurrent,
Distributed and Mobile Systems (MTCoord'05)},
EDITOR = {Luis Brim and Isabelle Linden},
PAGES = {61--80},
VOLUME = 150,
SERIES = {Electronic Notes in Theoretical Computer Science},
PDF = {http://www.itu.dk/people/hniss/pubs/mtcoord2005.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 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.}
}
@INPROCEEDINGS{LeiferMilner:2000:DerivingBisimCong,
AUTHOR = {James J. Leifer and Robin Milner},
TITLE = {Deriving Bisimulation Congruences for Reactive Systems},
BOOKTITLE = {Proceedings of the 11th International Conference
on Concurrency Theory (CONCUR'00)},
EDITOR = {Catuscia Palamidessi},
YEAR = 2000,
VOLUME = 1877,
PAGES = {243--258},
SERIES = {Lecture Notes in Computer Science},
OPTMONTH = {},
PUBLISHER = {Springer-Verlag},
PDF = {http://moscova.inria.fr/~leifer/articles/leifer-derbc.ps.gz},
ABSTRACT = {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.}
}
@ARTICLE{LeiferMilner:2006:LTSLinkGraphsPetriNets,
AUTHOR = {James J. Leifer and Robin Milner},
TITLE = {Transition systems, link graphs and Petri nets},
JOURNAL = {Mathematical Structures in Computer Science},
YEAR = 2006,
VOLUME = 16,
NUMBER = 6,
PAGES = {989--1047},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Milner:2001:BigraphicalReactiveSystems,
AUTHOR = {Robin Milner},
TITLE = {Bigraphical Reactive Systems},
BOOKTITLE = {Proceedings of the 12th International Conference
on Concurrency Theory (CONCUR'01)},
PAGES = {16--35},
YEAR = 2001,
EDITOR = {Kim Guldstrand Larsen and Mogens Nielsen},
VOLUME = 2154,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {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.}
}
@INPROCEEDINGS{JensenMilner:2003:BigraphsAndTransitions,
AUTHOR = {Ole H{\o}gh Jensen and Robin Milner},
TITLE = {Bigraphs and Transitions},
BOOKTITLE = {Proceedings of the 30th {ACM} {SIGPLAN--SIGACT}
{S}ymposium on {P}rinciples of {P}rogramming {L}anguages
(POPL'03)},
PAGES = {38--49},
YEAR = 2003,
PUBLISHER = {ACM Press},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Milner:2003:BigraphsForPetriNets,
AUTHOR = {Robin Milner},
TITLE = {Bigraphs for Petri Nets},
BOOKTITLE = {Lectures on Concurrency and Petri Nets, Advances in Petri
Nets},
PAGES = {686-701},
YEAR = 2003,
EDITOR = {J{\"o}rg Desel and Wolfgang Reisig and Grzegorz Rozenberg},
VOLUME = {3098},
SERIES = {Lecture Notes in Computer Science},
OPTMONTH = {},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Milner:2005:EmbeddingsContextsForLinkGraphs,
AUTHOR = {Robin Milner},
TITLE = {Embeddings and Contexts for Link Graphs},
BOOKTITLE = {Formal Methods in Software and Systems Modeling},
PAGES = {343--351},
YEAR = 2005,
EDITOR = {Hans-J{\"o}rg Kreowski and
Ugo Montanari and
Fernando Orejas and
Grzegorz Rozenberg and
Gabriele Taentzer},
VOLUME = {3393},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {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.}
}
@ARTICLE{Sassone:2002:DerivingBisimulationCongruences,
AUTHOR = {Vladimiro Sassone and
Pawel Soboci{\'n}ski},
TITLE = {Deriving Bisimulation Congruences: A 2-categorical Approach},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
YEAR = {2002},
VOLUME = {68},
NUMBER = {2},
PAGES = {105--123},
ABSTRACT = {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.}
}
@ARTICLE{Sassone:2003:DerivBisimCongUsing2Cat,
AUTHOR = {Vladimiro Sassone and
Pawel Soboci{\'n}ski},
TITLE = {Deriving Bisimulation Congruences using 2-categories},
JOURNAL = {Nordic Journal of Computing},
YEAR = 2003,
VOLUME = {10},
NUMBER = {2},
PAGES = {163--184},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Sassone:2003:2CatsVsPrecats,
AUTHOR = {Vladimiro Sassone and
Pawel Soboci{\'n}ski},
TITLE = {Deriving Bisimulation Congruences: 2-Categories
Vs Precategories},
BOOKTITLE = {Proceedings of the 6th International
Conference on Foundations of Software Science and
Computation Structure (FoSSaCS'03)},
PAGES = {409--424},
YEAR = 2003,
EDITOR = {Andrew D. Gordon},
VOLUME = {2620},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {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.}
}
@ARTICLE{Sobocinski:2004:ProcessCongFromReactRules,
AUTHOR = {Pawel Soboci{\'n}ski},
TITLE = {Process congruences from reaction rules
({L}uca {A}ceto's {C}oncurrency {C}olumn)},
JOURNAL = {Bulletin of the EATCS},
YEAR = 2004,
VOLUME = {84},
PAGES = {102--127},
ABSTRACT = {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.}
}
@ARTICLE{Sassone:2005:LocatingReactionWith2Cats,
AUTHOR = {Vladimiro Sassone and
Pawel Soboci{\'n}ski},
TITLE = {Locating reaction with 2-categories},
JOURNAL = {Theoretical Computer Science},
YEAR = 2005,
VOLUME = {333},
NUMBER = {1--2},
PAGES = {297--327},
ABSTRACT = {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.}
}
@ARTICLE{Sassone:2005:CongruenceForPetriNets,
AUTHOR = {Vladimiro Sassone and
Pawel Soboci{\'n}ski},
TITLE = {A Congruence for Petri Nets},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
YEAR = 2005,
VOLUME = {127},
NUMBER = {2},
PAGES = {107--120},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Sassone:2005:ReactiveSystemsOverCospans,
AUTHOR = {Vladimiro Sassone and
Pawel Soboci{\'n}ski},
TITLE = {Reactive Systems over Cospans},
BOOKTITLE = {Proceedings of 20th IEEE Symposium on Logic in
Computer Science (LICS'05)},
PAGES = {311--320},
YEAR = 2005,
PUBLISHER = {IEEE Computer Society},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Bruni:2005:DerivWeakBisimCong,
AUTHOR = {Roberto Bruni and
Fabio Gadducci and
Ugo Montanari and
Pawel Soboci{\'n}ski},
TITLE = {Deriving Weak Bisimulation Congruences from
Reduction Systems},
BOOKTITLE = {Proceedings of the 16th International Conference on
Concurrency Theory 2005 (CONCUR'05)},
PAGES = {293--307},
YEAR = 2005,
EDITOR = {Mart\'{\i}n Abadi and
Luca de Alfaro},
VOLUME = {3653},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Klin:2005:LabelsFromReductions,
AUTHOR = {Bartek Klin and
Vladimiro Sassone and
Pawel Soboci{\'n}ski},
TITLE = {Labels from Reductions: Towards a General Theory},
BOOKTITLE = {Proceedings of the First International Conference on
Algebra and Coalgebra in Computer Science (CALCO'05)},
PAGES = {30--50},
YEAR = 2005,
EDITOR = {Jos{\'e} Luiz Fiadeiro and
Neil Harman and
Markus Roggenbach and
Jan J. M. M. Rutten},
VOLUME = {3629},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {We consider open terms and parametric rules in the
context of the systematic derivation of labelled
transitions from reduction systems.}
}
@INPROCEEDINGS{Conforti:05:BigraphicalLogicsForXML,
AUTHOR = {Conforti, Giovanni and Macedonio, Damiano and
Sassone, Vladimiro},
TITLE = {Bigraphical Logics for {XML}},
BOOKTITLE = {Proceedings of the Thirteenth Italian Symposium
on Advanced Database Systems (SEBD'05)},
PAGES = {392--399},
YEAR = 2005,
EDITOR = {Cal\`{\i}, Andrea and Calvanese, Diego and Franconi,
Enrico and Lenzerini, Maurizio and Tanca, Letizia},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Conforti:05:SpatialLogicsForBigraphs,
AUTHOR = {Conforti, Giovanni and Macedonio, Damiano and
Sassone, Vladimiro},
TITLE = {Spatial Logics for Bigraphs},
BOOKTITLE = {Proceedings of the 32th International Colloquium on
Automata, Languages and Programming (ICALP'05)},
PAGES = {766--778},
YEAR = 2005,
EDITOR = {Caires, Lu\'{\i}s and Italiano, Giuseppe F. and
Monteiro, Lu\'{\i}s and Palamidessi, Catuscia and
Yung, Moti},
VOLUME = {3580},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Chang:07:BRSCheckArchitecturalInstanceConforming,
AUTHOR = {Zhiming Chang and XinJun Mao and Zhichang Qi},
TITLE = {An Approach based on Bigraphical Reactive Systems
to Check Architectural Instance Conforming to its Style},
BOOKTITLE = {First Joint IEEE/IFIP Symposium on Theoretical Aspects of
Software Engineering (TASE'07)},
PAGES = {57--66},
YEAR = 2007,
PUBLISHER = {IEEE Computer Society},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Bonchi:06:SaturatedSemanticsForReactiveSystems,
AUTHOR = {Filippo Bonchi and Barbara K{\"o}nig and Ugo Montanari},
TITLE = {Saturated Semantics for Reactive Systems},
BOOKTITLE = {Proceedings of 21st IEEE Symposium on Logic in
Computer Science (LICS'06)},
PAGES = {69--80},
YEAR = 2006,
PUBLISHER = {IEEE Computer Society},
DOI = {10.1109/LICS.2006.46},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Bonchi:06:ProcessBisimViaGraphicalEncoding,
AUTHOR = {Filippo Bonchi and Fabio Gadducci and Barbara K{\"o}nig},
TITLE = {Process Bisimulation {\it Via} a Graphical Encoding},
BOOKTITLE = {Proceedings of the 3rd International Conference on
Graph Transformations (ICGT'06)},
PAGES = {168--183},
YEAR = 2006,
EDITOR = {Andrea Corradini and Hartmut Ehrig and
Ugo Montanari and Leila Ribeiro and Grzegorz Rozenberg},
VOLUME = 4178,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {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{\"o}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.}
}
@INPROCEEDINGS{Bonchi:07:CoalgebraicModelsForReactiveSystems,
AUTHOR = {Filippo Bonchi and Ugo Montanari},
TITLE = {Coalgebraic Models for Reactive Systems},
BOOKTITLE = {Proceedings of the 18th International Conference
on Concurrency Theory (CONCUR'07)},
PAGES = {364--379},
YEAR = 2007,
EDITOR = {Lu\'{\i}s Caires and Vasco Thudichum Vasconcelos},
VOLUME = {4703},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {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.}
}
@INCOLLECTION{Conforti:07:StaticBiLogUnifyingLanguage,
AUTHOR = {Conforti, Giovanni and Macedonio, Damiano and Sassone, Vladimiro},
TITLE = {Static {B}i{L}og: a Unifying Language for Spatial Structures},
BOOKTITLE = {Half a century of inspirational research, honouring the scientific influence of Antoni Mazurkiewicz},
PAGES = {91--110},
PUBLISHER = {IOS Press},
YEAR = 2007,
EDITOR = {Penczek, Wojciech and Rozenberg, Grzegorz},
VOLUME = {80},
NUMBER = {1--3},
SERIES = {Fundamenta Informaticae},
OPTTYPE = {},
OPTCHAPTER = {},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Birkedal:08:ConstucSortedReactSyst,
AUTHOR = {Lars Birkedal and S{\o}ren Debois and Thomas Hildebrandt},
TITLE = {On the Construction of Sorted Reactive Systems},
BOOKTITLE = {Proceedings of the 19th International Conference
on Concurrency Theory 2008},
PAGES = {218--232},
YEAR = 2008,
EDITOR = {Franck van Breugel and Marsha Chechik},
VOLUME = 5201,
SERIES = {Lecture Notes in Computer Science},
MONTH = AUG,
PUBLISHER = {Springer-Verlag},
OPTPDF = {},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Grohmann:08:AlgebraDirectedBigraphs,
AUTHOR = {Davide Grohmann and Marino Miculan},
TITLE = {An Algebra for Directed Bigraphs},
BOOKTITLE = {Proceedings of the 4th International Workshop
on Computing with Terms and Graphs 2008},
PAGES = {49--63},
YEAR = 2008,
EDITOR = {Ian Mackie and Detlef Plump},
VOLUME = 203,
NUMBER = 1,
SERIES = {Electronic Notes in Theoretical Computer Science},
MONTH = MAR,
PUBLISHER = {Elsevier},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Grohmann:08:ContrResouAccessInDirectedBigraphs,
AUTHOR = {Davide Grohmann and Marino Miculan},
TITLE = {Controlling resource access in Directed Bigraphs},
BOOKTITLE = {Proceedings 7th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2008)},
PAGES = {},
YEAR = 2008,
EDITOR = {Claudia Ermel and de Lara, Juan and Reiko Heckel},
VOLUME = 10,
SERIES = {Electronic Communications of the EASST},
PUBLISHER = {European Association of Software Science and Technology},
ABSTRACT = {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.}
}
@ARTICLE{Milner:05:AxiomsForBigraphicalStructure,
AUTHOR = {Robin Milner},
TITLE = {Axioms for Bigraphical Structure},
JOURNAL = {Mathematical Structures in Computer Science},
YEAR = 2005,
VOLUME = 15,
NUMBER = 6,
PAGES = {1005--1032},
OPTMONTH = {},
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 this paper
demonstrates; this is because bigraphs treat locality and
connectivity orthogonally.}
}
@INPROCEEDINGS{Leifer:00:DerivingBisimCongForReactiveSystems,
AUTHOR = {James J. Leifer and Robin Milner},
TITLE = {Deriving Bisimulation Congruences for Reactive Systems},
BOOKTITLE = {Proceedings of the 11th International Conference
on Concurrency Theory (CONCUR'00)},
PAGES = {243--258},
YEAR = 2000,
EDITOR = {Catuscia Palamidessi},
VOLUME = 1877,
SERIES = {Lecture Notes in Computer Science},
OPTMONTH = {},
PUBLISHER = {Springer-Verlag},
OPTPDF = {},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Milner:01:BigraphicalReactiveSystems,
AUTHOR = {Robin Milner},
TITLE = {Bigraphical Reactive Systems},
BOOKTITLE = {Proceedings of the 12th International Conference
on Concurrency Theory (CONCUR'01)},
PAGES = {16--35},
YEAR = 2001,
EDITOR = {Kim Guldstrand Larsen and Mogens Nielsen},
VOLUME = 2154,
SERIES = {Lecture Notes in Computer Science},
OPTMONTH = {},
PUBLISHER = {Springer-Verlag},
OPTPDF = {},
ABSTRACT = {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.}
}
@ARTICLE{Milner:06:PureBigraphs,
AUTHOR = {Robin Milner},
TITLE = {Pure Bigraphs: Structure and Dynamics},
JOURNAL = {Information and Computation},
YEAR = 2006,
VOLUME = 204,
NUMBER = 1,
PAGES = {60--122},
MONTH = JAN,
OPTPDF = {},
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. 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.}
}
@INPROCEEDINGS{Milner:07:LocalBigraphsAndConfluence,
AUTHOR = {Robin Milner},
TITLE = {Local Bigraphs and Confluence: Two Conjectures: (Extended
Abstract)},
BOOKTITLE = {Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS 2006)},
OPTPAGES = {65--73},
YEAR = 2007,
EDITOR = {Roberto Amadio and Iain Phillips},
VOLUME = 175,
NUMBER = 3,
SERIES = {Electronic Notes in Theoretical Computer Science},
OPTMONTH = {},
PUBLISHER = {Elsevier},
OPTPDF = {},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Milner:08:BigraphsAndTheirAlgebra,
AUTHOR = {Robin Milner},
TITLE = {Bigraphs and Their Algebra},
BOOKTITLE = {Proceedings of the LIX Colloquium on Emerging Trends in Concurrency Theory (LIX 2006)},
PAGES = {5--19},
YEAR = 2008,
EDITOR = {Catuscia Palamidessi and Frank D. Valencia},
VOLUME = 209,
OPTNUMBER = {},
SERIES = {Electronic Notes in Theoretical Computer Science},
OPTMONTH = {},
PUBLISHER = {Elsevier},
OPTPDF = {},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Bonchi:08:SymbolicSemanticsRevisited,
AUTHOR = {Filippo Bonchi and Ugo Montanari},
TITLE = {Symbolic Semantics Revisited},
BOOKTITLE = {Proceedings of the 11th International Conference on
Foundations of Software Science and Computational Structures
(FoSSaCS'08)},
PAGES = {395--412},
YEAR = 2008,
EDITOR = {Roberto M. Amadio},
VOLUME = 4962,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
OPTMONTH = {},
OPTPDF = {},
ABSTRACT = {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. }
}
@INPROCEEDINGS{Bundgaard:08:FormalizingHOBPELwithBindingBigraphs,
AUTHOR = {Mikkel Bundgaard and Arne J. Glenstrup and
Thomas T. Hildebrandt and Espen H{\o}jsgaard and
Henning Niss},
TITLE = {Formalizing Higher-Order Mobile Embedded Business Processes
with Binding Bigraphs},
BOOKTITLE = {Proceedings of the 10th International Conference on Coordination Models and Languages (COORDINATION 2008)},
OPTPAGES = {83--99},
YEAR = 2008,
EDITOR = {Doug Lea and Gianluigi Zavattaro},
VOLUME = 5052,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
OPTMONTH = {},
OPTPDF = {},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Chang:08:FormalModelReconfSoftArchByBigraphs,
AUTHOR = {Zhiming Chang and XinJun Mao and Zhichang Qi},
TITLE = {Towards a Formal Model for Reconfigurable Software Architectures
by Bigraphs},
BOOKTITLE = {Proceedings of the 7th Working IEEE/IFIP Conference on Software Architecture (WICSA 2008)},
PAGES = {331--334},
YEAR = 2008,
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTMONTH = {},
PUBLISHER = {IEEE Computer Society},
OPTPDF = {},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Zhang:08:BigraphicalModelOfWSBPEL,
AUTHOR = {Min Zhang and Ling Shi and Longfei Zhu and
Yifei Wang and Libo Feng and Geguang Pu},
TITLE = {A Bigraphical Model of WSBPEL},
BOOKTITLE = {Second Joint IEEE/IFIP Symposium on Theoretical Aspects of
Software Engineering (TASE'08)},
PAGES = {117--120},
YEAR = 2008,
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTMONTH = {},
PUBLISHER = {IEEE Computer Society},
OPTPDF = {},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Fernandez:06:IntertNetsVSRhoCalculus,
AUTHOR = {Maribel Fern{\'a}ndez and
Ian Mackie and
Fran\c{c}ois-R{\'e}gis Sinot},
TITLE = {Interaction Nets vs. the $\rho$-calculus: Introducing
Bigraphical Nets},
BOOKTITLE = {Proceedings of the 12th Workshop on Expressiveness in Concurrency (EXPRESS 2005)},
PAGES = {19--32},
YEAR = 2006,
EDITOR = {Jos Baeten and Iain Phillips},
VOLUME = 154,
NUMBER = 3,
SERIES = {Electronic Notes in Theoretical Computer Science},
OPTMONTH = {},
PUBLISHER = {Elsevier},
OPTPDF = {},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Elsborg:08:TypeSystForBigaphs,
AUTHOR = {Ebbe Elsborg and Thomas Hildebrandt and Davide Sangiorgi},
TITLE = {Type Systems for Bigraphs},
BOOKTITLE = {Proceedings of the 4th International Symposium on Trustworthy Global Computing (TGC 2008)},
PAGES = {126--140},
YEAR = 2009,
EDITOR = {Christos Kaklamanis and Flemming Nielson},
VOLUME = 5474,
SERIES = {Lecture Notes in Computer Science},
OPTMONTH = {},
PUBLISHER = {Springer-Verlag},
PDF = {http://www.itu.dk/~elsborg/TGC08_elsborg.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
\emph{bigraphs}. Concretely, we propose to define
type systems for the term language for bigraphs,
which is based on a fixed set of \emph{elementary
bigraphs} and \emph{operators} on these. An
essential elementary bigraph is an \emph{ion}, to
which a \emph{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 \emph{controls} and a set of \emph{reaction
rules}, collectively a \emph{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
\texttt{i}/\texttt{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.}
}
@INPROCEEDINGS{Krivine:08:StochasticBigraphs,
AUTHOR = {Jean Krivine and Robin Milner and Angelo Troina},
TITLE = {Stochastic Bigraphs},
BOOKTITLE = {Proceedings of the 24th Conference on the Mathematical
Foundations of Programming Semantics (MFPS 2008)},
PAGES = {73--96},
YEAR = 2008,
EDITOR = {Andrej Bauer and Michael Mislove},
VOLUME = 218,
OPTNUMBER = {},
SERIES = {Electronic Notes in Theoretical Computer Science},
OPTMONTH = {},
PUBLISHER = {Elsevier},
PDF = {http://www.lix.polytechnique.fr/~krivine/articles/KriMilTro08.pdf},
ABSTRACT = {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.}
}
@INPROCEEDINGS{OConchuir:09:KindBigraphs,
AUTHOR = {\'{O} Conch\'{u}ir, Shane},
TITLE = {Kind Bigraphs},
BOOKTITLE = {Proceedings of the Irish Conference on the Mathematical
Foundations of Computer Science and Information Technology
(MFCSIT 2006)},
PAGES = {361--377},
YEAR = {2009},
EDITOR = {Anthony Seda and Menouer Boubekeur and Ted Hurley and
Mac an Airchinnigh, Micheal and Michel Schellekens and
Glenn Strong},
VOLUME = {225},
OPTNUMBER = {},
SERIES = {Electronic Notes in Theoretical Computer Science},
PUBLISHER = {Elsevier},
OPTPDF = {},
DOI = {10.1016/j.entcs.2008.12.086},
ABSTRACT = {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.}
}
@INPROCEEDINGS{Bonchi:09:ReactSysyBarbSemMobilAmbients,
AUTHOR = {Filippo Bonchi and Fabio Gadducci and Giacoma Valentina Monreale},
TITLE = {Reactive Systems, Barbed Semantics, and the Mobile Ambients},
BOOKTITLE = {Proceedings of the 12th International Conference on
Foundations of Software Science and Computational Structures
(FoSSaCS'09)},
PAGES = {272--287},
YEAR = 2009,
EDITOR = {Luca de Alfaro},
VOLUME = 5504,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
OPTPDF = {},
ABSTRACT = {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 Soboci{\'n}ski
and by Merro and Zappa Nardelli.}
}
@INPROCEEDINGS{Bonchi:09:LTSforMAviaGraphEnc,
AUTHOR = {Filippo Bonchi and Fabio Gadducci and Giacoma Valentina Monreale},
TITLE = {Labelled Transitions for Mobile Ambients (As Synthesized via a Graphical Encoding)},
BOOKTITLE = {Proceedings of the 15th Workshop on Expressiveness in Concurrency (EXPRESS 2008)},
PAGES = {73--98},
YEAR = 2009,
EDITOR = {Thomas Hildebrandt and Daniele Gorla},
VOLUME = 242,
NUMBER = 1,
SERIES = {Electronic Notes in Theoretical Computer Science},
OPTMONTH = {},
PUBLISHER = {Elsevier},
OPTPDF = {},
ABSTRACT = {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{\"o}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.}
}
This file has been generated by
bibtex2html 1.52