Chinese Journal of Computers   Full Text
Title	Bigraphical Semantics of Seal Calculus
Authors	JIN Long-Fei LIU Lei
Address	(College of Computer Science and Technology, Jilin University, Changchun 130012)
Year	2008
Issue	No.3(522—528)
Abstract &   Background	Abstract Bigraphical Reactive Systems (BRS) is a new theoretical tool, and is based on a graphical model of mobile computation that emphasizes both locality and connectivity， named Bigraph. Bigraphs generalize both characteristics of the π calculus and the Mobile Ambient calculus, and it can represent complex systems that emphasize both locality and connectivity. The theory of BRS provides a uniform modeling framework for design and implementation of pervasive computing in different levels. The Seal calculus is a process language for describing mobile computation with security features. A bigraphical representation of a Seal calculus without replication is provided in this paper, and structural correspondence and operational correspondence between the Seal calculus and its bigraphical representation are analyzed. This work extends the application domains of BRS and illustrates the ability of BRS in describing security calculi. All are foundations for researching characteristics and applications of Seal calculus within the bigraphical framework. keywords Seal calculus; bigraph; bigraphical reactive system; structural correspondence; operational correspondence background This research is supported by the Research Fund for the Doctoral Program of Higher Education under grant No.20061083044, and the Science Development Plan Project Found of Jilin Province under grant No.20050527. The first project aims to bridge semantic Web domain and process calculi domain, and provide a methodology for researching semantic Web issues using process calculi theories. The second project aims to provide formal semantics of OMG’ ontology definition meta-model (ODM) and apply these formal semantics in semantic Web application domain. The theory of bigraphical reactive systems, due to Milner and co-workers, is based on a graphical model of mobile computation that emphasizes both locality and connectivity. A bigraph comprises a place graph, representing locations of computational nodes, and a link graph, representing interconnection of these nodes. Dynamics are given to bigraphs by defining reaction rules that rewrite bigraphs to bigraphs, roughly, a bigraphical reactive system (BRS) is a set of such rules. There are two principal aims for the new theory of bigraphical reactive systems: (1) to model ubiquitous systems; and (2) to be a meta-theory encompassing existing calculi for concurrency and mobility. Along the second aim, the authors provide a bigraphical representation of the Seal calculus without replication in this paper, and analyze structural correspondence and operational correspondence between the Seal calculus and its bigraphical representation. All are foundations for researching characteristics and applications of Seal calculus within the bigraphical framework. This research is the theory part of the two research projects above. Formal bridge between the logic foundation of semantic Web (such as description logics) and process calculi is built on it. The authors also pay their attentions on researching other important issues of semantic Web using theories of process calculi (especially bigraphs). These issues include ontology definition meta-model, ontology modeling, ontology analysis, ontology evolution and semantic Web applications, etc.