Modeling multi-rate DSP specification semantics for formal transformational design in HOL

The CATHEDRAL Silicon Compilers synthesize hardware for DSP algorithms specified in Silage, a high level applicative language. In order to optimize the results of the silicon compilation in terms of chip-area and/or throughput, the user often massages the specification applying transformations to the Silage code. To guarantee that the transformations preserve the behavior of the specified algorithm, the formal semantics of the specification language had to be defined. The semantics has been used to prove in HOL the correctness of the transformations and to prove properties of the specification. We are currently building a system where a menu of useful andcorrectness preserving transformations will be available to the user. In this system the user could choose appropriate transformations from the menu taking advantage of his creativity and expertise to interactively guide the silicon compiler, without the risk of introducing inconsistencies. This article describes the formalmulti-rate semantics of a substantial subset of Silage and illustrates some formally verified transformations.     

Verification of Software Requirements on Program Systems Represented by Attribute Transition Systems

An approach to the verification of requirements is presented. A formal requirement language is described and the properties to be checked are formulated. A scheme for proving some important dynamic properties is developed.     

Induction in the Timed Interval Calculus

The Timed Interval Calculus, a timed-trace formalism based on set theory, is introduced. It is extended with an induction law and a unit for concatenation, which facilitates the proof of properties over trace histories. The effectiveness of the extended Timed Interval Calculus is demonstrated via a benchmark case study, the mine pump. Specifically, a safety property relating to the operation of a mine shaft is proved, based on an implementation of the mine pump and assumptions about the environment of the mine.     

命题演算形式系统在Isabelle／HOL中的形式化

本文针对命题演算形式系统,在机器辅助定理证明系统Isabelle／HOL中为其建立逻辑模型,并分别形式化验证了PC和ND的主要性质,以及完备性定理的证明。通过对PC和ND的分析和验证表明,采用机器辅助定理证明系统,对以数理逻辑为平台的各种形式系统进行严格的分析和证明是可行的。     

MEASUR方法在信息系统体系结构设计中的应用

信息系统体系结构是系统开发、集成的指南,体系结构开发的质量直接关系到系统成功与否。由于以往体系结构研究主要关注体系结构产品的设计方法和工具,使得体系结构问题域的分析缺乏有效的方法和手段。以DoDAF1.0为背景,研究了MEASUR方法在体系结构设计中的应用。重点研究了问题清晰法、语义分析方法以及规范分析方法在体系结构设计中的应用。最后,通过案例说明了方法的可用性。     

Applications of parallel processing technologies in heuristic search planning: methodologies and experiments

The goal of this paper is to investigate the application of parallel programming techniques to boost the performance of heuristic search‐based planning systems in various aspects. It shows that an appropriate parallelization of a sequential planning system often brings gain in performance and/or scalability. We start by describing general schemes for parallelizing the construction of a plan. We then discuss the applications of these techniques to two domain‐independent heuristic search‐based planners—a competitive conformant planner (CP A) and a state‐of‐the‐art classical planner (FF). We present experimental results—on both shared memory and distributed memory platforms—which show that the performance improvements and scalability are obtained in both cases. Finally, we discuss the issues that should be taken into consideration when designing a parallel planning system and relate our work to the existing literature. Copyright © 2009 John Wiley & Sons, Ltd.     

Iterated belief change in the situation calculus

John McCarthy's situation calculus has left an enduring mark on artificial intelligence research. This simple yet elegant formalism for modelling and reasoning about dynamic systems is still in common use more than forty years since it was first proposed. The ability to reason about action and change has long been considered a necessary component for any intelligent system. The situation calculus and its numerous extensions as well as the many competing proposals that it has inspired deal with this problem to some extent. In this paper, we offer a new approach to belief change associated with performing actions that addresses some of the shortcomings of these approaches. In particular, our approach is based on a well-developed theory of action in the situation calculus extended to deal with belief. Moreover, by augmenting this approach with a notion of plausibility over situations, our account handles nested belief, belief introspection, mistaken belief, and handles belief revision and belief update together with iterated belief change.     

一种Internet移动代理系统的黄页服务模型

提出了一种基于信度推理网络的移动代理系统黄页服务模型,为自主迁移的移动代理提供迁移决策支持。与现有的移动代理系统黄页服务模型相比,该模型较好地解决了信息局部性和信息更新的问题,其结构具有良好的可扩展性和灵活性,能更好地适应Ｉｎｔｅｒｎｅｔ动态的网络环境。     

An Australian Perspective on Research and Development Required for the Construction of Applied Legal Decision Support Systems

At the Donald Berman Laboratory for Information Technology and Law, La TrobeUniversity Australia, we have been building legal decision support systems for a dozenyears. Whilst most of our energy has been devoted to conducting research in ArtificialIntelligence and Law, over the past few years we have increasingly focused uponbuilding legal decision support systems that have a commercial focus.In this paper we discuss the evolution of our systems. We begin with a discussion ofrule-based systems and discuss the transition to hybrid rule-based/case-based systems.We next discuss how we have used machine learning in building legal decision supportsystems. Our focus on using machine learning led us to investigate the domains ofexplanation and argumentation. We conclude by discussing our current work onbuilding negotiation support systems and tools for constructing web-based legaldecision support systems.     

标记迁移系统的组合可达性分析

标记迁移系统是一种在计算机辅助设计和验证中得到广泛使用的形式模型。当系统中的模块比较多时,系统的整体模型有可能出现状态空间的指数级爆炸,组合可达性分析是缓解这一问题的一种有效方法。已有的工作缺乏对该方法基本原理的清晰描述和精确表达。本文对其基本原理进行了分析和概括,并作了形式化陈述,证明了相关结论。本文的工作有助于深入理解和澄清组合可达性分析的内部工作机制。     

Locomotion control of a four-legged robot embedding real-time reasoning in the force distribution

This paper discusses the application of rule-based reasoning to manage in real time the force distribution computation within a locomotion control of quadruped robots. The control uses input–output linearization in the attitude subsystem, and optimal linear control in the overall locomotion system. The force distribution approach provides more adaptability and flexibility to the locomotion control, because the system is capable of fast adaptation to a wide variety of situations. Rules defining the knowledge about how to deal with walk events and feet forces calculation are presented. The rule-based reasoning is made using the system (LAAS).     

An Implicit Transition Matrix Approach to Stability Analysis of Flexible Multi-Body Systems

The stability of linear systems defined by ordinarydifferential equations with constant or periodic coefficients can beassessed from the spectral radius of their transition matrix. Inclassical applications of this theory, the transition matrix isexplicitly computed first, then its eigenvalues are evaluated; if thelargest eigenvalue is larger than unity, the system is unstable. Theproposed implicit transition matrix approach extracts the dominanteigenvalues of the transition matrix using the Arnoldi algorithm,without the explicit computation of this matrix. As a result, theproposed implicit method yields stability information at a far lowercomputational cost than that of the classical approach, and is ideallysuited for stability computations of systems involving a large number ofdegrees of freedom. Examples of application of the proposed methodologyto flexible multi-body systems are presented that demonstrate itsaccuracy and computational efficiency.     

基于案例系统的一种案例标引和获取方法及算法

基于案例系统通过模拟人们分析和处理问题的方式,以达到辅助决策的目的。案例标引和获取是基于案例系统中的两个重要环节。针对已有方法的不足,提出一种新的案例标引和获取方法。     

Participatory decision-support model in the context of building structural design embedding BIM with QFD

The design and optimisation of building structures is a complex undertaking that requires the effective collaboration of various stakeholders and involves technical and non-technical expertise. The paper investigated an integrated decision-support framework using Quality Function Deployment (QFD) in structural design optimisation. The aim of the study was to develop and test a systematic participatory model that utilises Building Information Modelling (BIM)-enabled technologies for data collection and group decision-making theory. The uncertainties associated with the decision-makers’ preferences were computed using Evidential Reasoning (ER) algorithms in the QFD house of quality. An actual decision scenario was used to test the proposed framework and investigate its capabilities in the context of reinforced concrete buildings. The study demonstrated how the proposed QFD model could effectively enhance decision-making by managing the diversity of stakeholders’ preferences via design integration, enhanced communication and shared domain knowledge.     

论辩系统的动态性及其研究进展

论辩系统是一种非单调形式体系,能够支持个体Agent的推理决策和多Agent之间的有效交互.由于个体Agent的知识、观察信息和资源的动态性以及多Agent交互过程的动态性,在各类论辩系统中,论证及其攻击关系的动态性是普遍存在的.作为一个新的研究领域,有关论辩系统动态性的概念、理论和方法远未成熟.在介绍论辩系统相关概念的基础上,阐明论辩系统动态性的两个主要研究方向(正向动态性和逆向动态性),并讨论需要解决的开放性问题.围绕这些问题,简要回顾现有的理论和方法,并分析其特点和不足.     

Statistical Properties of Transition Amplitudes in Generic Systems

I review some recent results on the statistical properties of matrix elements of typical observables (transition amplitudes) in an eigenbasis of generic quantum Hamiltonian systems. The classical limit of an underlying system can be either integrable, or fully chaotic, or mixed with regular and irregular regions coexisting in phase space. In any case, the variance of transition amplitudes (the local average transition probability) as a function of energy and transition frequency can be calculated in terms of classical power spectra. The probability distribution of transition amplitudes in high energy (semiclassical) regime is derived by means of random matrix theory, whereas in low and intermediate energy (nonsemiclassical) regime the probability distribution of transition amplitudes exhibits universal exponential tails which still call for theoretical explanation.     

事件演算在行动推理中的应用

事件演算是基于一阶谓词演算的行动推理理论.它可作为描述事件的一个工具,在行动推理的应用中显示出其强大的表示能力和实现能力.在事件演算中,可以对行动进行公理化,可以描述行动的时间性、并发性、连续变化及知识,而且还可用Prolog实现.讨论介绍与这些应用相关的基本概念、思想和方法等,并且通过一个送咖啡的例子说明了如何通过事件演算来描述和实现.     

Applications of Hierarchical Reasoning in the Verification of Complex Systems

In this paper we show how hierarchical reasoning can be used to verify properties of complex systems. Chains of local theory extensions are used to model a case study taken from the European Train Control System (ETCS) standard, but considerably simplified. We show how testing invariants and bounded model checking (for safety properties expressed by universally quantified formulae, depending on certain parameters of the systems) can automatically be reduced to checking satisfiability of ground formulae over a base theory.