Goguen命题逻辑系统公理化扩张的Γ-k真度理论及性质

本文首先对n值Goguen命题逻辑进行公理化扩张,Goguen_~,△,记为Π_~,△.利用公式的诱导函数给出公式在k（k任取~或△）连接词下相对于局部有限理论Γ的Γ-k真度的定义;讨论了Π_~,△中Γ-k真度的MP规则、HS规则等相关性质;最后,在Π_~,△中定义了两公式间的Γ-k相似度与Γ-k伪距离,得到了公式在连接词下相对于局部有限理论Γ的Γ-k相似度与Γ-k伪距离所具有的一些良好性质.     

公交网络下的一种费用限制最小时态路径查询索引

私人交通网络下的最短路径查询主要考虑路径长度、行驶时间等因素,而公共交通网络下的路径查询需要考虑路径上相邻的边的时间顺序约束以及路径的费用.研究了公共交通网络下3种查询：给定起点、终点、时间区间和费用上限,查找在时间区间内不超过费用上限的最早到达路径、最晚出发路径和最短耗时路径.首先给出一种Dijkstra变种算法Dijk-CCMTP,在此基础上给出3类查询的查询算法.然后提出一种高效的索引结构ACCTL（approximate cost constrained time labelling）.ACCTL采用Dijk-CCMTP对图中的每个顶点预先计算部分从该顶点出发的和到达该顶点的基本路径.对于任意从起点s到终点d的查询,可以采用类似数据库表连接的方式从ACCTL中连接从a出发的和到达d的路径生成近似解,避免遍历原图搜索路径.ACCTL建立索引的时间复杂度是O（|V|·△_max·|E|·（log|E|+△_max））,其中,|V|表示顶点数,|E|表示边数,△_max表示顶点的最大度数.实验验证ACCTL索引支持的查询速度比Dijkstra的变种算法的查询速度快2~3个数量级,并分析了影响建立索引时间和空间大小的因素.     

高阶类型化软件体系结构建模和验证及案例

根据权威统计数据，软件测试中发现的70%以上的错误由需求获取或体系结构设计引起.因此，应用软件体系结构在设计阶段的正确性验证非常重要.现有的软件体系结构设计方法不支持需求满足验证，需求满足验证需要其他验证工具的支持.面向主流Web应用软件的体系结构设计及其需求满足验证，提出了一种高阶类型化软件体系结构建模和验证语言（SAML）与软件体系结构建模和验证方法（SAMM）.SAML语言通过定义类型和项的语法及语义，描述软件体系结构中类型和对象的构造，通过定义类型规则及其类型检查算法来判定Γ|-t：T和Γ|-R（T₁，T₂）是否成立.SAMM给出了软件体系结构建模范式，包括构建接口类型M_cls（type interface）、组件M_cmpt（component）、容器M_cont（container）、框M_frm（frame）和框架M_frwk（framework）这5层建模过程，以及生成层内与层间类型之间关系对应的类型规则，同时定义了接口类型方法调用图（G_SA）用以刻画软件体系结构设计要求，定义了类型序列及其正确性用以刻画需求期望的性质，并给出了相应的验证算法.设计实现了基于该方法的原型工具系统SAMVS，其中，模型编辑环境支持应用软件的设计过程，验证环境支持设计满足需求的自动化验证.通过一个实际案例，完成了一个较大规模"互联网+"应用软件系统的体系结构建模和验证.     

γ演算到Action演算的转换

Action演算簇(action calculi)作为描述不同并发交互行为的数学框架,可以表示一大类具有某些相同特性的并发形式化模型.试图把(演算(一种基于约束的高阶并发计算模)也包含在action演算簇的框架下.首先定义了一个具体的action演算AC(K_γ),然后给出了从(演算到AC(K_γ)转换的形式描述,最后在定义AC(K_γ)的可观察性、弱互模拟关系和弱等价关系的基础上,以(演算为中间表示,证明了这种转换保持了(演算的弱行为等价性.研究表明,action演算簇可以表示基于约束的并发模型,从而充分说明了action演算簇的描述能力,并且为在action演算簇框架下把(演算与其他并发模型结合并进行比较提供了前提.     

关于并发系统分支互模拟关系发散性保持的研究

带发散性说明的分支互模拟是van Glabbeek和Weijland提出的一个概念,并被用来定义等价关系.该等价关系应该是最弱的一个发散性保持的并且满足分支互模拟性质的等价关系.然而在概念提出时并没有提供这些重要性质的证明,并且我们认为在原定义的基础上这个证明是不显然的.本文通过co-induction的手段利用染色迹的概念定义了着色完全迹等价,并证明该等价关系是最弱的一个保持发散的并且满足分支互模拟性质的等价关系.然后我们证明了着色完全迹等价关系和≈_b^△是相同的,因而补充了van Glabbeek和Weijland的工作,即证明了≈_b^△是最弱的一个保持发散的并且是满足分支互模拟性质的等价关系.     

有中断时间代价的一致并行机抢先调度问题

提出了一种具有中断时间代价的抢先调度问题(P|ptmn(δ)|C_max):在抢先调度中,一个任务发生一次中断,其总的执行时间会增加一个δ.该问题在工程任务分配、分布式计算和网络通信等实际问题中有着广泛的应用背景.证明了这是一个NP-hard问题,给出了一个时间复杂度为O(nlogn+m)的脱线近似算法LPT-Wrap,其近似比小于等于1.40825,并分析了P|ptmn(δ)|C_max的在线特性,给出一个线性时间复杂度的在线近似算法,其竞争比为2.     

P2-Packing问题参数算法的改进

P₂-Packing问题是一个典型的NP难问题.目前这个问题的最好结果是时间复杂度为O^*(2^5.301k)的参数算法,其核的大小为15k.通过对P₂-packing问题的结构作进一步分析,提出了改进的核心化算法,得到大小为7k的核,并在此基础上提出了一种时间复杂度为O^*(2^4.142k)的参数算法,大幅度改进了目前文献中的最好结果.     

QBF问题中隐蔽集的求解过程

隐蔽集作为QBF问题的重要结构之一,能使QBF这一难求解问题变得更加简单. QBF问题中隐蔽集的求解相当复杂且难以理解. 为了使读者更好的理解QBF问题中隐蔽集的求解过程,本文对QBF问题中隐蔽集的求解过程进行深入研究,结合实例计算变量的深度、选择符合条件的变量X并计算其对应的三角依赖变量集D_ψ^Δ（x）,根据B=B∪{x}=x和ψ''=ψ-D_ψ^Δ（x）的思想求解出问题的隐蔽集,希望本文能为该领域的相关研究人员提供一定的参考.     

有Mate-Pairs的个体单体型MSR问题的参数化算法

个体单体型MSR(minimum SNP removal)问题是指如何利用个体的基因测序片断数据去掉最少的SNP(single-nucleotide polymorphisms)位点,以确定该个体单体型的计算问题.对此问题,Bafna等人提出了时间复杂度为O(2^kn²m)的算法,其中,m为DNA片断总数,n为SNP位点总数,k为片断中洞(片断中的空值位点)的个数.由于一个Mate-Pair片段中洞的个数可以达到100,因此,在片段数据中有Mate-Pair的情况下,Bafna的算法通常是不可行的.根据片段数据的特点提出了一个时间复杂度为O((n-1)(k₁-1)k₂2^2h+(k₁+1)^2h+nk₂+mk₁)的新算法,其中,k₁为一个片断覆盖的最大SNP位点数(不大于n),k₂为覆盖同一SNP位点的片段的最大数(通常不大于19),h为覆盖同一SNP位点且在该位点取空值的片断的最大数(不大于k₂).该算法的时间复杂度与片断中洞的个数的最大值k没有直接的关系,在有Mate-Pair片断数据的情况下仍然能够有效地进行计算,具有良好的可扩展性和较高的实用价值.     

网格多处理机的一种改进的子网分配算法

子网分配问题是指识别并分配一个空闲的、满足指定大小要求的节点机.首先,提出了网格结构中一种新的具有O(N²_a·1og₂N_a)时间复杂度的空闲子网搜索算法,它优于现有的O(N³_a)时间复杂度的搜索算法.然后,用该算法对基于保留因子的最佳匹配类子网分配算法——RF(reservation factor)算法进行了改进,得到了