可满足赋值算子的设计与实现

在很多应用领域中,我们都需要获取逻辑公式所有无冗余的可满足解集合,即集合中的任意两个解不能互相蕴涵。为了获取无冗余解集合,本文提出了两种实现方案。由于二叉决策图BDD具有对逻辑公式的高效表达特性,因此两种方案都是在逻辑公式转换成BDD的基础上实现的[1]。一种方案是直接对该BDD进行遍历,获取从根节点到终端节点1的所有路径集合,然后借助一致性理论获取无冗余解的一致性算子的实现。另一种方案借助香农分解定理对BDD先进行逐层分解,然后对分解后的BDD再进行一致性运算的可满足赋值算子的实现。本文最后对两种方案的实验效果进行对比分析。     

消防通信调度指挥系统中地理信息系统的建设

现代化消防通信调度指挥系统是一个高科技。多学科综合应用的系统，其中地理信息系统具有重要的位置，在消防作战过程中，时间是最关键的因素，地理信息系统占有空间上可视性，一些作战要素能通过地理信息快速的查询到，从而有助于有效的扑灭火灾。一、消防地理信息要素概括来讲，在消防地理信息系统中，信息要素可分为点、线、面。标注四种类型，这些类型要素都具有一个或多个空间坐标，同时包含其特定的属性。具体说明如下：l、点型要素：比较重要的点型要素有：单位、消火栓、建筑物等。单位属性：具有一个空间坐标值，同时包含有单位名…     

基于模型检查的XMLSchema特征提取

XQuery用于查询XML文档,对XQuery查询优化有助于提高查询效率,有重要的研究意义.树模式把XQuery表示成树结构的查询,如何基于XMLSchema对树模式进行优化是当前的研究热点,需要利用XMLSchema的一些特征进行树模式优化,因此如何自动提取XMLSchema的特征是需要解决的问题.提出基于模型检查的XMLSchema特征提取方法.首先把XMLSchema转换成Schema图,进而转换成模型检查器NuSMV的输入模型,从而可以对时态逻辑公式表示的XMLSchema特征进行检查,提取的孩子关系以及子孙关系特征可以用于树模式优化.     

SET证书申请协议在SPV下的自动化验证及改进

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.     

利用城市GIS中数据信息进行消防站的选址

本文根据公安部部颁标准对消防站的选址要求，给出了利用城市地理信息系统（GIS）对消防站选址的算法。     

最经济路线规划算法研究

在城市的公交网络系统中,如果通过乘公交车从点X到点Y,那么如何乘坐(可能需要换乘公交车),使得花费最少?这是Datar和Ranade提出的一个开问题。该文通过对城市公交网络系统的分析,给出了一个解决该问题的时间复杂度为多项式的算法。另外文章还讨论了当找到一条费用最小的乘车路线规划时,如何乘坐公交车使得能最快地到达目的地,并给出了时间复杂度为多项式的算法。     

利用OBDD编码的快速二值图算法(英文)

对利用有序二元判定图 OBDD 编码二值图像进行了研究,该方法可以节约大量的空间,并在此基础上,提出了各种二值图的算法,包括解码和集合运算(并、交、差、对称差、包含和互补)。实验结果表明这种基于OBDD 编码的方法比现有的二值图编码方法效率更高。     

符号化模型检测CTL

提出了一个关于时态逻辑CTL＊ 的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL＊规范. 根据该理论,作者已实现了一个基于OBDD技术的CTL＊符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等, 都只能对CTL＊的子集逻辑（如CTL,LTL）进行检测,而文中算法的结果是令人满意的,并且当规范不是特别复杂时, 高效的CTL＊符号化模型检测是可能的.