一种改进的子集可满足性算法用于FPGA布线

介绍了用布尔可满足性(SAT)和子集可满足性(sub-SAT)算法解决FPGA的详细布线问题。在布线资源固定的FPGA布线环境中,布尔公式可以证明所给电路的不可布通性,这一点要优于典型的one-net-at-a-time方法。子集可满足性方法把一个有N个约束的"严格的"SAT问题转换成一个新的"松弛的"SAT问题,仅当在原始问题中变量的不可满足个数不超过阈值k(kN)时,这一问题是可满足的。它改进了布尔可满足性,但是却产生了很多额外的变量和子句。针对这一问题,提出了用伪布尔可满足性(PBS)来消除子集可满足性公式带来的缺点。初步的实验结果表明,把这个方法加入子集可满足性方法中可以减少变量和子句数量,并显著减少运行时间。     

基于布尔可满足性的精确逻辑综合综述

逻辑综合是电子设计自动化(EDA)的重要步骤,随着算力逐渐提升和新的计算范式不断涌现,传统基于全局启发式算法的逻辑综合面临新的挑战。启发式算法面临的主要问题是得到一个次优解,随着算力的提升,逻辑优化越来越追求精确解而不满足于次优解。该文首先简述逻辑函数表达方法和布尔可满足性(SAT)问题;其次针对精确综合的算法、编码等方面介绍了在布尔逻辑网络的面积优化和深度优化方面的精确综合研究进展;最后对精确综合的未来发展趋势进行讨论。     

铁路信号区间自动闭塞逻辑检查的应用

在既有普速铁路自动闭塞区段通过增加继电器搭建的逻辑电路,及在高速铁路区段通过修改列控中心等地面设备软件,增加信号系统对区间占用的逻辑检查功能,可以实现对正常运行列车出现分路不良时的红灯防护,从而提高自动闭塞区间列车运行的安全性,增强对既有区间行车过程的监控程度。     

基于可满足性问题的非对称密码方案设计

基于可满足性问题构造加密方案具有挑战性,关键是如何构造具有加密功能的难解的SAT合取范式,并将明文安全地隐藏在其中。文章首先改进了SRR(N,k,s)模型用以隐藏明文;其次,通过恰当选取约束密度值,保证密文的难解性;最后,证明方案满足选择明文攻击(IND-CPA)是安全的。     

模糊线性时序逻辑的可实现性

模糊线性时序逻辑（fuzzy linear temporal logic）被应用于刻画模糊系统的规范语言,其可实现性（realizability）用于判断满足该时序逻辑公式的开放系统模型是否存在.模糊线性时序逻辑可实现性和系统合成（synthesis）的基本思想是：给定模糊线性时序逻辑公式,判断是否存在满足该公式的系统.如果存在,则构造满足该公式的最优系统.为了检验模糊线性时序逻辑的可实现性,首先引入模糊Büchi博弈的定义,作为检验模糊线性时序逻辑公式是否可实现的模型.其次通过归约的方法,研究模糊Büchi博弈的性质（最优无记忆策略存在性.最后验证模糊线性时序逻辑的可实现性并且给出其系统合成的过程,并说明它们的时间复杂度.     

使用布尔可满足性的组合电路等价性验证算法

该文提出了一种使用布尔可满足性SAT的新颖组合电路等价性验证技术。算法是在联接电路(Miter circuit)中进行推理来简化验证问题,推理中使用了与／非图结构简化、BDD扩展、隐含学习多种方法,最后使用有效SAT解算器zChaff解决验证任务。该算法综合了BDD和SAT的优点,限制BDD构建大小避免了内存爆炸,推理简化减小了SAT搜索空间。ISCAS85电路实验结果表明了本算法的有效性。     

基于回溯树分解的互斥约束工作流可满足性计数

工作流可满足性（WS）研究一定访问控制策略下的资源分配问题,其计数问题有利于判断工作流对资源异常情况的顽健性。本文研究互斥约束下的WS计数问题,通过多项式计数归约为约束可满足性计数问题,将经典的回溯树分解方法用于#WS（≠）求解。实验表明,改进后的算法降低了执行时间,相对于现有#WS（≠）算法,提出的算法对低密度约束下的工作流具有一定的综合性能优势。     

结合二叉判决图和布尔可满足性的等价性验证算法

本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术.算法是在与/非图AIG中进行推理,并交替使用BDD扩展和基于电路SAT解算器简化电路.如尚未解决,将用基于合取范式SAT解算器进行推理.与已有算法相比主要有如下改进:在AIG中结合多种引擎进行简化,不存在误判可能;充分利用了基于电路解算器和基于合取范式解算器各自优点,减小了SAT推理的搜索空间.实验结果表明了本算法的有效性.     

工作流可满足性(≠,=)计数及其#P完全性

工作流可满足性（WS）是资源分配对访问控制（AC）策略提出的基本要求.相关工作主要围绕WS决策问题展开,通过找到一个具体的解来说明AC策略的正确性.然而为了进一步验证AC策略在资源异常情况下的合理性,统计所有解的数量将更有帮助.本文对互斥和绑定约束下的WS计数问题进行研究,通过构造从典范性#P完全问题#3SAT到该问题的多项式计数归约,证明其属于#P完全问题,为其恰当地求解奠定了理论基础.     

基于可满足性计数的(≠,=)约束工作流鲁棒性验证

工作流将业务过程分解为有序的步骤并分配人力资源加以执行.资源分配受访问控制约束及资源异常干扰,存在可满足性和鲁棒性问题.而其鲁棒性验证又依赖于其可满足性判定,目前通过求可满足性的一个解来完成.本文提出另一种途径,通过统计解的个数来完成判定.特别地,通过多项式计数归约为有求解器可用的#SAT问题,给出了互斥和绑定约束下的可满足性计数算法.实验表明,相对目前时间复杂度最低的可满足性求解算法,该可满足性计数算法显著提高了实际判定效率和适用规模.     

从线性时序逻辑公式到自动机的转换算法

To combat the well-known state-space explosion problem in Propositional Linear Temporal Logic (PLTL) model checking, a novel algorithm capable of translating PLTL formulas into Nondeterministic Automata (NA) in an efficient way is proposed. The algorithm firstly transforms PLTL formulas into their non-free forms, then it further translates the non-free formulas into their Normal Forms (NFs), next constructs Normal Form Graphs (NFGs) for NF formulas, and it finally transforms NFGs into the NA which accepts both finite words and infinite words. The experimental data show that the new algorithm reduces the average number of nodes of target NA for a benchmark formula set and selected formulas in the literature, respectively. These results indicate that the PLTL model checking technique employing the new algorithm generates a smaller state space in verification of concurrent systems.     

一种基于区间时序逻辑模型检测的入侵检测算法

Model checking based on linear temporal logic reduces the false negative rate of misuse detection. However, linear temporal logic formulae cannot be used to describe concurrent attacks and piecewise attacks. So there is still a high rate of false negatives in detecting these complex attack patterns. To solve this problem, we use interval temporal logic formulae to describe concurrent attacks and piecewise attacks. On this basis, we formalize a novel algorithm for intrusion detection based on model checking interval temporal logic. Compared with the method based on model checking linear temporal logic, the new algorithm can find unknown succinct attacks. The simulation results show that the new method can effectively reduce the false negative rate of concurrent attacks and piecewise attacks.     

一种改进的有界模型检验子句规则

为有界模型检验提出了改进的子句规则。在节点分类的基础上,首先对精简布尔电路表示进行逻辑化简,去掉功能冗余节点;然后识别、记录和处理多元运算的操作数,把多元运算作为单个节点直接生成子句;最后合并相邻节点,根据合并后的逻辑关系生成变量和子句。实验结果表明,改进的子句规则普遍减少了可满足性问题的变量、子句数目和运行时间。     

概率时态认知逻辑模型检测中三值抽象技术的研究

 为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认知逻辑的满足性保持关系;提出概率时态认知逻辑模型检测算法;依据初始模型检测的结果,给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过Dining Cryptographer协议说明了抽象技术的应用,及其在约简系统状态空间方面的效果.     

不确定型模糊Kripke结构的计算树逻辑模型检测

本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词∃和任意量词∀在不确定型模糊Kripke结构中的两种语义解释,在模糊计算树逻辑语法中引入了路径量词∃_sup,∃_inf和∀_sup,∀_inf,分别用于替换存在量词∃和任意量词∀.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法,特别地对于模糊计算树逻辑公式∃_suppUq,∀_suppUq,∃_infpUq和∀_infpUq分别给出时间复杂度为对数多项式时间的改进算法.     

时间感知Web服务交互行为建模与失配检测方法研究

针对现有Web服务组合过程中存在时间感知力弱、服务利用率低、组合可靠性差等问题,通过将定量时间属性引入Web服务交互适配框架中,研究时间感知Web服务交互行为的形式化建模与交互行为失配的自动检测问题.提出了用于表达单个时间感知Web服务交互行为的时间服务协议(TSP)模型和用于表达多个时间感知Web服务并发组合的时间服...     

具有模糊时态的广义可能性线性时序逻辑的模型检测

本文首先定义了具有模糊时态的广义可能性线性时序逻辑GPoFLTL（Generalized Possibilistic Fuzzy Linear Tempora Logic）的语构以及基于路径和基于语言的两种语义解释,证明了GPoFLTL在模糊时态方面对GPoLTL（Generalized Possibilistic Linear Tempora Logic）进行了扩张,并通过实例说明了GPoFLTL比GPoLTL具有更强的表达能力;其次在广义可能性测度下通过模糊矩阵运算讨论了"不久","几乎总是"等几类模糊时态性质的模型检测问题;最后研究了模糊时态性质的必要性阈值模型检测问题,给出了基于自动机的GPoFLTL的阈值模型检测算法及算法的复杂度.     

以DNA为载体的线性时序逻辑模型检测

线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(Deoxyribo Nucleic Acid,DNA)为载体对线性时序逻辑(Linear Temporal Logic,LTL)实施模型检测,给出了使用粘贴自动机实现Until算子模型检测的方法.首先,使用粘贴自动机对Until公式的有穷状态自动机(Finite State Automata,FSA)模型进行编码;然后,将系统模型转换为粘贴自动机的输入字符串;最后,用粘贴自动机验证系统是否满足公式.仿真实验结果证实,新方法可实现对LTL逻辑时序算子的检测.     

面向SoC系统芯片中跨时钟域设计的模型检验方法

 传统方法无法在RTL验证阶段全面验证SoC系统芯片中的跨时钟域设计.为解决此问题,本文首先提出描述亚稳态现象的等价电路实现,用以在RTL验证中准确体现亚稳态现象的实际影响;然后使用线性时序逻辑对跨时钟域设计进行设计规范的描述;为缓解模型检验的空间爆炸问题,进一步针对跨时钟域设计的特点提出基于输入信号的迁移关系分组策略和基于数学归纳的优化策略.实验结果表明本文提出的方法不仅可以在RTL验证阶段有效地发现跨时钟域设计的功能错误,而且可以使验证时间随实验用例中寄存器数量的递增趋势从近似指数级增长减小到近似多项式级增长.     

概率实时时态认知逻辑模型检测中抽象技术的研究

概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于PTACTLK中的实时部分PTACTL,采用抽象离散时钟赋值,把概率实时解释系统的无限状态空间转化成有限形式;对于PTACTLK中的认知算子K,给出了抽象状态关于智体认知等价的定义.定义了概率实时解释系统的抽象模型,给出了抽象模型上概率实时时态认知逻辑的语义,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似.最后通过一个通信协议来说明抽象技术的有效性.