— |
cours:c-2-3-3 [2011/07/12 19:26] (current) |

| + | |

| + | ===== Bigraphs -- unifying models of mobile interaction (12h, 2 ECTS) ===== |

| + | Responsible: [[http://www.lix.polytechnique.fr/~rm135/|Robin Milner]], |

| + | professor, Ecole Polytechnique |

| + | |

| + | The course will be held in english. The venue is Room OC2, 175 rue du Chevaleret; |

| + | time 16h15--19h15; dates 8,15,22,29 January 2007. All are welcome. |

| + | |

| + | The lecture notes are at http://www.lix.polytechnique.fr/~rm135/big-lectures.pdf ; |

| + | slides for the first half of the course are at http://www.lix.polytechnique.fr/~rm135/big-slides-1-a.pdf ; |

| + | slides for the last half are at http://www.lix.polytechnique.fr/~rm135/big-slides-2.pdf . |

| + | |

| + | Exercises on each chapter will be handed out, and the last hour each week will be spent trying them. |

| + | (Solutions will be available probably a week later.) |

| + | |

| + | NEW, 19/01/07: Exercises for the first half of the course are now at http://www.lix.polytechnique.fr/~rm135/big-exercises-1.pdf , and for the second half at http://www.lix.polytechnique.fr/~rm135/big-exercises-2.pdf . |

| + | |

| + | There won't be time to cover everything in the notes. |

| + | Comments are welcome from anyone at any time. |

| + | |

| + | ==== Summary ==== |

| + | There has been recently a surge in ideas for how to model mobile |

| + | interaction, not only in informatic systems but even in |

| + | biology. Algebraic calculi are playing a strong part in this |

| + | development. With the new ideas comes a problem of unity. As yet |

| + | there is no canonical way to handle mobility, and we need much more |

| + | experiment --- both in logic and algebra and in attempted |

| + | applications --- before we can solve this problem. |

| + | |

| + | Bigraphs are effort towards this unity. They build upon existing |

| + | models, which show two kinds of mobility. There is the mobility of |

| + | linkage, or connectivity, represented by the pi calculus; and there |

| + | is the spatial mobility pioneered by mobile ambients. Bigraphs |

| + | reflect this duality in the mathematical structures involved. They |

| + | also try to unite the spatial metaphors that are found throughout |

| + | computing (even sequential computing: think of locations, pointers, |

| + | storage, scope, nesting, heap, ...) with phenomena of physical |

| + | space (think of building structure, plant structure, sensor |

| + | networks, ...). |

| + | |

| + | The course will begin with simple examples of modelling physical |

| + | space and movement. This will move rapidly to a model based upon |

| + | elementary category theory; this seems to be the best way to |

| + | represent the modularity in spatial structure and the way it |

| + | changes. The next example is direct presentation of CCS, showing |

| + | how we can recover some of the theory for existing models, and even |

| + | enrich them. A strong focus of the course is on recovering |

| + | behavioural equivalence, such as bisimilarity, in a uniform way. |

| + | The result for CCS is encouraging and does not require difficult |

| + | mathematics. This completes Part I of the course. |

| + | |

| + | Part II begins by enriching the mathematics not only to handle |

| + | system structure algebraically, but also to handle the notion |

| + | of occurrence of one system within another. This will be essential |

| + | to model the way the elements of a mobile system (nodes, processes |

| + | or other kinds of substructure) retain their identity as the system |

| + | reconfigures itself. We use a simple categorical construction |

| + | that also underpins a uniform treatment of transition systems, and |

| + | hence of behavioural equivalence. The techniques are illustrated |

| + | by application to Petri nets --- which, though not mobile, do |

| + | provide a further test of the use of bigraphs. |

| + | |

| + | The course aims to deal with these theories and applications in |

| + | some detail, with plenty of exercises. The aim is not to rush |

| + | through a predetermined amount, but to deal with the material in |

| + | whatever depth it needs. |

| + | |

| + | Many of the ideas of bigraphs were worked out with James Leifer and |

| + | Ole Hogh Jensen over the past decade. There will be a citation |

| + | list, and also a complete text written with this course in mind. |

| + | |

| + | |

| + | ==== Prerequisites ==== |

| + | |

| + | There is no strong mathematical prerequisite (e.g. the category |

| + | theory is elementary), but an interest in mathematical modelling will |

| + | be very helpful. |

| + | |

| + | ==== Related courses ==== |

| + | 2-3: This course treats related topics and the student may find in |

| + | them interesting connections and useful background knowledge. However |

| + | it is not required, since our course will be self-contained |

| + | |

| + | ==== References ==== |

| + | |

| + | |

| + | ==== Les années précédentes ==== |

| + | * [[2009-2010-C-2-3-3|Année 2009-2010]] |

| + | * [[2008-2009-C-2-3-3|Année 2008-2009]] |

| + | * [[2007-2008-C-2-3-3|Année 2007-2008]] |

| + | * [[2006-2007-C-2-3-3|Année 2006-2007]] |

| + | |

| + | |

| + | ------ |

| + | * Set ALLOWTOPICCHANGE = %MAINWEB%.WebMastersGroup, %MAINWEB%.RobinMilner |

| + | |

| | | |