数字游戏中的协同——描述任务逻辑方法

传统的数字游戏只注重底层实体级别的交互协同,不支持多层次群体协同关系描述和协同规划描述,且很少有形式化理论支持.描述任务逻辑结合了描述逻辑的知识表示结构和任务逻辑的任务语义.描述任务逻辑方法对数字游戏中的协同关系和协同规划进行了形式化描述,给出了任务和规划可完成性的定义,以及联合策略下的规划可完成性的判定理论.通过示例说明,描述任务逻辑方法能够准确地描述虚拟群体高层指挥关系的任务交互语义,同时又能提供协同规划可完成性的可判定的推理验证服务.     

基于描述任务逻辑的群体组织协同关系模型

群体组织模型是深入研究群体协同行为的基础,而现有的组织模型大多集中在对Agent组织的结构或个体低层指令级的交互上,不能描述组织高层的动态任务交互。提出一个新的群体组织协同关系模型GRNA。该模型包含两个子模型:认知模型和交互模型。认知模型构建于领域本体之上,为GRNA模型提供准确的术语定义;交互模型则基于描述任务逻辑理论,反映了群体的任务协同语义。实例分析表明,GRNA支持对群体规范和能力的描述,提供了组织任务可完成性的可判定的推理服务,能够描述组织的高层任务交互语义。     

面向交互的主体能力描述和推理方法研究

主体间的交互对主体能力的影响是主体能力描述和推理需要考虑的一个重要因素．给出了一个面向交互的主体能力描述和推理框架．该框架将描述逻辑中的知识表示结构和任务逻辑中的任务语义结合起来，可以显式地描述主体之间的交互关系对主体能力的影响并可提供可判定的推理服务．建立了一个用于任务可完成性判定的逻辑系统DTL，并证明了它是可靠、完备和可判定的．     

描述任务逻辑及其应用

针对任务逻辑存在的两个缺点：（1）不可判定,无法保证推理过程都能在有限的时间内结束;（2）任务的定义局限于抽象的、逻辑的定义。无法描述任务的具体属性和任务之间的关系,将描述性结构引入任务逻辑,构造了一个可描述具体属性的、可判定的任务逻辑系统——描述任务逻辑．将所构造的逻辑系统应用于具有组织的多主体系统行为建模,建立了基于描述任务逻辑的多主体组织模型和建模框架,并且表明应用描述任务逻辑构造应用系统具有表达能力强、结构紧凑的特点．     

基于时序描述逻辑的UML状态图语义

将UML图形转换成形式化规范是一种精确UML语义、扩大形式化软件方法适用范围的有效途径。鉴于描述逻辑强的可判定推理能力,提出一种采用时序描述逻辑形式化UML状态图,对描述逻辑进行时序扩展,得到可以表示动态和时序语义的形式化规范——时序描述逻辑,给出一套UML状态图向时序描述逻辑表达式转换的规则,通过实例验证了该方法的可行性。     

UML2.0顺序图的时序描述逻辑语义

针对UML2.0顺序图用于对象间交互行为建模时存在动态语义缺乏精确形式化描述的问题,提出一种基于时序描述逻辑的UML2.0顺序图形式化方法。对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑,根据UML2.0新增的交互操作符将UML2.0顺序图分成一个或多个最大顺序片段,通过形式化最大顺序片段和交互操作符得到UML2.0顺序图的时序描述逻辑语义。实例检验结果表明,该方法具有可行性。     

计算机支持的协同工作系统的时序逻辑模型

为了使群体能够协同完成任务,CSCW(computer supported cooperative work)系统不仅要解决各种分布性、处理应用领域的特殊性,而且要提供面向用户的协作支持,从而使其行为异常复杂.然而对系统行为进行形式化的描述是构造软件系统的必经阶段.为了清晰地描述CSCW系统的行为,使其特定性质的验证成为可能,本文在时序逻辑的基础上,建立了CSCW系统行为的抽象描述模型.在此模型中,CSCW系统由分布运行实体和信息对象组成,系统的主要行为表现为用时序逻辑语言XYZ/E描述的实体间的交互.此模型可较好地对系统的分析和构造进行指导.     

基于时序描述逻辑的UML顺序图形式化研究

在统一建模语言（UML）规范中顺序图的语义是以自然语言的形式描述的,是一种半形式化的语言,不能对系统的交互行为进行形式化分析及论证.针对UML顺序图缺乏精确的形式化描述问题,根据顺序图的时序特征,提出了增加交互操作符的UML顺序图的六元组形式化方法.对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑.应用时序描述逻辑的时态算子得到时序描述逻辑语义形式的UML顺序图.用UML顺序图描述完整的C语言执行过程,将其形式化描述,实验结果表明,这种方法是可行的.     

ALC中的Tableau算法及其性质

描述逻辑是一族知识表示的形式化语言,是一阶谓词逻辑的可判定子集,已成为语义Web的理论基础.描述逻辑中ALC是最小命题封闭的,是其它描述语言的基础,而可判定是描述逻辑的最重要的问题,在ALC中Tableau算法巧妙地解决了这一问题,掌握ALC中的Tableau算法是理解各种描述逻辑中可判定性的基础.对ALC中的Tableau算法进行详细阐述,并对其关键的几个性质: 可终止性、完备性和判定性给出了证明,为研究SHOIN(D)中的Tableau算法及性质奠定了基础.     

满足复杂要求的机器人最优巡回控制系统设计与实现

本文结合线性时序逻辑理论与模糊控制方法,设计并实现了一种满足复杂任务需求的移动机器人巡回控制系统,它既能够针对复杂时序任务进行路径规划,又能够对机器人进行模糊控制实现路径跟踪.首先,基于线性时序逻辑理论,确定能够满足复杂巡回任务需求的全局最优路径.接着,根据所获得的最优路径,采用模糊控制方法设计轨迹跟踪控制器,使其通过实时位姿反馈对机器人进行路径跟踪控制.仿真结果验证了移动机器人巡回控制系统的有效性.最后,基于E-Puck移动机器人构建了能够满足复杂任务需求的移动机器人巡回控制实验系统.基于所提出的最优巡回路径规划算法和模糊控制器设计方法,通过图像处理、数据通信、算法加载等软件模块的实现完成了满足复杂任务需求的移动机器人巡回控制.     

包含时间约束的作战任务建模与验证方法

制定作战计划时往往需要考虑作战任务的时间约束问题。目前对作战任务的时间约束分析方法都存在约束类型少、验证方法适用范围小等问题。为此提出基于业务流的作战任务时间约束建模方法,构建了作战任务流模型并用以描述作战任务的相对和绝对时间约束。提出了作战任务的时间约束形式化验证方法,设计了作战任务模型到NuSMV语言的转换算法,并基于时序逻辑给出了作战任务的基本时间约束描述方法。最后以登岛作战任务为例,验证了其相对约束和绝对约束的部分性质,并根据反馈结果对模型进行了修正。     

Task apportionment in a rearrangement problem of multiple mobile robots

A rearrangement problem involving multiple mobile robots is addressed in this paper. In the problem, it is important to identify task decomposition, task allocation, and path planning applicable to distinct environments while rearrangement tasks are executed. We here define ‘task apportionment’ as an operation that sets up task decomposition and conducts task allocation based on that setup. We propose a method for task apportionment and path planning applicable to distinct environments. The method establishes the necessary intermediate configurations of objects as one way of task decomposition and determines task allocation and path planning as a semi-optimized solution by using simulated annealing. The proposed method is compared with a continuous transportation method and a territorial method through simulations and experiments. In the simulations, the proposed method is, on the average, 17 and 20% faster than the continuous transportation method and the territorial method, respectively. In the experiments, the proposed method is, on the average, 22 and 16% faster than the continuous transportation and the territorial method, respectively. These results show that the proposed method can realize an efficient rearrangement task by mobile robots in various working environments under feasible computation time, especially in environments with a mixture of wide and narrow areas and an uneven distribution of objects.     

A logical foundation for the semantic Web

World Wide Web (WWW) has been one of important channels from which people acquire information and services, but most web pages are only used by humans at pre-sent, and these pages cannot be processed and understood automatically by computers. The semantic Web is an essential reformation of Web. The main objective of the seman-tic Web is to enrich Web with semantics and make Web be understood by computers, in order to communicate and cooperate between people and computer. The key of the se-…     

语义网的一阶逻辑推理技术支持

研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.     

动态描述逻辑动作间关系的Petri网分析方法研究

针对动态描述逻辑动作理论在描述和分析多个动作间关系(尤其并发关系)时能力的不足, 提出对多个动态描述逻辑动作间关系描述和分析的 Petri 网方法. 首先讨论了动态描述逻辑动作的等价 Petri 网描述, 进一步通过对动作描述的推理和各个动作的 Petri 网共享合成操作, 得到多个动态描述逻辑动作的 Petri 网系统. 在此基础上, 应用 Petri 网的相关理论与方法, 如可达图分析方法, 研究了多个动态描述逻辑动作间关系的分析与判定方法, 对动态描述逻辑动作理论的描述和分析能力进行了必要的扩充.     

一类具有3种否定的模糊模态命题逻辑

对不同否定知识的认知、区分、表达、推理及计算是模糊知识研究处理的一个基础。具有矛盾否定、对立否定和中介否定的模糊命题逻辑形式系统FLCOM是一种能够完整描述模糊知识中的不同否定及其关系与规律的理论。基于FLCOM和中介模态命题逻辑MK,提出一类具有3种否定的模糊模态命题逻辑MKCOM及其扩充系统MTCOM,MS₄COM和MS₅COM;讨论了MKCOM的语义和语法解释,并证明了MKCOM的可靠性定理和完备性定理。