偶图范畴的规范描述

范畴论是抽象地处理数学结构以及结构之间联系的一门数学理论。以范畴论为数学基础的偶图,为普适信息系统提供一个设计、模拟和分析的平台。然而偶图的范畴理论缺少规范的描述,一些概念术语的定义甚至有错误的地方。改进了偶图基本签名的定义,校正了位置图并置运算的定义,揭示了预范畴、范畴、s-范畴、对称偏幺半范畴之间的联系,给出了构造偶图范畴的算法,以便进一步研究偶图理论及其应用。     

Seal演算的偶图语义

偶图反应系统是一种新的理论工具,其基础是一种强调位置和连接的移动计算图形化模型--偶图,偶图范化了π演算和移动Ambient演算的特征,能够表示具有位置和移动性质的复杂系统.偶图反应系统为普适计算不同层次的设计和实现提供了统一的建模框架.Seal演算是一种用于描述移动计算的进程语言,具有良好的安全性质.文中给出了一种不带复制进程表达式的Seal演算的偶图表示,分析了该Seal演算与其偶图表示间的结构对应和操作对应.本研究扩展了偶图理论的应用范围,展示了偶图理论在描述安全演算方面的能力,为在偶图反应系统框架下研究Seal演算的性质和应用奠定了基础.     

值域为坡代数的加权图和模糊图的范畴关系

坡代数是元素的乘法小于等于每个因子的加法幂等的半环。以坡代数为取值域,证明了加权图范畴可以作为余反射子范畴嵌入到模糊图范畴中去;如果坡代数的乘法有单位元,则这种嵌入还具有反射性。     

计算机科学中的范畴数据类型的研究综述

范畴数据类型是指以范畴论为数学理论基础研究数据类型的描述、计算、语义和应用。早期的范畴数据类型研究以归纳数据类型为主,采用代数从归纳的角度研究有限数据类型的构造语义和递归性质。近年来,归纳数据类型的对偶概念——共归纳数据类型逐渐引起计算机科学工作者的关注与研究,他们采用共代数从观察的角度研究无限数据类型的行为语义和共递归性质。利用范畴论可以为数据类型研究提供统一的数学理论基础,并将代数和共代数中的各种重要研究成果有机地融合在一起,如语法构造与动态行为、递归与共递归、同余与互模拟等。目前,范畴数据类型已经在程序语言、计算描述、理论证明器和并行计算等领域得到广泛的应用。对范畴数据类型的基本概念、数学理论基础、逻辑基础及应用等方面的最新研究成果进行介绍,以引起国内外相关研究领域的学者对计算机科学中的范畴数据类型理论的关注。     

多部图的匹配算法研究

本文给出了一个多部图的商匹配问题的定义,提出了求解多部图商匹配问题的一个算法。该算法使用圈与割集中偶图的交相结合的方法,利用求二部图的最大匹配算法,求解多部图的最大商匹配问题。     

准最佳三进阵列偶

最佳二进阵列在通信领域中有着广泛的应用,但由于其存在体积的限制,制约了它的应用范围,针对这种现象,提出了一种新的最佳离散信号,即准最佳三进阵列偶,给出了准最佳三阵列偶的定义和变换性质,研究了它的组合允许条件,分析了它与准最佳二进阵列偶、准最佳屏蔽二进阵列偶以及最佳三进阵列偶之间的关系,并用计算机搜索出部分小体积的准最佳三进阵列偶。实验结果显示准最佳三进阵列偶的存在范围非常广泛,为通信工程的应用提供了更多的选择。     

粗代数研究

在粗糙集的代数方法研究中,一个重要的方面是从粗糙集的偶序对((下近似集,上近似集()表示入手,通过定义偶序对的基本运算,从而构造出相应粗代数,并寻找能够抽象刻画偶序对性质的一般代数结构.其中最有影响的粗代数分别是粗双Stone代数、粗Nelson代数和近似空间代数,它们对应的一般代数结构分别是正则双Stone代数、半简单Nelson代数和预粗代数.通过建立这些粗代数中算子之间的联系,证明了:(a) 近似空间代数可转化为半简单Nelson代数和正则双Stone代数;(b) 粗Nelson代数可转化为预粗代数和正则双Stone代数;(c) 粗双Stone代数可化为预粗代数和半简单Nelson代数,从而将3个不同角度的研究统一了起来.     

子共代数与共同余共关系

共代数方法是近几年来理论计算机科学的研究热点之一,在并行计算模型、自动机及面向对象技术的理论基础方面有着广泛的应用.以范畴理论为工具讨论子共代数的性质,特别是集合范畴上的子共代数的性质,证明了集合范畴上的子共代数都是正则子共代数.进一步利用共同余共关系与子共代数之间的对应,给出了集合范畴上共生成子共代数的一种构造方式.     

低相关区序列偶集的构造方法

提出了两种新的构造低相关区(LCZ)序列偶集的方法.一种方法是基于二元二值周期自相关序列与正交矩阵偶,利用交织技术生成一个长LCZ序列,再将其扩展为一个低相关区序列偶集;另一种方法是基于二元二值周期自相关序列偶与正交矩阵偶,利用交织生成一个长LCZ序列偶,再将其扩展为低相关区序列偶集.对构造方法讲行了理论证明和举例.由于LCZ序列偶集的存在范围更广,所以可以为实际的工程应用提供更多的选择.     

书本图的偶匹配可扩性

该文得出的主要结论是:书本图Bm是偶匹配可扩的当且仅当书本图Bm同构于B1或者B2.并且书本图Bm是基本的.     

基于嵌套赋类的Bigraph反应系统模型

针对Bigraph反应系统中位置图控制间的嵌套关系问题,提出了一个赋类的Bigraph扩展模型。在利用标签范畴Scat(K)给出嵌套赋类位置图定义的基础上,讨论了嵌套赋类位置图的相关性质,给出了嵌套赋类位置图中RPO的构建、证明,以及同前推出IPO的一致性条件的定义、证明。     

Real-time verification of wireless home networks using bigraphs with sharing

Home wireless networks are difficult to manage and comprehend because of evolving locality, co-locality, connectivity and interaction. We define formal models of home wireless network infrastructure and policies and investigate how they can be used in a network management system designed to provide user-oriented support. We model spatial and temporal behaviour of network interactions and user-initiated network policies and define an online framework for generation of models from network and user-initiated events. The models are expressed in an extension to Milnerʼs bigraphical reactive systems. Analysis of the models is carried out in real-time by a bespoke bigraph reasoning system based on checking predicates, which is encoded as bigraph matching. Real-time model generation and analysis is implemented on the experimental Homework system router and trialled with synthetic and actual network data.     

A bigraphical model for specifying cloud-based elastic systems and their behaviour

The few recent years have witnessed the appearance of a new kind of self-adaptive systems called cloud based-elastic systems. These systems are particularly appealing for their ability to maintain a decent quality of service and reduce a system’s operating cost at the same time. They achieve this by dynamically adjusting resources allocation in terms of elasticity. Meanwhile, complexity of structural and behavioural aspects related to cloud-based elastic systems increase the difficulty of designing and developing such systems. In this paper, we address this challenge by proposing a formal approach based on bigraphical reactive systems for modelling both structural and behavioural aspects of cloud-based elastic systems. In particular, we represent their behaviour in terms of client/application interactions and elasticity methods at different levels using bigraphical reaction rules. The feasibility of the proposed approach is illustrated through a motivating example running on the top of an Amazon Elastic Compute Cloud (EC2) infrastructure.     

Matching of Bigraphs

We analyze the matching problem for bigraphs. In particular, we present a sound and complete inductive characterization of matching of binding bigraphs. Our results pave the way for a provably correct matching algorithm, as needed for an implementation of bigraphical reactive systems.     

Optimization‐based group performance deducing

Large‐scale group performance animation has been an important research topic because of its diverse range of applications including virtual rehearsal and film production. Animating hundreds of virtual actors as what the director wishes is a tough task. In this paper, we address this challenge by introducing an optimization method that generates large‐scale group performance by deducing a small‐scale one with fewer actors. We introduced group motion bigraph technique and transformed the motion‐deducing problem into a constrained optimization problem. A solving process is then presented to automatically obtain the motion of the large group with velocity constraints. Moreover, an interactive system of constructing the group motion bigraph has been implemented, which provides flexible edit and control on deducing group motion. The animation results show that our method is competent for deducing large‐scale group performance from only several motion clips performed by small groups. Copyright © 2013 John Wiley & Sons, Ltd.     

归纳数据类型的范畴论方法

归纳数据类型是类型论研究的重要分支,传统的数理逻辑或代数方法侧重于描述归纳数据类型的有限语法构造,在语义性质与归纳规则的分析与设计方面存在一定的不足.基于范畴论的方法,在集合范畴的框架内给出谓词的形式化定义,分析谓词范畴与代数范畴的构成与性质,并探讨集合范畴上自函子到谓词范畴上自函子的提升,最后利用伴随函子及其伴随性质深入分析了归纳数据类型具有普适意义的归纳规则.     

Fibrations理论在索引归纳数据类型语法构造中的应用

应用Fibrations理论对索引归纳数据类型的语法构造进行了研究。提出了索引fibration及其真值与内涵函子的定义,构造了索引与代数范畴,利用折叠函数与伴随函子等工具构造了索引范畴中一类相对复杂的索引归纳数据类型,辅以实例进行了简要分析,并通过相关工作的论述指出了Fibrations理论研究方法的优势。     

Categories of fuzzy sets

In this paper we look at two categories, the category of fuzzy subsets and a quotient category / of fuzzy sets. The category / is an extension of the category of sets, and the standard constructions in fuzzy set theory arise naturally within this category. This paper was presented at a workshop in the Czech Republic, hosted by Professors Vilém Novák and Irina Perfilieva. I thank them for their warm hospitality and the opportunity to participate in an inspiring workshop.     

A verification environment for bigraphs

We present the BigMC tool for bigraphical reactive systems that may be instantiated as a verification tool for any formalism or domain-specific modelling language encoded as a bigraphical reactive system. We introduce the syntax and use of BigMC, and exemplify its use with two small examples: a textbook “philosophers” example, and an example motivated by a ubiquitous computing application. We give a tractable heuristic with which to approximate interference between reaction rules, and prove this analysis to be safe. We provide a mechanism for state reachability checking of bigraphical reactive systems, based upon properties expressed in terms of matching, and describe a checking algorithm that makes use of the causation heuristic.     

Rare category exploration

Rare category discovery aims at identifying unlabeled data examples of rare categories in a given data set. The existing approaches to rare category discovery often need a certain number of labeled data examples as the training set, which are usually difficult and expensive to acquire in practice. To save the cost however, if these methods only use a small training set, their accuracy may not be satisfactory for real applications. In this paper, for the first time, we propose the concept of rare category exploration, aiming to discover all data examples of a rare category from a seed (which is a labeled data example of this rare category) instead of from a training set. To this end, we present an approach known as the FRANK algorithm which transforms rare category exploration to local community detection from a seed in a kNN (k-nearest neighbors) graph with an automatically selected k value. Extensive experimental results on real data sets verify the effectiveness and efficiency of our FRANK algorithm.