The Concurrency and Mobility Group @ ITU

Welcome to the homepage of the Concurrency and Mobility (CoMo) group at the IT University of Copenhagen.

See the student page for teaching and project proposals in the area of concurrency and mobility.

News

• Fall 2007: Some new papers
  
  • A Calculus for Mobile Ad Hoc Networks (Extended Abstract). Jens Chr. Godskesen. In Proceedings of Coordination'07, June 2007, Paphos, Cyprus. Full version pdf.
  • Modelling the security of smart cards by hard and soft types for higher-order mobile embedded resources. Mikkel Bundgaard, Thomas Hildebrandt, and Jens Chr. Godskesen. In Proceedings of the 5th International Workshop on Security Issues in Concurrency (SecCo'07), Electronic Notes in Theoretical Computer Science. Elsevier, 2007. pdf. Full version here.
• Fall 2006: New paper
  Formal verification of the ARAN protocol using the applied Pi-calculus. Jens Chr. Godskesen. In Proceedings of Sixth International IFIP WG 1.7 Workshop on Issuses in the Theory of Security, (WITS), pages 99--113, Vienna, Austria, March 2006. pdf.
• July 2006: New paper on Bigraphs
  Typed Polyadic Pi-calculus in Bigraphs. Mikkel Bundgaard and Vladimiro Sassone. In Proceedings of the 8th International Symposium on Principles and Practice of Declarative Programming (PPDP'06), pages 1-12. ACM Press, 2006. pdf.
• June 2005: New papers on Semantics of Higher-order Mobile Embedded Resources
  • Extending Howe's Method to Early Bisimulations for Typed Mobile Embedded Resources with Local Names, Jens Chr. Godskesen and Thomas Hildebrandt. In Foundations of Software Technology and Theoretical Computer Science 2005, volume 3821 of Lecture Notes in Computer Science. Springer-Verlag. pdf.
  • Bigraphical Semantics of Higher-Order Mobile Embedded Resources with Local Names, Mikkel Bundgaard and Thomas Hildebrandt. In Rensink, A., Heckel, R., and König, B., editors, Proceedings of Graph Transformation for Verification and Concurrency Workshop 2005, volume 154 of Electronic Notes in Theoretical Computer Science, pages 7-29. Elsevier. pdf.

People

Researchers: Lars Birkedal (assoc. professor), Room 4C 15 Mikkel Bundgaard (PostDoc), Room 3C 10 Troels C. Damgaard (Ph.D. student), Room 4C 07 Søren Debois (Ph.D. student), Room 4C 07 Ebbe Elsborg (Ph.D. student), Room 3C 10 Jens Chr. Godskesen (assoc. professor), Room 4C 10 Thomas Hildebrandt (assoc. professor), Room 4C 12

Students: Bo Mikael Blomqvist Li Chen Kirankumar Gullapalli Lars Christian Hansen Tahseen Hussain Kenneth Ahn Jensen Kasper Svenstrup Kock Jon Ebbe Larsen Jesper Munk Trygve Plohn

Current Activities

The activities of the members of the group spans a great variety of areas within the theory of concurrency and mobility. Below we present the main areas of research: Homer, Mobility and Security, Connectivity Testing, Bigraphs, and Categorical Models for Concurrency.

Homer

Homer is a process calculi with process passing, local names, non-linear active process mobility, and nested locations. The calculus has a very simple syntax and semantics, which conservatively extend the standard syntax and semantics for process passing calculi. Homer is an abbreviation for Higher-Order Mobile Embedded Resources. See this page for a short presentation of Homer.

Publications

• T. Hildebrandt, J. C. Godskesen, and M. Bundgaard. Bisimulation Congruences for Homer --- a Calculus of Higher Order Mobile Embedded Resources. Technical Report TR-2004-52, IT University of Copenhagen, 2004. (pdf and ps)
• M. Bundgaard, T. Hildebrandt, and J. C. Godskesen. A CPS Encoding of Name-passing in Higher-Order Mobile Embedded Resources. In Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS'04), ENTCS. Elsevier, 2004. To appear. (pdf and ps)
• J. C. Godskesen, T. Hildebrandt, and V. Sassone. A Calculus of Mobile Resources. In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR'02), volume 2421 of LNCS, pages 272--287. Springer Verlag, 2002.
• J. C. Godskesen, T. Hildebrandt, and S. E. Jacobsen. An Implementation of the MR calculus. Technical Report TR-2002-14, IT University of Copenhagen, 2002. (pdf and ps).

Projects and Theses

• Jesper Munk - A prototype implementation of Homer. In preparation.

Mobility and Security

Mobility and security is a quite new topic within the group. Right now we study various security protocols for mobile systems, the goal is to develop calculi and tools for reasoning about spatial security protocols.

Projects and Theses

• Trygve Plohn - Secure anonymous mobile communication. In preparation.
• Kenneth Ahn Jensen - Security in XML based Web Services. In preparation.
• Bo Mikael Blomqvist and Lars Christian Hansen - Security on ad hoc networks. In preparation.
• Tahseen Hussain and Kirankumar Gullapalli - AAA Architecture for Mobile IP. In preparation.
• Kasper Svenstrup Kock and Jon Ebbe Larsen - Zonebased communications- and interactionsystem

Connectivity Testing

In this project we consider automatic test derivation for embedded systems (i.e. mobile phones, pda's, etc.). To guide the test derivation process we make use of so called fault models, in our case a fault is a missing connection between the interface of the system and the embedded software. One of the goals is to make use of standard model checkers to do the test generation. The project is a joint effort with the Center for Embedded Software Systems (CISS) at Aalborg University.

Publications

• J. C. Godskesen. Connectivity Testing. In Formal Methods in System Design, 25(1):5-38, 2004.
• J. C. Godskesen, Brian Nielsen and Arne Skou. Connectivity Testing through Model-Checking. International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), September 2004, Madrid, Spain.
• J.C. Godskesen. Complexity issues of connectivity testing. FATES'01, Aalborg University, August 2001.
• J.C. Godskesen. Fault models for embedded systems. CHARME'99, volume 1703 of Lecture Notes in Computer Science, Bad Herrenalb, September 1999. Springer-Verlag.

Projects and Theses

• Li Chen - System monitor In Automation Test Environment. In preparation.

Bigraphs and Reactive XML

Bigraphs is a process framework for modelling systems with mobile placing and linking. The framework tries to unite existing process calculi such as the pi-calculus, Mobile Ambients and Petri nets. Members of the CoMo group participates in the Bigraphical Programming Languages (BPL) project at ITU. See the BPL project page for more information.

Reactive XML is an XML representation of the abstract model of Bigraphical Reactive Systems. Models of computation in which the computation state is represented in XML have been proposed as an answer to the demand for interoperability, heterogeneity and openness in globally distributed applications. We propose Reactive XML as such an XML-centric model of computation, which allows general reactive systems, their state as well as behaviours, to be described in XML. A prototype tool for Reactive XML has been implemented and described in an Internet and Software Technology MSc thesis by Jacob Winther and a distributed, peer-2-peer implementation based on XML-store has been implemented by MSc student and research assistant, Martin Olsen.

Publications

• Distributed Reactive XML - an XML-centric coordination Thomas Hildebrandt, Henning Niss, Martin Olsen and Jacob W. Winther,ITU Technical report TR-2005-62,
• Reactive XML - an XML-centric coordination middleware for context-dependent mobile communication, Thomas Hildebrandt, Henning Niss, Martin Olsen and Jacob W. Winther, Poster at the 11th international conference on Coordination Models and Languages
• Bigraphs and (Reactive) XML - an XML-centric model of computation, Thomas Hildebrandt, Jacob W. Winther, ITU Technical report TR-2005-56.

Projects and Theses

• Jakob W. Winther - Reactive XML, MSc thesis
• Jakob Bang Hansen - Process Models for Biological Systems, MSc thesis.

Categorical Models for Concurrency

This work contributes to the categorical approach to a unified semantics for concurrency developed through the last 20 years, initially reported on in the chapter on models for concurrency by Glynn Winskel and Mogens Nielsen, Handbook of Logic in Computer Science.

Publications

• T. Hildebrandt, P. Panangaden, and G. Winskel. A relational model of non-deterministic dataflow. In Journal of MSCS, 14(5):613-649, 2004. (Full version of CONCUR '98 paper).
• T. Hildebrandt. Towards Categorical Models for Fairness: Fully Abstract Presheaf Semantics of SCCS with Finite Delay. In Journal of Theoretical Computer Science, 294(1-2):151-181, 2003.
• T. Hildebrandt and V. Sassone. Comparing Transition Systems with Independence and Asynchronous Transition Systems. In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR'96), volume 1119 of LNCS, pages 84--97. Springer Verlag, 1996. Also available as BRICS Report, RS-96-18 (ps and dvi).
• T. Hildebrandt and V. Sassone. Transition Systems with Independence and Multi-Arcs. In Proceedings of the DIMACS workshop on Partial order methods in verification (POMIV'96), pages 273--288. AMS Press, 1996. Also available as BRICS Report, RS-97-10 (pdf, ps, and dvi).

Previous Visitors

• Matthew Hennessy, Professor of Computer Science at Department of Informatics, University of Sussex. Visiting November 29th - 30th. Seminar: November 29th: SafeDpi: a language for controlling mobile code and speaker at the conference on Context-aware Computing
• Daniele Varacca, Post. Doc. at Ecole Normale Superieure.Visiting November 9th - November 23th, 2004. Minicourse: Probabilistic Models for Concurrency
• Mogens Nielsen, Associate Professor at BRICS. Seminar: November 19th, 2004: Towards Formal Models for Trust in Global Computing
• Francesco Zappa Nardelli, Associate Professor at INRIA Rocquencourt. Visiting November 7th - November 10th, 2004. Seminar: LaCoMoCo Research Seminar on Programming Languages and Models for Mobile Communicating Systems
• Björn Victor, Senior Lecturer at Department of Information Technology, Division of Computer Systems at Uppsala University. Visiting November 7th - November 13th, 2004. Seminar: November 8th: LaCoMoCo Research Seminar on Programming Languages and Models for Mobile Communicating Systems
• Peter Sewell, Fellow and Director of Studies at Wolfson college, at University of Cambridge. Visiting November 8th - November 12th, 2004. Seminar: LaCoMoCo Research Seminar on Programming Languages and Models for Mobile Communicating Systems

Related Research Groups

• The Mobility Group at Uppsala University, Sweden
• The Foundations of Computation at Informatics at University of Sussex, UK

Links

• Calculi for Mobile Processes - Links to bibliographies, books, introductory reading, people, and projects.
• Selected Bibliography on Mobile Processes - A bibliography by Kohei Honda.
• AmbientCalculiOnline - Wiki for Ambient Calculi containing references to people and articles.
• MOCA - A mailing list on models for mobility founded by Davide Sangiorgi, until june 2005 moderated by Davide and Pascal Zimmer, now moderated by Michael Baldamus and Björn Victor.
• The Concurrency Mailing List - A mailing list for concurrency.

last updated November 2007