摘要：针对析取回答集程序的结构化测试基础理论匮乏的问题,系统化地提出析取回答集程序结构化测试覆盖的概念。首先,定义针对析取回答集程序的测试用例,确立析取回答集程序的主要测试实体为程序中的逻辑规则;其次,通过对规则的头、规则的体、规则的集合等不同测试目标构建了规则覆盖、定义覆盖、环覆盖等基本概念来模拟结构化测试中的语句覆盖、分支覆盖等概念;最后,提出了析取回答集程序的测试覆盖率计算公式,并举例说明各种覆盖下的覆盖率计算方法,并讨论了析取回答集程序的部分特殊性质和关键指标。

摘要：模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前,CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.

摘要：针对求解复杂度为NP难问题的Slater选举,提出一种回答集程序设计(ASP)方法用于求解选举结果。通过ASP构造尽可能少的无回路锦标赛,找到与原锦标赛差别最小的一个并从中选出获胜者。实验结果表明,该方法的编码方式不依赖于候选人的数量,时间复杂度低,可读性强,并且适用于Kemeny选举。

摘要：回答集程序设计(ASP)是一种主流的非单调知识表示工具。为了能够在利用ASP求解问题过程中使用现有的以经典逻辑表示的知识,给出了一种把以谓词逻辑公式表示的约束型知识和定义型知识转化为ASP程序或知识库的新方法,并以实例说明了其有效性。该方法满足转化后ASP程序的回答集与原公式集的模型具有一一对应关系。在实际应用中,该方法提供了一项从现存的以谓词逻辑为表示语言的知识库,构建以ASP为知识表示语言的非单调知识库的技术。

摘要：主要通过指称语义和回答集程序(Answer Set Programming,简称ASP)完成迹模型的生成,并构建了一套基于计算树逻辑(computing tree logic,简称CTL)的CSP模型验证方法.实验表明,该方法对于分支类型的性质具有较好的描述能力,且保证了验证的正确性.

摘要：哈密尔顿回路问题是图论的经典NP-难解问题之一,在计算机科学中被广泛用作测试用例以测试算法/系统的有效性,包括可满足性(SAT)、回答集程序设计(ASP)以及约束可满足问题(CSP)等。在本文中,我们通过ASP实验研究了40到100个节点(步长为10)随机图的哈密尔顿回路存在性、不存在性、以及难于计算等的分布情况,结果表明它们都具有一定的规律。这不仅对随机图的哈密尔顿回路本身是有益的探索,也为生成随机图哈密尔顿测试用例提供了有益的指导。

摘要：针对现有模型检测工具对活性描述不足、模型转换复杂,提出一种基于ASP及稳定失败语义的CSP模型检测方法。该方法采用时态逻辑LTL刻画性质,将进程的稳定失败模型和LTL公式转化为ASP,利用ASP求解器验证性质,实现一次运行验证多条性质。实验结果表明,该方法既扩大了基于稳定失败模型的活性验证范围,也避免了不同模型之间的转换。

摘要：针对顺序协商模型中的资源浪费问题,以及电子商务中间人模型的适用性低问题,提出一个基于ASP的中间人协商模型。利用回答集给出了协商建议的形式化描述,结合ASP规则将中间agent的功能转化为ASP知识库,通过ASP求解器实现协商过程。实验结果表明,与顺序协商模型相比,该模型可有效解决顺序协商中的资源浪费问题,且提高了协商效率;与电子商务中间人模型相比,该模型可用于非数字形式的协商元素的协商。