张春霞[1]2000年在《基于动态逻辑的Agent的形式化模型》文中认为随着计算机网络以及基于网络的分布式计算的发展，对于Agent系统的研究，已成为 人工智能领域中一个新的研究热点，也成为分布式人工智能的重要研究方向。基于Agent 的技术被认为是软件领域中的一次重大突破。 本文提出了一种基于动态逻辑的Agent的BDIK_h形式化模型；定义了信念、知识、愿 望、目标、意愿和Know-how；描述了它们的逻辑；讨论了Agent所具有的性质；给出了 这个模型的完备性的证明；在一定条件下避免了逻辑全知问题；解决了无为而治问题以及 理论与实践分离的问题；同时动态逻辑的灵活性和动态性更好地描述了Agent的动态性质。
伍晓敏[2]2004年在《基于VSK-t逻辑的Agent形式化模型》文中认为随着计算机网络以及基于网络的分布式计算的发展，对于Agent系统的研究，已成为人工智能领域中一个新的研究热点。基于Agent的技术被认为是软件领域中的一次重大突破。 本文提出了一种基于时序逻辑的Agent形式化模型。VSK-t逻辑是一种对处在特定环境中的计算Agent的信息特征进行推理的多模态逻辑。VSK-t逻辑可以描述环境中客观真的事物、环境中可访问的或可知的信息，以及Agent能感知到的环境信息，最后还可描述Agent真正知道的信息，同时，时序逻辑的灵活性和动态性更好地描述了Agent的动态性质。系统中Agent的行为能力是与其所处环境的时间密切相关的，Agent不会执行那些自己在某些时间没有能力执行的动作，而Agent的感知能力也是随时间变化而变化的。这样的描述是合乎理性的。 用形式化方法构建了一种基于VSK-t逻辑的Agent形式化模型。定义了VSK-t逻辑的语法规则，语义框架。提出了相应的公理体系，并对其合理性进行了充分的阐述。讨论了Agent所具有的性质，提出并详细证明了一系列理论结果。证明了VSK-t逻辑的无矛盾性、完全性以及完备性。通过具体示例说明了该逻辑的应用。讨论了该模型的特点。提出了今后的一些研究工作。
刘玉鹏[3]2011年在《面向混成特性的CTCS-3系统规范建模与验证》文中提出系统规范是系统开发的起点和基础。系统规范的缺陷将给项目成功带来极大的风险。对系统规范进行建模和验证是消除潜在缺陷的有效方法,也是保证系统正确设计和开发的前提。近些年来,中国轨道交通事业快速发展。以CTCS-3级列车运行控制系统为代表的基于无线通信的列车运行控制系统是今后的发展方向。CTCS-3级列车运行控制系统系统是一个典型的混成系统,列车的连续运行过程和无线闭塞中心(RBC)的离散作用机制之间交互影响,呈现复杂的混成性。列车事故的发生往往同速度、加速度、距离等连续变化量的不良控制密切相关。因此,从混成性的角度对安全关键CTCS-3系统规范进行建模与验证是非常有必要和有意义的。以此为出发点,本文在列车运行控制系统规范建模与验证体系的基础上,给出面向混成性的CTCS-3系统规范建模与验证的方法和流程：首先利用可描述系统混成性的HybridUML对CTCS-3系统规范建模,接着将模型转换为形式化的微分动态逻辑模型,最后在验证工具里对系统规范的微分动态逻辑模型进行形式化验证。本文重点阐述了基于UML2.0的扩展机制在建模软件RSA中构建概要文件(profile)实现UML2.0到HybridUML扩展的过程；同时以列车运动加速减速过程为例阐述了如何利用经扩展得到的HybridUML对CTCS-3系统规范进行建模；接着给出了从HybridUML模型到微分动态逻辑模型的转换规则,进而使CTCS-3系统的形式化模型的获得和对模型的形式化验证能够得以实现。最后本文以CTCS-3系统中典型的RBC切换流程为案例,给出了面向混成性的CTCS-3系统规范建模与验证的方法的具体应用。首先介绍了CTCS-3系统规范中RBC切换流程的过程,接着在RSA中对RBC切换流程建立HybridUML模型,然后根据从HybridUML到微分动态逻辑的转换规则得到RBC切换的微分动态逻辑模型,最后在形式化验证工具KeYmaera中对微分动态逻辑模型的安全性等性质进行验证并对验证结果进行了分析。案例分析很好地展示了面向混成性的建模与验证的方法和流程,充分体现出方法和流程的有效性和可行性。
章江花[4]2006年在《基于BDI-VSK-T逻辑的Agent系统形式化模型的研究》文中认为随着计算机网络、计算机通信等技术的发展，对于Agent和多Agent系统的研究己成为分布式人工智能(DAI)重要的研究领域。Agent系统的研究成果主要基于思维状态的BDI模型和VSK逻辑。Agent思维状态的BDI模型是指如何形式化地描述Agent的各种思维属性和它们之间的关系，以及与Agent规划、行为、协调、合作等活动的关系，进而指导Agent系统的构建。基于VSK逻辑的Agent系统是对处在特定环境中的Agent信息特征进行推理的一种多模态逻辑，使用VSK逻辑，我们能表示环境中客观真的事物，在环境中可以访问的信息以及Agent借助于感知器能感知到的信息，还能表示Agent真正知道的信息。本文试图将Agent的BDI逻辑，VSK逻辑和时序逻辑结合，通过其思维状态以及客观和主观认识为达到某一目标或完成任务做出行为选择。提出基于时序逻辑的Agent形式化模型BDI-VSK-T,它是基于BDI逻辑和VSK逻辑展开的，首先融合了BDI逻辑和VSK逻辑，然后在时序上重新定义语义框架，以时序结构构建可达世界。每个世界的时间结构是一个时间树，时间树中的分支代表Agent在相应时刻的动作选择，同时定义相应的模态算子：B(Visibility)环境访问算子、S(Perception)环境感知算子和K(Knowledge)知道算子，它们分别表示Agent对环境的可访问、感知、知道的信息及其特征；Bel(Belief)信念算子，Des(Desire)愿望算子，Int(Intention)意图算子，它们分别用来表示系统状态中的Agent具有的信念、愿望和意图等思维状态．此外在BDI逻辑和VSK逻辑基础上还引入○(next)，◇(eventually)，□(always)，F(full)和E(exist)等五个时序算子，它们分别用来表示系统状态中的Agent状态和它所处环境的有关时间的信息特征。这些模态算子可以按任何可能的方式进行组合以决定Agent面临的动作选择。基于时序逻辑从Agent为完成某项任务时应具备客观环境及其思维出发，能表示随着时间的变化，环境中客观真的事物，在环境中可以访问的信息以及Agent借助于感知器能感知到的信息，还能表示Agent真正知道的信息，同时能够描述Agent在客观环境中具有的信念、愿望和意图等思维状态，而且能描述思维，客观环境，时间的关系及其对Agent动作选择的影响。在此语义形式化环境解释下，用可达世界来构建语义框架并提出了该模型的公理体系，并给出这个公理体系的有效性证明，再进一步用归纳法证明模型的可靠性，用构造法证明了完全性，完备性。
林怡[5]2008年在《基于Em-BDI-VSK逻辑的Agent系统形式化模型的研究》文中提出随着人工智能的发展,有关Agent理论和技术的研究和应用引起了人们的高度关注和重视.在Agent的理论研究中,人们常常从较高层次利用基于意向观点的抽象工具来研究和认识主体.除基于意向观点从抽象层次来认识主体和划分认知成分外,还需要一种严格的数学工具把这些认知成分表示出来,并让它们来影响Agent的行为.逻辑工具很好的完成这个目标.针对各种问题和实际应用,人们提出了多种逻辑系统.随着发展的不断深入,出现了将多种逻辑结合起来,或者扩展各种逻辑来表示Agent的方法.纵观以往的Agent研究,集中在理智Agent的构造上.虽有认知型Agent的代表BDI模型表示了其内部的思维状态.但随着生物学和心理学的发展,人们发现情感对于人的推理,规划和学习也有重要的作用.因此,把情感加入Agent中,也越来越受到计算机科学家的关注.把情感加入计算机中,首先,要研究情感的类型：其次,人们希望把情感加入到Agent的体系结构中参与Agent内部推理和决策.人们从心理学和认知学的角度,提出了很多模型.其中,OCC模型被认为更加适合在计算机中实现.更多细节请参看综述2.3.3节.目前,人们在Agent体系中构建情感主要基于BDI和KARO两个主体模型之上.两者都是在构建好的主体形式化系统上分别构建不同的情感,并由情感和其它认知成分相互影响共同决定Agent的决策和行为.本文提出的模型是基于这样的认识：人类自然的行为决策过程不仅受到所处的外部环境和Agent内部思维状态的影响外,还受到当时情感的影响,三方面相互作用共同决定当前Agent的行为选择.因此,该模型试图融合了代表外部环境的VSK逻辑,代表内部思维状态的BDI逻辑以及情感因素.带有情感的Agent形式化模型Em-BDI-VSK融合BDI逻辑和VSK逻辑并加入情感,定义相应的模态算子Em,并采用OCC模型中22种情感中一种最常见和基本的情感Fear做为示例.利用Em-BDI-VSK逻辑,能表示环境中客观真的事物,在环境中可以访问的信息以及Agent借助于感知器能感知到的信息等外部环境,还能表示Agent真正知道的信息(把外化的信息内化自己的知识),同时能够描述Agent在客观环境中具有的信念、愿望和意图等思维状态和情感,这些因素共同对Agent动作选择产生影响.Em-BDI-VSK逻辑基于时序逻辑从Agent为完成某项任务应具备的能力和权利的角度及其思维以及情感出发,进行动作的选择以及状态的转换.在该模型中,各种信息有着自己的特点,并且各类信息之间互相影响.本模型中,用交互公理来刻划各类信息间的相互关系.在此语义环境解释下,本文构建了该模型的语义框架,并提出了该模型的公理体系,包括BDI逻辑、VSK逻辑、情感算子和时序算子的公理,以及这些模态算子间相互联系的交互公理,并给出了这些公理的合理性解释.最后,给出这个公理体系的有效性证明,进而证明了模型的可靠性和完全性.虽然AI专家对情感一直有兴趣,但在人工智能中未受到足够重视。直到近年来,心理学上认知理论的发展,极大的促进了情感在人工智能中的研究。心理学大量的实验证明,情感并不游离在理智之外,情感对于人的规划、学习和行为也有着重要的作用。为了让agent能更自然更合理的进行行为决策,人们希望在以前理智型agent的基础上加入情感因素,和其它认知成分共同作用于agent的行为决策。本文总结出情感在计算机研究中的两个方面主要问题：一方面是情感表示和情感识别。大多都采用模式识别的方法来研究情感,并结合生理学理论提取相关特征辅肋情感计算机计算和识别情感,通过内部的计算模型还可以利用仿真面部表示出要求的情感。但这种方法也继承了模式识别的一些固有的缺点,并且要找到模式识别中与情感相对应的特征也是该方法的难点所在。在这个方面,已有大量的成果出现,并有些作为产品深入到家庭中。另一方面,把情感引入到主体(agent)体系结构中,让情感参与主体的行为决策过程,更自然合理的模拟人的行为,使决策的制定更自然和更人性化。大多数构造的情感agent体系结构中,多从三个方面来考虑agent的内部决策过程受到的影响。基于实际中的心理学、生理学的相关理论,普遍认为agent的决策受到了来自外部环境、内部思维状态和情感状态三方面的共同影响,大量的模型被提出希望把三方面共同作用决策过程的内部机理表示出来,但正因如此,这些模型也存在实现的复杂性的问题。而对于agent的研究,其内部推理机制还需要一种严格的数学工具把这些认知成分和情感表示出来,并共同影响Agent的行为,其中,逻辑工具很好的完成这个目标。针对各种问题和实际应用,人们提出了多种逻辑系统,如经典命题逻辑、一阶谓词逻辑、模态逻辑、时序逻辑、动态逻辑、模糊逻辑等等。随着发展的不断深入,出现了将多种逻辑结合起来,或者扩展各种逻辑来表示Agent的方法。对情感agent的研究,主要基于心理学的认知理论,其推理过程归纳为各认知成分和情感的相互作用共同决定agent的行为决策。加入情感的agent推理模型,首先要研究情感的类型。心理学上提出了很多模型,主要分为三类：基于外在情感表现形式和基于维度的分类以及前两类的结合。其中,OCC模型是第一个以机器实现为目的的情感分类,因此大多数的情感建模也基于OCC模型来定义情感类型。其次,使用逻辑来表示情感类型。就目前提出的加入情感的逻辑表示中,主要基于两类逻辑进行扩展：BDI逻辑和KARO框架。本文列举了一个基于OCC和KARO的情感评价机制形式化系统来描述逻辑表示情感和情感加入决策制定的推理过程的方法。该方法基于计算机实现为目的,进行情感和各认知成分共同推理获得行为选择和影响决策的过程,为以后的研究起到了一个借鉴的作用。
王兴超[6]2005年在《结合思维状态的VSK-Agent形式化模型》文中指出随着计算机网络以及基于网络的分布式计算的发展,对于Agent技术的研究,已经成为人工智能领域以及分布式人工智能的一个热点和重要的研究方向。Agent技术,特别是多Agent技术,为分布开放系统的分析、设计和实现提供了一种崭新的方法,由此产生了一系列新的思想、方法和技术。基于Agent的技术被认为是软件领域中的一次重大突破。 本文在VSK逻辑的基础上,引入了信念(Belief)、愿望(Desire)和意图(Intention)等三个思维属性,提出了一种对Agent的信息特征及其思维属性进行推理的形式化体系-VSK-BDI逻辑。VSK-BDI逻辑是一种命题多模态逻辑,定义了访问、感知、知识等算子,用以表示环境中客观真的事物、以及对Agent而言,环境中可访问的信息、Agent能感知到的环境信息以及Agent真正知道的信息;同时定义了信念、愿望、意图等算子,用以描述Agent具有的内部思维状态;并考虑了所定义的算子之间的关系。在提出了VSK-BDI逻辑并且建立了它与Agent的形式化模型间的关系后,给出了该逻辑的公理体系,并对其合理性进行了充分的阐述:同时给出了该公理体系的一致性、完全性以及完备性证明;最后,通过具体实例说明了此逻辑的用途,并讨论了今后的一些研究工作。该形式化模型是基本可计算的;其语义是自然的、合理的;由于考虑了Agent对所处的客观环境的认识及其思维状态之间的相互关系,因而能够更好的描述Agent的动态性。
代国林[7]2005年在《基于BDI的协商公理体系多Agent系统模型》文中研究说明随着计算机网络及其基于网络的分布计算技术的发展,Agent以及多Agent系统(MAS)的研究成为分布式人工智能(DAI)研究的一个热点.单Agent所拥有的知识和能力是有限的,而现实系统往往异常复杂,并且具有开放、分布和动态的特点,因此对MAS的研究迅速发展.在MAS的研究中,Agent之间的交互和推理是一个重要的研究内容,Agent之间的交互主要有三种形式:合作、协调、协商。其中协商是合作和协调的基础. 本文针对多模态逻辑VSK和BDI的特点,采用形式化方法对多Agent系统和多Agent系统的协商进行了研究,具体研究工作包括以下几个方面: 首先,在对VSK逻辑和BDI逻辑研究的基础上,结合两种模型的特点,构建了基于BDI的协商公理体系多Agent系统模型.该模型以VSK逻辑为基础,进一步刻画了Agent的内部状态,主要涉及Agent的信念(belief)、愿望(desire)和意图(intention)等思维属性,使模型既能描述客观环境,又能描述Agent的思维状态及其变化过程,Agent主要根据它的思维状态及其所处的环境进行行为选择和协商. 其次,采用符号结构的方法来描述信念、愿望和意图的语义,该方法与可能世界语义相比,具有简单、易于理解的特点,这样的描述是直觉的、合理的、自然的. 然后,构建了基于BDI的协商公理体系,并且给出了公理的合理性解释,证明了公理的有效性和协商推理逻辑的可靠性、完全性及完备性. 最后,通过一个实例描述了模型的应用,并且给出了进一步研究的方向.
吴浩[8]2007年在《基于SOA的综合电子信息系统的面向Agent研发方法研究》文中研究说明我军的军用电子信息系统,现在已步入综合一体化阶段,其目标是将多种军事电子信息系统整合成为一个有机的大型综合电子信息系统。目前综合电子信息系统的研发面临着涉及面广、应用背景复杂、分布式、不同子系统不相兼容等诸多困难。SOA面向服务架构,为综合电子信息系统提供了新的体系架构。基于SOA的综合电子信息系统具有松耦合性、高可复用性、灵活性、可扩展性等优点,能够很好地解决上述诸多问题,是目前综合电子信息系统发展的方向。但是,目前的综合电子信息系统开发方法,如结构化方法、面向对象方法、构件化方法都不能适应基于SOA的综合电子信息系统开发的需要。而面向Agent的开发方法对应用系统进行了更高层次的抽象,其中引入了许多社会学,组织学方面的观点和技术,为复杂大型信息系统的分析和设计提供了很好的思路和方法。面向Agent的开发方法将系统抽象为一个个具有自主性的Agent,通过多个Agent之间相互协作实现系统的功能。面向Agent的开发方法所具有的高层次抽象、自然建模、问题分解、系统组织等优点使其能够适应基于SOA的综合电子信息系统开发的需要。本文从Agent的理论研究出发,分析并介绍目前主要的面向Agent的开发方法,根据基于SOA的综合电子信息系统的特点,充分借鉴已有的面向Agent开发方法,提出了一种适合基于SOA的多Agent系统开发方法——MASS方法。该方法具有一般面向Agent开发方法的特点和优势,并且能够支持系统开发全过程。MASS方法能够适应基于SOA的综合电子信息系统开发的需要,可以为综合电子信息系统的开发提供良好的支持。最后,本文给出了该方法的一个具体应用示例。
朱敏, 李必信, 陈乔乔, 吉顺慧, 李加凯[9]2012年在《基于微分动态逻辑的CPS建模与属性验证》文中研究指明随着信息物理融合系统(Cyber-Physical Systems,CPS)应用的越来越普及,CPS的设计和实现能否满足实际需求显得至关重要.本文提出了一种CPS建模与属性验证框架.在框架中,首先使用HybridUML对CPS进行建模,然后将该通用模型转换为形式化模型,进而进行形式化验证.本文采用的形式化验证方法为dL(Differential Dynamic Log-ic),其操作模型为hybrid program.将HybridUML模型转换为hybrid program时,基于语义一致性的原则定义转换规则.转换完成后,结合得到的hybrid program对验证的CPS属性进行规约,最后使用定理证明器KeYmaera对属性进行自动化验证.
孙瑜[10]2002年在《基于VSK-AF逻辑的多Agent系统的形式化模型》文中研究表明随着计算机网络、计算机通信等技术的发展，对于Agent和多Agent系统的研究已成为分布式人工智能(DAI)一个热点和重要的研究领域。 本文提出了一种对多Agent系统的信息特征进行推理的形式化体系-VSK-AF逻辑。VSK-AF逻辑是对处在特定环境中的计算Agents的信息特征进行推理的多模态逻辑。它可以表示环境中客观真的的事物、环境中可访问的或可知的信息以及Agent能感知到的环境信息，最后还可表示Agent真正知道的信息。该逻辑的语义是以一般的多Agent系统模型给出的，并且与认知逻辑的解释系统密切相关。在提出了VSK-AF逻辑并且建立了它与多Agent系统的形式化模型间的关系后，给出了该逻辑的公理化体系，并对其合理性进行了充分的阐述。同时证明了这个公理体系的一致性、无矛盾性、完全性以及完备性。最后，通过具体案例分析来说明此逻辑的用途，并讨论了今后的一些研究工作。
参考文献：
[1]. 基于动态逻辑的Agent的形式化模型[D]. 张春霞. 云南师范大学. 2000
[2]. 基于VSK-t逻辑的Agent形式化模型[D]. 伍晓敏. 云南师范大学. 2004
[3]. 面向混成特性的CTCS-3系统规范建模与验证[D]. 刘玉鹏. 北京交通大学. 2011
[4]. 基于BDI-VSK-T逻辑的Agent系统形式化模型的研究[D]. 章江花. 云南师范大学. 2006
[5]. 基于Em-BDI-VSK逻辑的Agent系统形式化模型的研究[D]. 林怡. 云南师范大学. 2008
[6]. 结合思维状态的VSK-Agent形式化模型[D]. 王兴超. 云南师范大学. 2005
[7]. 基于BDI的协商公理体系多Agent系统模型[D]. 代国林. 云南师范大学. 2005
[8]. 基于SOA的综合电子信息系统的面向Agent研发方法研究[D]. 吴浩. 中国电子科学研究院. 2007
[9]. 基于微分动态逻辑的CPS建模与属性验证[J]. 朱敏, 李必信, 陈乔乔, 吉顺慧, 李加凯. 电子学报. 2012
[10]. 基于VSK-AF逻辑的多Agent系统的形式化模型[D]. 孙瑜. 云南师范大学. 2002
标签：自动化技术论文; 逻辑模型论文; 建模软件论文; 人工智能技术论文; 形式化方法论文; 系统思维论文; 微分算子论文; 关系逻辑论文; 公理系统论文; 动态模型论文; 推理论文;