基于代理技术的NSS设计与实现

谈判支持系统(negotiation support system,NSS)通常为两方人员提供一个协商服务平台.实际生活中常出现某方人员难以亲临参加谈判的情形,需要系统为其提供一个软件代理继续协商下去.提出一种基于代理技术的NSS以解决上述问题,给出了该系统的体系框架和逻辑结构,构建了买卖交易中的卖方代理,并设计了使其具有智能特性的两个重要方法.最后,在移动代理开发平台Aglets上开发了一个原型系统ANSS,对它的人机交互界面做了简要介绍.     

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

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

基于动态描述逻辑的UML状态图形式化方法

统一建模语言(UML)状态图包括静态语义和动态语义.针对该特点,提出基于动态描述逻辑的UML状态图形式化方法,介绍动态描述逻辑DDL_SHOIN(D)的语法和语义,设计UML状态图的DDL_SHOIN(D)形式化方法,研究状态图动作推理问题.给出状态图状态可达性和动作包含关系的定义,并证明其正确性.     

基于扩展颜色Petri网的拍卖协议建模与分析

电子商务自动谈判是多主体协商的典型应用.谈判协议的形式化是实现电子商务谈判自动化的关键.给出一种带抑止弧和时间变迁的颜色Petri网模型及其扩展或然状态图分析方法.用该扩展颜色Petri网模型对拍卖谈判协议进行了建模,同时用扩展或然状态图分析方法证明了协议模型的可达性.     

状态图到PTL形式规范的转化

本文讨论从状态图到PTL形式规范的转化方法.状态图是描述系统行为的半形式化的图形工具,但缺少精确的形式语义,PTL(投影时序逻辑)是一种具有离散的时间模型的时序逻辑,把状态图转换到PTL后可以使其具有精确的形式语义并能使用形式化验证方法来证明状态图所描述的系统的一些重要性质是否得到满足,同时可把系统的形式描述转换为Tempura程序进行模拟,从而提高系统设计的可信性.     

采用动态描述逻辑实现UML状态图特性检测

状态图是UML（Unified Modeling Language）语言中刻画对象行为的重要视图，而如何对状态图模型定义的正确性和有效性进行检验一直是一个亟待解决的问题。本文提出采用动态描述逻辑对UML状态图形式化，并利用该逻辑系统的推理能力对状态图相关静态和动态特性进行检测。我们首先将状态图描述为一个形式系统。其中，状态图中的一个状态对应于该形式系统中的一个状态，状态特性及描述被表示为该形式系统中的概念和公理，事件被表示为该形式系统中的动作。然后，我们通过概念测试来检验状态图状态可满足性和冗余性，通过公式可满足性测试来验证状态转移引起的对象特性变化。     

基于商务谈判的机器学习理论方法研究

电子商务的谈判中应用机器学习方法可增加其智能特性.探讨基于商务谈判的机器学习理论,建立了商务谈判学习模型,设计出相应的学习算法Strategy Learning以获取谈判领域的专家知识-谈判规则.通过一个应用实例,验证了SL方法的可行性和正确性.     

规则驱动的体结构演化设计

针对轻量化结构设计,提出一种规则驱动的体结构演化方法.首先定义模型中每个体素及其邻域为一个智能主体,将模型内部结构装配问题转化为一个多智能主体系统的优化问题;然后将物理约束和人工策略定义为设计规则,通过引入可废止逻辑表达不完备的知识和约束;最后通过群体涌现行为生成全局结构.实验结果表明,该方法能够在相同规则的控制下根据不同的边界条件演化出有针对性的结构,也可以在相同边界条件下根据不同的规则得到相异的设计.     

基于形式化规格说明的UML状态图提取

为了辅助软件开发者理解形式化规格说明,提出一种从B方法规格说明中提取UML状态图的方法。通过分析状态信息在规格说明中的表现形式,定义一系列精确的简单状态、状态迁移、复合迁移、分层状态和状态图通信等提取规则。借助状态变量表和状态迁移表,最终实现状态元素和状态关系的提取,并以此构造完整的UML状态图。实验结果验证了方法的正确性及有效性。     

一种新的Statechart模型验证方法

在传统的基于时序逻辑的模型检查框架下验证Statcchart模型面临三大挑战:全状态空间搜索、多次重复搜索和复杂时序逻辑公式难写。基于上述问题和实践工作,提出一种新的Statechart模型验证方法。该方法的中心是一种强化了的属性描述语言—属性状态图,并利用属性状态图中存在的先后关系和并发关系,把各个属性状态图有机地结合成一个树结构—属性树。属性树涵盖了目标系统要求验证的属性空间,因此可自上而下的验证整棵属性树。在验证过程中系统Statechart模型对应状态空间是逐步展开的,每验证部分属性就展开相应的部分状态空间并对其进行验证,验证过程是基于属性树转换并以step为单位,验证step的初始status和结束status是否满足对应属性树节点公式对其的属性约束,这样既能够迅速找出错误又能屏蔽step内部系统Statcchart模型的状态变化,使得验证过程更简单快捷。为了说明属性状态图和基于其的验证算法是实用和易用的,通过一个例子说明了从模型设计到具体验证整个过程。     

A formal approach to negotiating agents development

This paper presents a formal and executable approach to capture the behaviour of parties involved in a negotiation. A party is modeled as a negotiating agent composed of a communication module, a control module, a reasoning module, and a knowledge base. The control module is expressed as a statechart, and the reasoning module as a defeasible logic program. A strategy specification therefore consists of a statechart, a set of defeasible rules, and a set of initial facts. Such a specification can be dynamically plugged into an agent shell incorporating a statechart interpreter and a defeasible logic inference engine, in order to yield an agent capable of participating in a given type of negotiations. The choice of statecharts and defeasible logic with respect to other formalisms is justified against a set of desirable criteria, and their suitability is illustrated through concrete examples of bidding and multi-lateral bargaining scenarios.     

Logical control of an elevator with defeasible logic

The elevator control program of Dyck and Caines (1995) can be implemented more concisely in d-Prolog, a defeasible logic programming system developed by Nute (1992, 1996, 1997). To demonstrate this, the program is recast, first into ordinary Prolog and then into d-Prolog. In defeasible logic, more specific rules take precedence over more general ones. Thus, the d-Prolog programmer can state general rules and then give explicit exceptions, just as humans do when explaining complex regularities to each other     

A conditional logic for defeasible beliefs

This paper provides a framework for representing beliefs by distinguishing between (i) the defeasible principles of a belief system, (ii) the propositions that are beyond reasonable doubt in a belief state, and (iii) the propositions ‘favored’ on the basis of defeasible principles and those propositions that are beyond reasonable doubt. Defeasible principles are interpreted semantically by means of a Lewis-style ranking of worlds (without the assumption that the actual world is among the ‘innermost’, or most highly ranked, worlds). The ‘favored closure’ (F-closure) of a set of defeasible principles and reasonable propositions is non-monotonic. Yet, given the concept of ‘pruning’ the default ranking relative to a set of worlds (determined by what is beyond reasonable doubt in a particular belief state) we provide a formal characterization of the conditions under which in inference to a favored conclusion on the basis of defeasible rules and reasonable propositions, is warranted. The adequacy of our representation of defeasible principles can be tested by considering a number of valid formulas that we list. We show that our concept of defeasible principle parallels but is not identical to the concept of ‘relatively high conditional probability’. An example of application of the formal language and semantics is given, and the final parts of the paper contain u     

ANGLE: An autonomous, normative and guidable agent with changing knowledge

Some emerging computing systems (especially autonomic computing systems) raise several challenges to autonomous agents, including (1) how to reflect the dynamics of business requirements, (2) how to coordinate with external agents with sufficient level of security and predictability, and (3) how to perform reasoning with dynamic and incomplete knowledge, including both informational knowledge (observations) and motivational knowledge (for example, policy rules and contract rules). On the basis of defeasible logic and argumentation, this paper proposes an autonomous, normative and guidable agent model, called ANGLE, to cope with these challenges. This agent is established by combining beliefs-desires-intentions (BDI) architecture with policy-based method and the mechanism of contract-based coordination. Its architecture, knowledge representation, as well as reasoning and decision-making, are presented in this paper. ANGLE is characteristic of the following three aspects. First, both its motivational knowledge and informational knowledge are changeable, and allowed to be incomplete, inconsistent/conflicting. Second, its knowledge is represented in terms of extended defeasible logic with modal operators. Different from the existing defeasible theories, its theories (including belief theory, goal theory and intention theory) are dynamic (called dynamic theories), reflecting the variations of observations and external motivational knowledge. Third, its reasoning and decision-making are based on argumentation. Due to the dynamics of underlying theories, argument construction is not a monotonic process, which is different from the existing argumentation framework where arguments are constructed incrementally.     

DR-Prolog: A System for Defeasible Reasoning with Rules and Ontologies on the Semantic Web

Nonmonotonic rule systems are expected to play an important role in the layered development of the semantic Web. Defeasible reasoning is a direction in nonmonotonic reasoning that is based on the use of rules that may be defeated by other rules. It is a simple, but often more efficient approach than other nonmonotonic rule systems for reasoning with incomplete and inconsistent information. This paper reports on the implementation of a system for defeasible reasoning on the Web. The system 1) is syntactically compatible with RuleML, 2) features strict and defeasible rules, priorities, and two kinds of negation, 3) is based on a translation to logic programming with declarative semantics, 4) is flexible and adaptable to different intuitions within defeasible reasoning, and 5) can reason with rules, RDF, RDF Schema, and (parts of) OWL ontologies     

Defeasible Logic on an Embedded Microcontroller

Defeasible logic is a system of reasoning in which rules have exceptions, and when rules conflict, the one that applies most specifically to the situation wins out. This paper reports a successful application of defeasible logic to the implementation of an embedded control system. The system was programmed in d-Prolog (a defeasible extension of Prolog), and the inferences were compiled into a truth table that was encoded on a low-end PIC microcontroller.Advantages of defeasible logic include conciseness and correct handling of the passage of time. It is distinct from fuzzy logic and probabilistic logic, addressing a different set of problems.     

On Resolving Conflicts Between Arguments

Argument systems are based on the idea that one can construct arguments for propositions—structured reasons justifying the belief in a proposition. Using defeasible rules, arguments need not be valid in all circumstances, therefore, it might be possible to construct an argument for a proposition as well as its negation. When arguments support conflicting propositions, one of the arguments must be defeated, which raises the question of which (sub‐) arguments can be subject to defeat. In legal argumentation, metarules determine the valid arguments by considering the last defeasible rule of each argument involved in a conflict. Since it is easier to evaluate arguments using their last rules, can a conflict be resolved by considering only the last defeasible rules of the arguments involved? We propose a new argument system where, instead of deriving a defeat relation between arguments, arguments for the defeat of defeasible rules are constructed. This system allows us to determine a set of valid (undefeated) arguments in linear time using an algorithm based on a JTMS, allows conflicts to be resolved using only the last rules of the arguments, allows us to establish a relation with Default Logic, and allows closure properties such as cumulativity to be proved. We propose an extension of the argument system based on a proposal for reasoning by cases in default logic.     

Self-defeating arguments

An argument is self-defeating when it contains defeaters for some of its own defeasible lines. It is shown that the obvious rules for defeat among arguments do not handle self-defeating arguments correctly. It turns out that they constitute a pervasive phenomenon that threatens to cripple defeasible reasoning, leading to almost all defeasible reasoning being defeated by unexpected interactions with self-defeating arguments. This leads to some important changes in the general theory of defeasible reasoning.     

Rule-based approaches for energy savings in an ambient intelligence environment

This paper presents a novel real-world application for energy savings in a Smart Building environment. The proposed system unifies heterogeneous wireless sensor networks under a Semantic Web Service middleware. Two complementary and mutually exclusive rule-based approaches for enforcing energy-saving policies are proposed: a reactive agent based on production rules and a deliberative agent based on defeasible logic. The system was deployed at a Greek University, showing promising experimental results (at least 4% daily savings). Although the percentage of energy savings may seem low, the greatest merit of the method is ensuring that no energy is wasted by constantly enforcing the policies.     

t-DeLP: an argumentation-based Temporal Defeasible Logic Programming framework

The aim of this paper is to propose an argumentation-based defeasible logic, called t-DeLP, that focuses on forward temporal reasoning for causal inference. We extend the language of the DeLP logical framework by associating temporal parameters to literals. A temporal logic program is a set of basic temporal facts and (strict or defeasible) durative rules. Facts and rules combine into durative arguments representing temporal processes. As usual, a dialectical procedure determines which arguments are undefeated, and hence which literals are warranted, or defeasibly follow from the program. t-DeLP, though, slightly differs from DeLP in order to accommodate temporal aspects, like the persistence of facts. The output of a t-DeLP program is a set of warranted literals, which is first shown to be non-contradictory and be closed under sub-arguments. This basic framework is then modified to deal with programs whose strict rules encode mutex constraints. The resulting framework is shown to satisfy stronger logical properties like indirect consistency and closure.