Home » forums » LtU Forum

Pure bigraphs: structure and dynamics (by Robin Milner)

I just came accross this interesting paper: Pure bigraphs: structure and dynamics. From the abstract:

"...it is shown that behavioural
analysis for Petri nets, pi-calculus and mobile ambients can all
be recovered in the uniform framework of bigraphs."

An interesting thing from my point of view is that an attempt is made to provide a descriptive explanation of the material, obviously along with math proofs.


There are also three, very basic, audio lectures(!) on pi-calculus at the following site: http://courses.cs.vt.edu/~cs5204/fall03/DayByDay.html.

By shahbaz at 2005-05-27 15:56 | LtU Forum | previous forum topic | next forum topic | other blogs | 8191 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

posted multiple times?

I'm not sure why I see this message posted three times! I only posted it once.

By shahbaz at Fri, 2005-05-27 16:24 | login or register to post comments

[admin] dups deleted

I've deleted the other two. They all had different posting times, which implies multiple separate posts, but it could also be gremlins (technical term).

By Anton van Straaten at Wed, 2005-06-01 03:12 | login or register to post comments

Could someone provide me a breif heirarchy of Milner's construct

ions?

I recall (trying to get through this stuff a few years ago), {pi,action,various other greek letters}-calculi and I recall him writing something about bigraphs awhile ago...

I get a little confused as to what each is practially intended for and where they sit wrt eachother in terms of abstraction...

By gmol at Tue, 2005-05-31 07:33 | login or register to post comments

What little I know

Milner's original bigraphs paper has been on my to read list for almost three years now, and I still haven't got past the abstract, but I did discuss the paper with some people who knew a little more about it, so here goes...

Milner was interested in finding clean abstractions that could model in a more natural and mathematically tractable manner than the language-based approach used in process algebras. He had become aware of the work on graph transformation grounded in the single/double-pushout approach, and bigraphs were the result of his investigations. They can be regarded as a sort of sufficiently rich class of algebraic models that can be used to express the properties of Petri nets, CCS, pi-calculus etc. The 2002 paper (the ancestor of the cited one) was the keynote talk at the first ICGT (that is, International Conference of Graph Transformation).

By Charles A Stewart at Wed, 2005-06-01 14:08 | login or register to post comments

Deriving process congruences from reaction rules

And here comes critique:

Deriving process congruences from reaction rules

Leifer and Milner, aware of the problems which arise as a consequence of discarding the 2-dimensional structure, have also introduced technology in order to deal with these issues. The main developments have centered around Leifer’s functorial reactive systems and Milner’s S-precategories, also known as well-supported precategories and S-categories. [...] Unfortunately, such supported structures no longer form categories – arrow composition is partial – which has the effect of making the theory laborious and based in part on set theoretical reasoning and principles.
And here comes solution:
We shall begin by extending Leifer and Milner’s theory of reactive systems to a 2-categorical setting.
The author extends underpinnings of bigraphs, basically "porting" them to 2-categorical "platform". Personally, I am affraid of 2-categories more than of sets, but let's see...
By Andris Birkmanis at Sat, 2005-06-11 19:24 | login or register to post comments

Some foolishness

I scanned the first chapter, the guy writes very clearly but since I lack CT-training have a lot of difficulty reading it. Is there an informal explanation to what he did?

It also remembers me of something I once -this is more than ten years ago- played with. Some ideas on finite bisimilar (self-containing) boxes (akin to graph structures) which encode both values and functions (this is actually pretty easy). I think in the end I reduced it to grammar theory -the composition of a function and a value reduced to calculating the intersection on ?two-level? grammars- and there I stopped. I guess, in the end, it was a foolish idea ;-). Anyway, there must have been a lot of people smarter than I am who went down some similar road so I wonder, any references on something like that?

By marco at Sat, 2005-06-11 21:55 | login or register to post comments

Getting informal

I scanned the first chapter, the guy writes very clearly but since I lack CT-training have a lot of difficulty reading it. Is there an informal explanation to what he did?
I like his style and find it very clear as well. I also lack a formal CT training, but by reading papers I think I acquired enough understanding to survive until 2.2.3 (still without attrition).

Informal explanation? I already gave it :-) He ported Milner's theory of bigraphs to a more categorial platform (in a way "replacing" set theory for supports of arrows by second level of arrows, 2-dimensional arrows or cells), thus making it more maintainable, optimizable, popular... Eh, the last one might be not completely correct :-)

In both theories objects are interfaces (or signatures, or types, or contracts), arrows are [syntactical] contexts (or terms with holes, or components with parameters), composition is inclusion of context in another one (or composition of components).

This structure alone is insufficient to fully model reactive systems, as there is some need to pin down items of contexts. Milner does this by introducing support sets (informally sets of oids for items) leading to a notion of s-categories (which are not categories). Sobocinski solves the problem by introducing "witness" arrows between arrows - which also happen to form what is traditionally called structural congruence (so terms/contexts are not syntactic entities any more, but classes of equivalences of them). This quotient is possible because the 2-cells (witnesses) used in the thesis are isomorphisms, so form an equivalence relation. All in all, this looks logical, smooth, and not as frightening as it sounded in the beginning. Ah, and it gives one a nice possibility to chase diagrams.

I hope this is sufficiently informal on one hand, and sufficiently correct on the other :-)

I wonder, if CAS or Marc will want to help and correct me.

[well, as you guessed, this was supposed to be a reply to marco]

[also, when I write about "porting" I mean "initial contribution", so it's ready to be open-sourced, if we continue to pursue this analogy]

By Andris Birkmanis at Sun, 2005-06-12 06:46 | login or register to post comments