MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\(','\\)']]}}); function MyAutoRun() {    var topp=$(window).height()/2; if($(window).height()>450){ jQuery(".outline_switch_td").css({ position : "fixed", top:topp+"px" }); }  }    window.onload=MyAutoRun; $(window).resize(function(){ var bodyw=$win.width(); var _leftPaneInner_width = jQuery(".rich_html_content #leftPaneInner").width(); var _main_article_body = jQuery(".rich_html_content #main_article_body").width(); var rightw=bodyw-_leftPaneInner_width-_main_article_body-25;   var topp=$(window).height()/2; if(rightw<0||$(window).height()<455){ $("#nav-article-page").hide(); $(".outline_switch_td").hide(); }else{ $("#nav-article-page").show(); $(".outline_switch_td").show(); var topp=$(window).height()/2; jQuery(".outline_switch_td").css({ position : "fixed", top:topp+"px" }); } }); 偶图及其应用研究综述
  软件学报  2016, Vol. 27 Issue (2): 195-208   PDF    
偶图及其应用研究综述
许东 , 王晶晶, 李静    
上海大学 计算机工程与科学学院, 上海 200444
摘要: 偶图是由Robin Milner在2001年提出的一种基于图形的形式化理论模型,试图为普适计算提供一个设计、模拟和分析的平台以及为现有的进程代数提供一个统一的可扩展的框架.介绍了偶图的基本概念,揭示了偶图的数学基础——预范畴、范畴、s-范畴、对称偏幺半范畴之间的关系,对偶图的代数系统进行总结,简化了偶图的离散范式的表述形式,并给予证明.综述了偶图的发展及其应用概况.对偶图范畴的定义、商变换等基本理论中存在的一些问题提出讨论,指出偶图范畴应该属于小范畴而不是大范畴,并给出商变换得出的大范畴转换为小范畴的方法.最后简述了偶图模型的扩展、应用的拓广.
关键词: 偶图    范畴论    偶图范畴    偶图反应系统    偶图应用    
Survey on Bigraph and Its Applications
XU Dong , WANG Jing-Jing, LI Jing    
School of Computer Engineering and Science, Shanghai University, Shanghai 200444, China
Abstract: Bigraph was proposed by Robin Milner in 2001 as a formal theoretical model based on graphs in attempt to provide a design, simulation and analysis platform for ubiquitous computing and present a unified, extensible framework for the existing process algebra. In this paper first introduces the basic concepts of bigraph and reveals relationships among precategory, category, s-category and symmetric partial monoidal category which form the mathematical basis of bigraph, and then summarizes bigraphical algebra system while providing a simplified representation of the discrete normal form in bigraph with a proof. Next, it discusses some questions related to the definition of bigraphical categories and quotient translations after making a survey of the development of bigraph and its applications. This study argues that bigraphical category should be small category other than large category. Moreover, the paper illustrates how to convert the large category derived by quotient to small category. Finally, it outlines the extensions of bigraphical models and their applications.
Key words: bigraph    category theory    bigraphical category    bigraphical reactive system    bigraphical application    

早期的存储式程序计算机,本身高度集成信息引擎,完成特定的计算任务,计算机主要是通过其内部部件之间的通信完成工作.随着信息网络技术的快速发展,如今的计算机工作涉及与环境的交互,包括信息的和物理的部件之间的通信.计算不仅研究人类社会的交互行为,还要研究自然界物质之间的交互.数字信息和物质世界不仅是并存的,而且是可以协作的.普适计算、云计算、物联网、信息物理系统等新型计算模型正是在这样的背景下应运而生.信息技术发展的一个典型特征体现在人、机、物三者之间的频繁交互,而且日趋复杂,通信显得比计算更为重要.

为了适应新型计算模型的需要,Robin Milner在2001年提出了一种基于图形的形式化理论模型——偶图(bigraph)[1].偶图试图集成现有的进程代数理论,如通信系统演算(CCS)[2]、π-演算[3]、λ-演算和移动环境(mobile ambient)演算[4]等的优势,重点强调位置和连接两方面的因素,建立了较为完整、可扩展的理论框架.偶图不是扩展这些经典代数,而是试图建立一个兼容这些进程代数的统一框架,目标是向无所不在的计算提供一个新的理论计算模型.偶图起源于动作演算(action calculi)[5].动作演算有其内在的缺点,在动作演算中,怎样选择合适的上下文是一个困扰多年的问题.后来,人们通过参数重写技术[6]导出带标记的上下文变迁系统.但是,这仍然没有处理反应式系统中的连接性问题.为了解决这个问题,Leifer和Cattani等人引进偶图演算[7, 8, 9]的概念.偶图的数学基础是范畴论,范畴论[10, 11]是抽象地处理数学结构以及结构之间联系的一门数学理论,s-范畴[12, 13]已经很好地应用于偶图中.传统的图重写技术是基于双推出(double pushout)的构造[14],使用一种以图作为对象、以嵌入作为箭头的范畴.相反地,s-范畴将接口看作对象,将图看作箭头,它具有良好的结构和很好的数学性质.偶图还结合范畴论[15]的最新研究成果,如相对推出(relative pushout,简称RPO)等概念,定义最小上下文标记,并保证行为等价是同余(congruence)关系[16, 17, 18, 19, 20].这一理论极大地推动了偶图理论的发展.Perrone等人[21]提出了偶图垂直精化思想,将偶图反应系统BRS泛化为一般的元-演算.

本文简要介绍偶图基本概念、偶图范畴理论、偶图应用概况,最后简述偶图模型的扩展、应用的拓广.

1 偶图基本概念

本节概括性地介绍偶图的基本概念,详细的概念和理论见Milner的介绍[22].

1.1 偶图的基本定义

在介绍偶图的定义之前,先定义几个运算符及符号:

· #表示两个集合是不相交的,如果S#T,那么S$\cap $T=∅;

· $\uplus$表示两个不相交集合的并,如S$\uplus$T;

· X,V和ℰ表示3个有穷集合,且这3个集合互不相交,分别表示名字、节点和边标识符的集合.

偶图是一个二元组B=〈BP,BL〉,BP,BL分别是位置图(place graph)和连接图(link graph).BP由图的节点集V、边的集合E和接口组成,嵌套的节点在位置图中为父子关系,用分支关系表示节点之间的嵌套.位置图的接口分为内部接口和外部接口,分别表示根(root)和站点(site),用有穷序数n表示,即n={0,1,…,n-1}.特别地,0=∅.连接图的接口也分为内部接口和外部接口,分别表示内部名字集和外部名字集.图1所示的偶图F,其位置图和连接图如图2所示.位置图FP的外部接口为3={0,1,2},代表3个根,分别是v1,v2,v3的父节点;而内部接口为1={0},表示其有一个站点(阴影框).这样,位置图可表示成FP:1→3.连接图FL的外部接口为{y0,y1,y2};而内部接口为{x0},说明有一个内部名.这样,连接图可表示成FL:{x0}→{y0,y1,y2}.偶图的外部接口为〈n,Y〉,n,Y分别是BP,BL的外部接口.偶图的内部接口〈m,X〉,m,X分别是BP,BL的内部接口.例如上面的例子F=〈FP,FL〉,其外部接口和内部接口分别是〈3,{y0,y1,y2}〉和〈1,{x0}〉.另外,图中的虚线矩形表示根,有时也称为区域(region).

Fig.1 An example of bigraph (F) 图1 一个偶图示例(F)

Fig.2 Place graph and link graph 图2 位置图和连接图

为了增强偶图的表示能力,引进基本签名.本文对基本签名(basic signature)的定义改写.基本签名是一个二元组(K,ar),这里,K表示控制(control)的集合,∀K$ \in $K,则有K::=K|K:n,其中,n$ \in $N,表示K的元数(arity),N为自然数集.每个控制都有一个映射ar:K→N,表示从控制节点到N的映射.基本签名К上的偶图,就是给每个节点指派一个控制,控制的元数就是该节点的端口(port)数,用小黑圆圈表示,如图3所示.如果给每个控制K指派一个状态,状态值取自于状态集{atomic,passive,active}({原子的,非活跃的,活跃的}),此时称签名为动态签名.说一个K-节点是原子的/非活跃的/活跃的,如果它的控制被赋予一个原子状态/非活跃状态/活跃状态.

Fig.3 Anatomy of bigraphs 图3 偶图剖面图

具体位置图(concrete place graph)FP=(VF,ctrlF,prntF):mn是一个三元组,m是内部接口,n是外部接口,都是有穷序数,分别表示位置图的站点和根.FP有一个有穷节点集VF$\subset $V,一个控制映射ctrlF:VFK和一个父映射:prntF:m$\uplus$VFVF$\uplus$n.具体连接图(concrete link graph)FL=(VF,EF,ctrlF,linkF):XY是一个四元组,X是内部接口,Y是外部接口,都是X的有穷子集,分别称为连接图的内部名字集和外部名字集.FL有一个有穷节点集VF$\subset $V、一个有穷边集EF$\subset $ℰ、一个控制映射ctrlF:VFK和一个连接映射:linkF:X$\uplus$PFEF$\uplus$Y.这里,PF={(v,i)|i$ \in $ar($ctrl_{F}^{L}$(v))}是F的端口集.因此,(v,i)就是节点的第i个端口.具体偶图(concrete bigraph)F=(VF,EF,ctrlF,prntF,linkF):〈m,X〉→ 〈n,YXY,它由一个具体的位置图FP和一个具体的连接FL构成.因此,可把具体偶图写成F=〈FP,FL〉.给每个位置图、连接图或偶图F都附上一个有穷集合|F|,即它的支集(support).对于位置图,定义|F|=VF;对于连接图或偶图, 定义|F|=VF$\uplus$EF.

偶图中的位置Places=Sites$\uplus$V$\uplus$Roots;点Points=Ports$\uplus$X;连接Links=E$\uplus$Y.这里,Places,Sites,Roots,Points, PortsLinks分别表示位置、站点、根、点、端口和连接的集合.边是闭连接,而外部名是开连接.说一个点(point)是开的,如果它的连接是开的;否则它是闭的.说一个偶图G是开的,如果它的所有连接是开的(即,它没有边).没有孩子的位置,或没有点(point)的连接称为闲置的(idle).如果一个偶图没有闲置的边,则称其为瘦(lean)偶图.两个位置有相同的父母或两个点有相同的连接称为兄弟(sibling).图3显示了偶图基本概念框架.

1.2 具体偶图上的算子

如果F:kmG:mn是两个位置图且|F|#|G|,则它们的组合为GoF=(V,ctrl,prnt):kn,其中,V=VF$\uplus$VG,控制映射ctrl=ctrlF$\uplus$ctrlG.m上的单位(identity)位置图定义为$i{d_m}\mathop {\rm{ = }}\limits^{{\rm{def}}} (\emptyset ,{\emptyset _\kappa },I{d_m}):m \to m.$如果F:XYG:YZ是两个连接图且|F|#|G|,它们的组合GoF=(V,E,ctrl,prnt):XZ,其中,V=VF$\uplus$VG,E=EF$\uplus$EG,ctrl=ctrlF$\uplus$ctrlG.X上的单位连接图定义为$i{d_X}\mathop {\rm{ = }}\limits^{{\rm{def}}} (\emptyset ,\emptyset ,{\emptyset _\kappa },I{d_X}):X \to X.$如果F:IJG:JK是两个偶图且|F|#|G|,则它们的组合是:

$G\circ F\overset{\text{def}}{\mathop{\text{=}}}\,{{G}^{P}}\circ {{F}^{P}},\text{ }{{G}^{L}}\circ {{F}^{L}}:I\to K.$

I=〈m,X〉上的单位偶图是〈idm,idX〉.

两个具有相同接口的偶图FG,从FG的一个支集变换r:|F|→|G|,由一对双射rV:VFVGrE:EFEG组成,rVrE遵从它们的结构.给定F和双r,G可由这些条件唯一决定.因此,可用r×F表示G,称GFr下的支集变换.如果这样的支持变换存在,称偶图FG支集等价,记作FG.类似地,可以定义位置图和连接图的支集变换.

如果两个位置图Fi(i=0,1),有|F0|#|F1|,则说它们是不相交的;如果两个连接图Fi:XiYi,有X0#X1,Y0#Y1且|F0|#|F1|,则说它们是不相交的;如果$F_0^P\# F_1^P$且$F_0^L\# F_1^L,$则说两个偶图Fi(i=0,1)是不相交的.这3种情况都可以写成F0#F1.当两个偶图不相交时,可以把两个偶图水平并排起来.水平并排的运算称作并置(juxtaposition).并置是幺半的(monoidal),即它是可结合的,并且有一个单位元(unit).

对于位置图,两个接口mi(i=0,1)的并置是m0+m1,单位元是0.如果Fi=(Vi,ctrli,prnti):mini是不相交的位置图,它们的并置F0F1:m0+m1n0+n1由下面的公式给出:

${F_0} \otimes {F_1}\mathop {\rm{ = }}\limits^{{\rm{def}}} $(V0$\uplus$V1,ctrl0$\uplus$ctrl1,prnt0$\uplus$prnt'1).
这里,prnt0$\uplus$prnt'1:(m0+m1)$\uplus$V0$\uplus$V1→(n0+n1)$\uplus$V0$\uplus$V1.

l=(m0+m1)\m0,即(m0+m1)\m0=(m0,m0+1,…,m0+m1-1).

$prn{t'_1}(w)\mathop {\rm{ = }}\limits^{{\rm{def}}} \left\{ {\begin{array}{*{20}{l}} {prn{t_1}(w),}&{{\rm{if }}w = {m_0} + i \in l{\rm{ and }}prn{t_1}(i) \in {V_1}{\rm{ or }}w \in {V_1}{\rm{ and }}prn{t_1}(w) \in {V_1}}\\ {{n_0} + j,}&{{\rm{if }}w = {m_0} + i \in l{\rm{ and }}prn{t_1}(i) = j \in {n_1}{\rm{ or }}w \in {V_1}{\rm{ and }}prn{t_1}(w) = j \in {n_1}} \end{array}} \right..$

对于连接图,两个不相交连接图的接口的并置是X0$\uplus$X1,单位元是∅.如果Fi=(Vi,Ei,ctrli,linki):XiYi是不相交的连接图(i=0,1),那么它们的并置F0F1:X0$\uplus$X1Y0$\uplus$Y1由下面的公式给出:

${F_0} \otimes {F_1}\mathop {\rm{ = }}\limits^{{\rm{def}}} $(V0$\uplus$V1,E0$\uplus$E1,ctrl0$\uplus$ctrl1,link0$\uplus$link'1).

对于偶图,两个不相交的接口Ii=〈mi,Xi〉(i=0,1)的并置是〈m0+m1,X0$\uplus$X1〉,单位元是e=〈0,∅〉.如果Fi:IiJi是不相交的偶图(i=0,1),那么它们的并置F0F1:I0$\uplus$I1J0$\uplus$J1由下面的公式给出:

${F_0} \otimes {F_1}\mathop {\rm{ = }}\limits^{{\rm{def}}} F_0^P \otimes F_1^P,F_0^L \otimes F_1^L.$

有了偶图的这些基本概念和算子,就可以将其与范畴的基本理论结合起来.

2 偶图范畴理论

本节的偶图范畴概念来自参考文献[22],从中抽象出性质1、性质2和定理1~定理3,总结几种基本范畴间的关系.

2.1 基本范畴理论

一个范畴(category)C有一个对象集合和一个箭头(arrow,有的用态射(morphism)表示)集合.常用大写字母I,J,K表示对象,小写字母f,g,h表示箭头.每个箭头f都有都一个定义域和值域,它们都是对象.如果定义域和值域是IJ,则写成f:IJ,I=dom(f)和J=cod(f).对于IJ的同态集(homset),即箭头f:IJ的集合,写成C(IJ),或只写(IJ).对每个对象I,有一个单位箭头(identity)idI:II.当I是已知的,简写成id.fg的组合gof满足下面条件:

(C1) gof有定义当且仅当cod(f)=dom(g);

(C2) ho(gof)=(hog)of,当等式的两边都有定义时等式成立;

(C3) idof=f,f=foid.

C3的意思就是,箭头f和单位箭头的组合在它的定义域和值域上总是有定义的.

根据范畴的定义,可得以下两个性质:

性质1. 范畴中单位箭头是唯一的.

性质2. 一般来讲,gof=hofg=h.

弱化范畴定义的条件,得出预范畴(precategory).将范畴中的条件(C1)改为(C1'):如gof有定义,则cod(f)=dom(g).其余部分与范畴定义完全一样,就得到预范畴的定义,用$`C$表示.这样预范畴与范畴的唯一区别是:即使当cod(f)=dom(g)时,fg的组合gof也未必有定义.

给范畴中添加偏张量积(tensor product)⊗算子,它在范畴的对象和箭头上都有定义,且满足关于箭头的结合律(M1):f⊗(gh)=(fg)⊗h,统一律(M2):idef=fide=f和对组合的分配律(M3):(f1g1)o(f0g0)=(f1of0)⊗(g1og0), 这样就构成了偏幺半范畴.再给偏幺半范畴添加对称的箭头gI,J:IJJI,且满足对称的统一律和分配律等,就构成了对称偏幺半范畴(symmetricpartial monoidal,简称spm).

通过支集,可在预范畴的基础上定义s-范畴.s-范畴$`C$是一个预范畴,其中,每个箭头被附上一个有穷支集|f|$\subset $S,S表示支集元素的无穷词汇.而且s-范畴$`C$具有偏张量积、单位元和对称性,就象在spm范畴中一样,且同样要求满足关于箭头的结合律(M1)、统一律(M2)和对组合的分配律(M3)以及关于对称的统一律和分配律等.单位箭头idI和对称箭头YI,J被附上空支集.另外,

(i) 对于f:IJg:J'→K,组合gof有定义当且仅当J=J',且|f|#|g|;那么|gof|=|f|$\uplus$|g|.

(ii) 对于f:I0I1g:J0J1,张量积fg有定义当且仅当IiIj有定义(i=0,1),且|f|#|g|;那么|fg|=|f|$\uplus$|g|.

由此可见:每个spm范畴可被直接看做一个s-范畴,即,支集全为空的s-范畴;相反,隐藏s-范畴支集,通过支集商转换,就可以从任何s-范畴得到spm范畴.具体如下:

对于s-范畴$`C$它的支集商:$C\mathop {\rm{ = }}\limits^{{\rm{def}}} `C/$,它的对象是$`C$的对象,箭头[f]:IJ是同态集(homset)$`C$上的支集等价类[f]:IJ和[g]:JK的组合定义为

$[g] \circ [f]\mathop {\rm{ = }}\limits^{{\rm{def}}} [g' \circ f']{\rm{.}}$
这里,f'$ \in $[f],g'$ \in $[g],且|f'|#|g'|.因此,支集商C是spm范畴.张量积的定义与此类似.C的单位箭头和对称箭头分别是$`C$中id'和${\gamma '_{I,J}}$的单元素集合(singleton)等价类,因为它们有空的支集.可以看出:给预范畴的第1个条件(C1')严格化,即dom(f)=cod(g)⇒fog有定义,预范畴就转为范畴.给预范畴添加张量积⊗,对称箭头gI,J和支集并满足其运算的两个性质,预范畴就转换成s-范畴.给范畴添加张量积⊗对称箭头gI,J并满足其运算性质,范畴就转换成对称偏张量范畴.

函子是两个范畴之间的一个函数F:CD,它使得C中的箭头f:IJ变成在D中的箭头F(f):F(I)→F(J),函子保持组合和单位箭头.如给s-范畴附上一个宽度函子,可以得到如下的宽s-范畴:一个s-范畴$`C$是宽的(wide s-category),如果给它配上一个函子width:$`C \to {\rm{NAT}},$这里的NAT表示有穷序数.偶图有一个由它的节点定义的空间结构,而这个结构一定能够产生一个宽度函子.

2.2 偶图范畴

将偶图的接口作为对象,将图结构看作箭头,偶图可以转换成不同类型的范畴.显然,有下面的定理:

定理1. 具体偶图是预范畴.

定理2. 把具体偶图中的并置运算⊗作为范畴中的张量积,再为其定义对称图:

${\gamma _{m,X,n,Y}}\mathop {\rm{ = }}\limits^{{\rm{def}}} {\gamma _{m,n}},{\gamma _{X,Y}}{\rm{,}}$
具体偶图就转换成s-范畴.

两个偶图FG,如果忽略了它们的闲置边,它们是支持等价的,那么称FG是瘦-支集等价的,写作FG.对于偶图的s-范畴$`BG\left( k \right)$它的瘦-支集商$BG\left( k \right)$${\mathop {\rm{ = }}\limits^{{\rm{def}}} }$$`BG\left( k \right)$/它的对象是$`BG\left( k \right)$的对象,箭头[G]:IJ,是$`BG\left( k \right)$中同态集(IJ)的瘦-支集等价类,BG(K)叫做抽象偶图.同时也定义了一个函子:

[·]$:`BG\left( k \right) \to BG\left( k \right)$

由抽象偶图的定义可得下面的定理:

定理3. 抽象偶图是spm范畴.

综上,它们的关系如图4所示.

Fig.4 Relation diagram of the basic categories 图4 基本范畴关系图
3 偶图代数系统

建立偶图的代数系统,偶图可以由较小的偶图——初等偶图(elementary bigraph),通过组合、张量积和单位偶图的运算构建出来,也是系统构建者进行系统合成的基础.偶图代数可将所有的偶图用代数形式表示出来.为了书写方便,经常在组合(FidI)oG中省略⊗idI.例如,把(mergeidX)oG写成mergeoG,把(idml)o(GX')写成loG.

3.1 初等偶图

表1总结了几个典型初等偶图及其性质.素(prime)偶图和离散偶图(discrete bigraph)对偶图的代数结构和偶图动力学非常重要,一个偶图可被分解成一个纯连接和一个离散素(prime)偶图.而基(ground)偶图g:eI,其定义域是e,记作g:I.

Table 1 Elementary bigraphs表1 初等偶图

定理4(离散范式(discrete normal form)). 考虑到Y的重命名,每个偶图G:〈m,X〉→〈n,Z〉可被表示为

G=(idnl)oD.
这里,λ:YZ是一个纯连接,D:〈m,X〉→〈n,Y〉是离散偶图.每个离散偶图D可以被因子分解为D=a⊗(P0⊗…⊗Pn-1). α是一个重命名,每个Pi都是素偶图,也是离散偶图.

D是基偶图的特殊情况下,结果可以简化成下面的形式:

推论1(基离散范式). 给Y重命名,基偶图g:〈n,Z〉可被表示为g=λod,d=d0⊗…⊗dn-1.这里,λ:YZ是一个纯连接,di是离散素偶图.

3.2 衍生的运算

可以将偶图中的并置运算(张量积)⊗衍生为并行积(parallel product),并行积还可以衍生为合并积(merge product),此外还有嵌套(nesting)运算等.表2总结了几种运算符及其特征.

Table 2 Some operators of bigraphs 表2 一些偶图运算符

由它们的特征可以看出:并行积||是并置⊗的拓广,嵌套是组合的拓广.并置⊗被拓广为并行积||,可得另一种形式的基连接范式.

推论2(基离散范式). 考虑到Y的重命名,基偶图g:〈n,Z〉可以被唯一表示成g=/Yo(p0||…||pn-1).这里,pi是素偶图,而且每个闭连接y$ \in $Y有着多个pi的端口.

4 偶图动力学

偶图动力学是在s-范畴的一般层面上研究偶图的动态理论.在进程演算中,通过反应式$a \to a'$描述进程动力学是很常见的.这些反应定义了所有可能的状态变化,把它推广到s-范畴得出基本反应系统.

4.1 基本反应系统

在s-范畴中,定义域为e的箭a:eI称为基箭头(ground arrow)或者叫智能体(agent),记为a:I.每个反应规则由一对基箭头(r:I,r':I)组成,r称为规则前件(redex),r'称为规则后件(reactum).规则集$`R$在支集变换下是闭合的, 即,如果(r,r')是一个规则,那么每当rsr's'(支集等价)时,(s,s')也是一个反应规则.一个基本的反应系统记为$`C(`R)$,由一个s-范畴$`C$及其上的反应规则集$`R$构成.智能体上的反应关系→是最小(smallest)的,就是说,对某个反应规则(r,r')和(r,r')的上下文c,每当acor,a'cor'时,有aa'.

宽s-范畴中对象的宽度可以表示地点(locality)概念,可将基本反应系统精化为宽反应系统(wide reactive system,简称WRS).于是就能描述一个智能体里面的每个反应发生的地点,这样可以定义一种宽反应关系,它允许反应仅在某些地点发生,从而确定反应可以发生的上下文.

基本反应关系、宽反应关系都没有考虑到智能体间的协作以及它们与环境的交互.一个智能体可以执行的反应,有可能是在它所处环境的协助下执行的,这种反应称为标记变迁(labelled transition).变迁的标记显示环境是如何起协助作用的.

一个宽s-范畴的变迁系统(TS)是一个四元组L=(Agt,Lab,Apl,Tra),其中,Agt是智能体的集合,Lab是标记的集合,AplAgtxLab是应用关系,TraAplxAgt是变迁关系.当(a,l)$ \in $Apl时,称l应用于a.一个三元组(a,l,a')$ \in $Tra称为一个变迁,记为$a\buildrel \ell \over \longrightarrow a'.$如果c是一个箭头,当a$ \in $Agt,每当coa有定义时,则coa$ \in $Agt,那么称c为一个L-上下文.

依据这些术语定义互相似(bisimilarity)的概念,它是一种行为等价关系,即,两个智能体行为一样当且仅当它们“在所有的上下文中反应相同”,也即它们有相同的变迁.在一个基本的反应系统中,互相似可能不是一个同余(congruence)关系,即,它可能不被上下文所保持.但是在一个宽反应系统中,互相似是一个同余.互相似是通过互模拟(bisimulation)定义的.

令$\grave{\ }C$是一个带变迁系统L的范畴.L上的模拟是智能体之间的一个二元关系S,如果aSb,$a\buildrel \ell \over \longrightarrow a'$且l应用于b,那么存在b'使得$b\buildrel \ell \over \longrightarrow b'$且a'Sb'.互模拟就是对称的模拟.互相似是最大的互模拟,用符号~表示,即~=$\cup $Si.

在一个WRS中,一个变迁$a\buildrel \ell \over \longrightarrow a'$是上下文的,如果它的标记l形如$(f,\tilde{J}).$这里,f:IJa的一个上下文,$\tilde{J}$代表J的地点.这个标记应用于智能体a当且仅当foa被定义.一个上下文变迁:$(a,(f,\tilde{J}),{a}')$记为$a\buildrel \ell \over \longrightarrow \tilde Ja',$它有一个宽度为m的基本反应规则$(r,{r}')\in \grave{\ }R\text{,}$使得对于某个活跃的d,即foa=dor.$\tilde{J}$={width(d)(i)|im}且a'dor'.

这就说明可以从一个给定的偶图反应规则集中导出一个变迁系统,而且可以进一步证明导出的变迁系统中的互相似是一个同余.为此,还需了解相对推出的概念.设figi(i=0,1)是范畴C中的箭头,如果dom(f0)= dom(f1),cod(g0)=cod(g1),giofi有定义,且g0of0=g1of1,则称(g0,g1)是(f0,f1)的一个界(bound).如果(h0,h1)也是(f0,f1)的一个界,且存在h,使得hoh0=g0,hoh1=g1,称三元组(h0,h1,h)是(f0,f1)相对于(g0,g1)的一个相对界(relative bound).如果对于任一相对界(k0,k1,k),存在唯一的箭头j使得joh0=k0,joh1=k1koj=h,则称相对界(h0,h1,h)是(f0,f1)相对于(g0,g1) 的一个相对推出(relative pushout,简称RPO).

关于相对推出的详细介绍可以阅读参考文献.而在一个具有RPO和极小变迁的宽反应系统中,智能体间的互相似是一个同余,即,如果a0~a1,那么coa0~coa1,a0,a1代表两个智能体,ca0,a1的任意上下文.

4.2 偶图反应系统(bigraphical reactive system,简称BRS)

偶图反应系统就是一组偶图和一组反应规则.集成现有进程代数理论,偶图反应系统可以导出标记变迁系统.偶图的应用大多与赋类(sorting)关联,通过赋类给控制分类.

位置赋类(place sorting)=(Θ,K,Φ),Θ是一个非空的类(sort)集合,以及一个签名К,它被位置-赋类(place- sorted)的,即给每个控制分配Θ中的一个类.Φ是构造规则,满足同一性和对称性,且被组合和张量积保持.一个接口是-赋类(-sorted)的,如果它的每一个位置都被分配Θ中的一个类.满足Φ的、被扩充的偶图称作-赋类的.它们分别构成了具体-赋类偶图的s-范畴$\grave{\ }BG(\Sigma )$、抽象-赋类偶图的spm范畴BG().

吴怀广等人还进一步做了嵌套赋类的研究[23].BRS是基于赋类的、通过参数实例化定义的.偶图参数化反应规则是一个三元组,形如(R:mJ,R':m'→J,h).这里,R是参数化的前件,R'是参数化的后件,h:m'→m是一个有穷序数的映射.RR'必须是瘦的,并且R必须没有闲置的根或名字.这个规则产生所有基规则(r,r').

这里,r(RidY)od,r'(R'⊗idY)o$\bar{\eta }$(d)且d:〈m,Y〉是离散的.其中,$\bar{\eta }$是实例函数:$\bar{\eta }$〈m,X〉→$\grave{\ }C$〈n,Y〉,即给定一个智能体g:〈m,X〉,离散范式$g=\lambda \circ ({{d}_{0}}\otimes ...\otimes {{d}_{m-1}}),\bar{\eta }(g)\overset{\text{def}}{\mathop{\text{=}}}\,\lambda \circ ({{{d}'}_{0}}||...||{{{d}'}_{n-1}})$,且对每一个$j\in n,{{{d}'}_{j}}$${{d}_{\eta (j)}}$.

BRS是在基本反应系统的基础上,通过参数化的反应规则导出的.赋类上的一个偶图反应系统由$\grave{\ }BG(\Sigma )$及其上的一个参数反应规则集$\grave{\ }R$构成,$\grave{\ }R$在支集等价下是闭合的,即,如果RS,R'S'且$\grave{\ }R$包含(R,R',η),那么它也包含(S,S',η),用$\grave{\ }BG(\Sigma ,\grave{\ }R)$表示BRS.这说明了参数化规则怎样生成基规则.此外,偶图有个宽函子.对每个接口I=〈m,X〉,定义width(I)为m,而对于偶图G:IJ,定义宽度width(G)(i),对所有iwidth(I),有唯一的jwidth(J), 使得对某个$k,j=prnt_{G}^{k}(i)$.容易验证,每个BRS是一个宽反应系统.同时,可以进一步证明BRS中的每个互相似~是一个同余,由BRS导出的特定变迁系统也是一个同余.

5 偶图与其他经典进程代数的关系

作为偶图的目标之一,是为现有的经典代数模型提供统一的框架.每个进程模型,如Petri网、通信顺序进程(CSP)[24]、移动环境演算、p-演算,从语法上定义进程,然后给出它们的交互规则.因此,每个进程模型可由偶图中的两个参量表示:一个是赋类科目(sorting discipline),它包括一个签名,使偶图可以表示模型的形式实体;另一个是一组反应规则,表示它们的行为.这两个参量产生特定模型的一个偶图反应系统.这些经典进程模型可以表示成偶图形式.模型之间的转换通常是一致的,有时是近似一致的.

p-演算的一部分,如不带和式(summation)和复制(replication)的异步p-演算,可以改写成偶图.在偶图中定义一类特殊的连接赋类(link sorting),然后把这类赋类应用到Petri网中[25],Petri网被转换成偶图形式.根据句法结构和反应的基本特征,可将通信系统演算CCS转换成偶图.依据动态签名声明控制“alt”,“send”和“get”都是非活跃的,这样保证反应仅发生它们的顶层.每类CCS的结构同余还可以改写成单个的偶图,可以导出上下文变迁系统.偶图也可以改写移动环境(mobile ambient)演算.移动环境中主要的构造器(constructor)是“amb”,控制元数(arity)为1,代表一个环境(ambient),即一个区域,依据动态签名将其标为活跃的,因此活动可以在里面发生.它的单端口允许环境被命名.其他的构造器代表命令(command)或者能力(capability).通信顺序进程中的算子——并行组合、隐藏、选择、穿插和非确定性选择,可通过汇合展开(confluent unfolding)表示成范式[26].说明这些算子的大多数等价定律不仅对失败等价是正确的,而且对强互相似也是正确的,这为CSP转换成偶图反应系统奠定基础.

此外,进程演算,如CCS、p-演算等,定义了两个进程行为相同的含义,称为行为等价.一个典型的例子是互相似.这种等价通常是一个同余,即进程被插入到任何其他环境中,这种等价性保持不变.证明这种同余通常因模型的不同而不同,Milner用偶图从一定程度上给出了一致性证明,它不仅通过进程演算一致地处理互相似,而且提供了同余的一致性证明方法.

6 偶图的应用与支持工具

偶图已在很多方面取得了应用.偶图的大多数应用基于偶图中节点的签名К,且涉及到一个赋类科目,这个科目决定签名К上的可接受的偶图.目前,偶图的应用表现在偶图建模与分析验证方面,相应的支持工具也相继问世.

6.1 偶图建模与分析

(1) 上下文感知计算

Birkedal等人研究了上下文感知的偶图模型[27],实际是在偶图的基础上定义了柏拉图(Plato-graphical)模型B,他们将上下文感知系统从逻辑上分成3部分:现实世界上下文C、观测上下文或中介P以及计算智能体A,即B=C$\cup $P$\cup $A.CA是分开的,它们仅可以通过中介P进行交互.其实,这是用3个偶图反应系统表示上下文感知系统,通过中介P,有效地解决了上下文中的查询问题.与其不同的是,吴怀广等人用带计算的偶图反应系统描述上下文感知系统[28],就是精化反应规则使其具有计算的能力,拓宽了偶图反应系统的表达能力.

(2) 信息物理系统的建模

美国加州大学伯克利分校的信息物理云计算小组将偶图和Actor[29]模型相结合,用于信息物理系统的形式化建模[30],将虚拟的和物理的构件模型分开,构造出物质世界中的信息实体——BigActor,给出一个结构感知的计算模型.此外,他还用BigActor给异质移动机器人系统的结构进行建模与控制[31],设计出机器人实体的位置和连接的计算模型.BigActor模型间的通信需进一步研究.

(3) 生物信息学建模

Milner等人给偶图的每个反应规则设置一个概率常数ρ.假定反应规则的前件γ在其上下文中可能出现的次数为μ,说明该规则可能引起不同的反应,则由此反应规则引起的反应概率为ρxμ.这样就构造了随机偶图[32].随机偶图可以用于生物系统蛋白质萌芽过程的模拟,它既可以对复杂生物分子反应的形式进行代数表示,也可以对其进行图形化的表示.如果将每个偶图作为一个状态,在特定条件下,随机偶图反应系统可以构成一个连续时间马尔科夫链,因而可由概率模型检验工具进行验证与分析.

(4) 时空建模

移动设备和无线网络的演变涉及到时间和空间的交互.Sevegnani等人将偶图扩展成带共享的偶图[33],偶图成为一个有向无环图,进而用随机共享偶图对IEEE 802.11CSMA/CA RTS/CTS协议进行建模与分析[34],用共享表示重叠信号区域,用随机规则表示常量和均匀分布的超时设定以及常量传播率.这样,可能有信号重叠的无线拓扑结构可以表示成一个带共享的随机偶图,从而可以进行概率模型检验和定量分析.共享偶图还可以用于无线网络的实时验证[35].Stell等人引入一种称为累积(cumulative product)的运算,处理共享祖先的连接,将随着时间变化的空间结构偶图化[36],其实并没有真正地引入时间参数,只是定性地说明随时间而改变的空间结构偶图建模问题,这种模型理论方面的性质有待进一步研究.Lisa等人运用偶图对室内空间中的实体和事件以及它们之间的位置和连接关系定性建模[37],用于室内环境中的任务导航,目前还缺乏推理机制.

(5) 软件体系结构及软件动态演化的建模与分析

常志明等人将偶图用于自适应软件体系结构及软件动态演化的建模与分析[38, 39, 40, 41, 42, 43].汪玲等人给出面向方面软件架构的偶图框架[44, 45].这些研究集中在偶图的建模方面,动态分析部分相对较少.

(6) 业务和服务流程的分析

Zhang等人给出了Web服务建模语言(WSBPEL)的偶图模型[46],Bundgaard等人结合高阶逻辑给出了商业流程的偶图模型[47].Wu等人用偶图构造出服务组合的模型[48].Conforti等人进行了XML的偶图语义分析[49, 50].这方面的验证工作有待进一步研究.

此外,金龙飞等人给出了Seal演算的偶图语义[51].Zhai等人分别讨论了城铁运输的多路选择[52]、城市地铁服务机制的偶图模型[53]以及石油的开采和提炼的偶图建模及偶图反应系统[54].Li等人将偶图模型用于分布式软件环境中的并行事务的处理[55]等.总之,偶图在这些领域的应用主要是给出这些领域的偶图形式化模型,这种模型的完备性、推理和验证都需要进一步研究.

6.2 偶图支持工具

在偶图的支持工具方面,丹麦的哥本哈根IT大学(ITU)设计并实现了偶图编程语言(BPL)[56],提供了偶图及偶图反应系统的操作、模拟等方面的支持,是支持偶图反应系统的一个原型系统.BigRed是一个偶图原型编辑器[57],它是作为Eclipse建模工具版本的一个插件.对于偶图和偶图反应系统,可以使用BigRed很方便地画出图形,并可使用该工具自动生成模型检验器BigMC[58, 59]的输入语言.BigMC是偶图的模型检验工具,可以检验偶图模型是否满足系统规定的属性,如果系统规约未被满足,工具会产生一个反例.这些工具分别是由不同的研究小组开发的,如BigRed是用Java语言开发的,BigMC是用C++语言开发的.此外,有关偶图的其他一些工具正处于设计或开发中.这些偶图工具应适应偶图模型自身的发展而改进,现有的工具需要集成,以便更好地得到应用.

7 小 结

偶图模型是从数学的直觉以及实验两方面结合发展起来的.实验涉及到现实的交互系统,包括自然界,如生物系统,也包括人工系统,如普适计算、商业系统等.偶图用“位置”和“连接”这样的简单思想,将交互系统的数学基础和它们的应用统一起来,并检验了这个假说.偶图具有坚实的数学理论,但是仍然需要规范和进一步研究.

目前研究的大都是纯偶图,其位置和连接在节点集上是相对独立的结构.这种位置和连接的独立性已从形式定义和理论研究两方面进行了探讨,但是应该允许位置和连接中存在某种有用的关联性,比如希望某些连接限定在某些位置内,这样可以限定一个连接只能在一个位置内部使用.这就需要建立绑定(binding)偶图,以满足某些场合需要位置对连接的约束建模;基于带支集s-范畴的偶图,可识别节点、边、名字、根和站点等元素在偶图中的出现情况.一个偶图的支集是其节点、边等元素的集合.这虽然能够导出标记变迁系统,可以定义同余的行为关系,但是s-范畴在位置感知方面的能力是不够的.现有的偶图只能通过支集静态地识别这些元素,而不能通过反应式动态地追踪这些元素的历史状态.为此,需要将偶图反应规则扩充为带参数的追踪反应规则等.现有的随机偶图模型,反应概率是根据反应规则可能匹配的情况计算出来的,缺乏随机反应的一般性.随机概率可考虑应用领域,通过专家经验、数理统计、机器学习等方式获得反应概率.此外,数据在信息科学领域所起的作用越来越大,带数据演算的偶图反应系统值得关注.

偶图已应用于上下文感知、移动计算以及生物系统等的建模和分析.然而偶图的大规模应用尚处于实验阶段,还需要更多的实验来检验.在偶图模型的扩展、应用的拓展、支持工具等方面,都还需要进一步的研究,使其成为普适计算、物联网、信息物理系统等新型计算的理论平台之一,同时也是一个设计、模拟和分析的平台.

参考文献
[1] Milner R. Bigraphical reactive systems. In: Proc. of the 12th Int'l Conf. on Concurrency Theory. LNCS 2154, Heidelberg: Springer-Verlag, 2001. 16-35.[doi: 10.1007/3-540-44685-0_2]
[2] Milner R. A calculus of communicating systems. In: Lecture Notes in Computer Science, Vol.92. Heidelberg: Springer-Verlag, 1980.[doi: 10.1007/3-540-10235-3]
[3] Milner R. Communicating and Mobile Systems: The p-Calculus. Cambridge: Cambridge University Press, 1999.
[4] Cardelli L, Gordon AD. Mobile ambients. Theoretical Computer Science, 2000,240:177-213.[doi: 10.1016/S0304-3975(99)00231-5]
[5] Milner R. Calculi for interaction. Acta Informatica, 1996,33(8):707-737.[doi: 10.1007/s002360050067]
[6] Sewell P. From rewrite rules to bisimulation congruences. Theoretical Computer Science, 2002,274(1):183-230.[doi: 10.1016/S03 04-3975(00)00309-1]
[7] Leifer JJ, Milner R. Deriving bisimulation congruences for reactive systems. In: Proc. of the 11th Int'l Conf. on Concurrency Theory (CONCUR 2000). LNCS 1877, Heidelberg: Springer-Verlag, 2000. 243-258.[doi: 10.1007/3-540-44618-4_19]
[8] Leifer J. Operational congruences for reactive systems [Ph.D. Thesis]. Cambidge: University of Cambridge Computer Laboratory, 2001.
[9] Cattani GL, LeiferJJ, Milner R. Contexts and embeddings for closed shallowaction graphs. Technical Report, 496, University of Cambridge Computer Laboratory, 2000.
[10] Sassone V, Sobocinski P. Deriving bisimulation congruences: A 2-categorical approach. Electronic Notes in Theoretical Computer Science, 2002,68(2):105-123.[doi: 10.1016/S1571-0661(05)80367-6]
[11] Sassone V, Sobocinski P. Locating reaction with 2-categories. Theoretical Computer Science, 2005,333(1):297-327.[doi: 10.1016/j.tcs.2004.10.025]
[12] Kelly GM. Basic concepts of enriched category theory. In: Proc. of the Republished (2005) in Theory and Applications of Categories 10. LNM 64, Cambridge: Cambridge University Press, 1982. 1-136.
[13] Lawvere FW. Metric spaces, generalized logic, and closed categories. Rendiconti del Seminario Matématico e Fisico di Milano, 1973,43(1):135-166.
[14] Ehrig H. Introduction to the algebraic theory of graph grammars. In: Proc. of the Graph Grammars and their Application to Computer Science and Biology. LNCS 73, Heidelberg: Springer-Verlag, 1979. 1-69.[doi: 10.1007/BFb0025714]
[15] Meseguer J, Montanari U. Petri nets are monoids. Information and Computation, 1990,88(2):105-155.[doi: 10.1016/0890-5401(90) 90013-8]
[16] Bundgaard M, Sassone V. Typed polyadic pi-calculus in bigraphs. In: Proc. of the 8th ACM SIGPLAN Int'l Conf. on Principles and Practice of Declarative Programming. ACM, 2006. 1-12.[doi: 10.1145/1140335.1140336]
[17] Jensen OH. Mobile Processes in Bigraphs. 2006. http://www.cl.cam.ac.uk/-rm135/Jensen-monograph.html
[18] Jensen OH, Milner R. Bigraphs and transitions. In: Proc. of the 30th SIGPLANSIGACT Symp. on Principles of Programming Languages. New Orleans: ACM Press, 2003. 38-49.[doi: 10.1145/604131.604135]
[19] Jensen OH, Milner R. Bigraphs and mobile processes (revised). Technical Report, UCAM-CL-TR-580, University of Cambridge Computer Laboratory, 2004.
[20] Milner R. Pure bigraphs: Structure and dynamics. Information and Computation, 2006,204(1):60-122.[doi: 10.1016/j.ic.2005. 07.003]
[21] Perrone G, Debois S, Hildebrandt T. Bigraphical refinement. In: Proc. of the Refinement Workshop 2011, EPTCS 55. 2011. 20-36.[doi: 10.4204/EPTCS.55.2]
[22] Milner R. The Space and Motion of Communicating Agents. Cambridge: Cambridge University Press, 2009.
[23] Wu HG, Jin BH, Gan Y, Wu GQ. Bigraphical reactive systems based on nested sort. Computer Science, 2012,39(9):143-151 (in Chinese with English abstract).
[24] Hoare CAR. Communicating sequential processes. Communications of the ACM, 1978,21(8):666-677.
[25] Leifer JJ, Milner R. Transition systems, link graphs and Petri nets. Mathematical Structures in Computer Science, 2006,16(6): 989-1047.
[26] Bundgaard M, Milner R. Unfolding CSP. In: Proc. of the Reflections on the Work of C.A.R. Hoare History of Computing 2010. Heidelberg: Springer-Verlag, 2010. 213-228.[doi: 10.1007/978-1-84882-912-1_10]
[27] Birkedal L, Debois S, Elsborg E, Hildebrandt T, Niss H. Bigraphical models of context-aware systems. In: Proc. of the 9th Int'l Conf. on Foundations of Software Science and Computation Structure. LNCS 3921, Berlin, Heidelberg: Springer-Verlag, 2006. 187-201.[doi: 10.1007/11690634_13]
[28] Wu HG, Ji HL, Wu GQ, Miao Y. Calculational bigraphical model of context-aware systems in ubiqutious computing environment. Computer Science, 2012,39(1):109-114 (in Chinese with English abstract).
[29] Agha G. Actors: A Model of Concurrent Computation in Distributed Systems. Cambridge: MIT Press, 1986.
[30] Pereira E, Kirsch C, Sengupta R, de Sousa JB. BigActors—A model for structure-aware computation. In: Proc. of the ACM/IEEE 4th Int'l Conf. on Cyber-Physical Systems (ICCPS 2013). 2013. 199-208.[doi: 10.1145/2502524.2502551]
[31] Pereira1 E, Potiron1 C, Kirsch CM, Sengupta R. Modeling and controlling the structure of heterogeneous mobile robotic systems: A bigactor approach. 2013. http://cpcc.berkeley.edu/papers/Modeling.pdf
[32] Krivine J, Milner R, Troina A. Stochastic bigraphs. In: Proc. of the 24th Int'l Conf. on Mathematical Foundations of Programming Systems. 2008. 73-96.[doi: 10.1016/j.entcs.2008.10.006]
[33] Sevegnani M, Calder M. Bigraphs with sharing. Theoretical Computer Science, 2015,577:43-73.
[34] Calder M, Sevegnani M. Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing. Formal Aspects of Computing, 2014,26(3):537-561.[doi: 10.1007/s00165-012-0270-3]
[35] Calder M, Koliousis A, Sevegnani M, Sventek J. Real-Time verification of wireless home networks using bigraphs with sharing. Science of Computer Programming, 2014,80:288-310.[doi: 10.1016/j.scico.2013.08.004]
[36] Stell J, Del Mondo G, Thibaud R. Spatio-Temporal evolution as bigraph dynamics. In: Proc. of the COS IT 2011. LNCS 6899, Berlin, Heidelberg: Springer-Verlag, 2011. 148-167.[doi: 10.1007/978-3-642-23196-4_9]
[37] Walton LA, Worboys M. A qualitative bigraph model for indoor space. In: Proc. of the GIScience 2012. LNCS 7478, Berlin, Heidelberg: Springer-Verlag, 2012. 226-240.[doi: 10.1007/978-3-642-33024-7_17]
[38] Chang ZM, Mao XJ, Qi ZC. Applying bigraph theory to self-adaptive software architecture. Chinese Journal of Computers, 2009, 32(1):97-106 (in Chinese with English abstract).[doi: 10.3724/SP.J.1016.2009.00097]
[39] Chen HL, Li RF. Analyzing and verifying method for dynamic evolution software based on bigraphical theory. Journal of Chinese Computer Systems, 2010,12(12):2305-2309 (in Chinese with English abstract).
[40] Chang ZM, Mao XJ, Qi ZC. An approach based on bigraphical reactive systems to check architectural instance conforming to its style. In: Proc. of the 1st Joint IEEE/IFIP Symp. on Theoretical Aspects of Software Engineering (TASE 2007). 2007. 57-66.[doi: 10.1109/TASE.2007.9]
[41] Chang ZM, Mao XJ, Qi ZC. Towards a formal model for reconfigurable software architectures by bigraphs. In: Proc. of the 7th Working IEEE/IFIP Conf. on Software Architecture. 2008. 331-334.[doi: 10.1109/WICSA.2008.17]
[42] Chang ZM, Mao XJ, Qi ZC. Formal analysis of architectural policies of self-adaptive software by bigraph. In: Proc. of the 9th Int'l Conf. for Young Computer Scientists. 2008. 118-123.[doi: 10.1109/ICYCS.2008.213]
[43] Liu PP, Zhang Y, Mo Q, Shao Z. Research on software evolution process model based on bigraph theory. Application Research of Computers, 2013,5(30):1423-1426 (in Chinese with English abstract).
[44] Wang L, Rong M, Zhang GQ, Wang S. Research on bigraph based aspect oriented dynamic software architecture evolution. Computer Science, 2010,37(9): 137-140 (in Chinese with English abstract).
[45] Yang X, Li T. An AOP framework supporting dynamic evolution. Computer Engineering, 2012,38(19):52-55 (in Chinese with English abstract).
[46] Zhang M, Shi L, Zhu L, Wang Y, Feng L, Pu F. A bigraphical model of WSBPEL. In: Proc. of the 2nd Joint IEEE/IFIP Symp. on Theoretical Aspects of Software Engineering. IEEE Computer Society, 2008. 117-120.[doi: 10.1109/TASE.2008.47]
[47] Bundgaard M, Glenstrup A, Hildebrandt T, Højsgaard E, Niss H. Formalising higher-order mobile embedded business processes with binding bigraphs. In: Proc. of the 10th Int'l Conf. on Coordination Languages. LNCS 5052, Berlin, Heidelberg: Springer-Verlag, 2008. 83-99.[doi: 10.1007/978-3-540-68265-3_6]
[48] Wu HG, Wu GQ, Wan L. Bigraphical model of service composition in ubiquitous computing environments. In: Proc. of the 2nd Conf. on Environmental Science and Information Application Technology. 2010. 658-662.[doi: 10.1109/ESIAT.2010.556 8325]
[49] Conforti G, Macedonio D, Sassone V. Bigraphical logics for XML. In: Proc. of the 13th Italian Symp. on Advanced Datebase Systems (SEBD). 2005. 392-399.
[50] Hildebrandt T, Niss H, Olsen M. Formalising business process execution with bigraphs and reactive XML. In: Proc. of the 8th Int'l Conf. on Coordination Models and Languages. LNCS 4038, Heidelberg: Springer-Verlag, 2006. 113-129.[doi: 10.1007/11767954 _8]
[51] Jin LF, Liu L. Bigraphical semantics of seal calculus. Chinese Journal of Computers, 2008,31(3):522-528 (in Chinese with English abstract).
[52] Zhai HW, Zhang WS, Cui LC, Liu HB, Abraham A. A bigraph model for multi-route choice in urban rail transit. In: Proc. of the 2011 Int'l Conf. on Communication Systems and Network Technologies. IEEE Computer Society Press, 2011. 699-703.[doi: 10. 1109/CSNT.2011.166]
[53] Zhai HW, Zhang WS, Cui LC, Shi JS, LI H.Toward formal description to metro services mechanism based on bigraph models. In: Proc. of the 2011 Int'l Conf. of Soft Computing and Pattern Recognition (SoCPaR). IEEE, 2011. 285-289.[doi: 10.1109/SoCPaR. 2011.6089257]
[54] Zhai HW, Zhang WS, Cui LC, Xie X, Zhang XG. High-Confidence petroleum industrial critical systems research based on bigraphical models. In: Proc. of the 2011 Int'l Conf. of Soft Computing and Pattern Recognition (SoCPaR). IEEE, 2011. 290-295.[doi: 10.1109/SoCPaR.2011.6089258]
[55] Li CY, Man JF, Wang ZB. An improved method for transaction footprints stripping with bigraph system. Journal of Software, 2012, 7(9):2141-2148.[doi: 10.4304/jsw.7.9.2141-2148]
[56] Birkedal L, Hildebrandt T. Bigraphical programming languages. Laboratory for Context-Dependent Mobile Communication, IT University, 2004.
[57] https://github.com/ale-f/big-red
[58] Perrone G, Debois S, Hildebrandt TT. A model checker for bigraphs. In: Proc. of the 27th Annual ACM Symp. on Applied Computing (SAC 2012). New York: ACM, 2012. 1320-1325.[doi: 10.1145/2245276.2231985]
[59] Perrone G, Debois S, Hildebrandt TT. A verification environment for bigraphs. Innovations in Systems and Software Engineering, 2013,9(2):95-104.[doi: 10.1007/s11334-013-0210-2]
[23] 吴怀广,金保华,甘勇,毋国庆.基于嵌套赋类的Bigraph 反应系统模型.计算机科学,2012,39(9):143-151.
[28] 吴怀广,姬厚灵,毋国庆,苗玥.普适环境中上下文感知的带演算的Bigraphs 描述.计算机科学,2012,39(1):109-114.
[38] 常志明,毛新军,齐治昌.Bigraph 理论在自适应软件体系结构上的应用.计算机学报,2009,32(1):97-106. [doi: 10.3724/SP.J.1016.2009.00097]
[39] 陈洪龙,李仁发.基于Bigraph 理论的动态演化软件相关特性分析与验证方法.小型微型计算机系统,2010,12(12):2305-2309.
[43] 刘培培,章勇,莫启,邵振.一种基于Bigraph 理论的软件演化过程模型研究.计算机应用研究,2013,5(30):1423-1426.
[44] 汪玲,戎玫,张广泉,王昇.基于Bigraph 的面向方面动态软件体系结构演化研究.计算机科学,2010,37(9):137-140.
[45] 杨曦,李彤.一种支持动态演化的AOP 框架.计算机工程,2012,38(19):52-55.
[51] 金龙飞,刘磊.Seal 演算的偶图语义.计算机学报,2008,31(3):522-528.