一种不确定时段的扩展时段对序逻辑：时间Petri网模型表示和线性推理

针对点－时段时序逻辑的不足,提出了一种新的时段时序逻辑－－扩展时段时序逻辑,对不确定时间段发生的事件具有较好的描述能力。时间Petri网模型表示的引入,增强了扩展时段时序逻辑的描述直观性及分析能力,为进行线性推理提供了有利的工具。同时还提出了几种变迁间的实施推理规则。运用这些规则可以简化复杂时序关系的Petri网模型,并在线性时间复杂度内定量地得到各变迁间的时序逻辑关系,因而是一种行这有效的方法。     

Linear logic as a tool for planning under temporal uncertainty

The typical AI problem is that of making a plan of the actions to be performed by a controller so that it could get into a set of final situations, if it started with a certain initial situation.The plans, and related winning strategies, happen to be finite in the case of a finite number of states and a finite number of instant actions.The situation becomes much more complex when we deal with planning under temporal uncertainty caused by actions with delayed effects.Here we introduce a tree-based formalism to express plans, or winning strategies, in finite state systems in which actions may have quantitatively delayed effects. Since the delays are non-deterministic and continuous, we need an infinite branching to display all possible delays. Nevertheless, under reasonable assumptions, we show that infinite winning strategies which may arise in this context can be captured by finite plans.The above planning problem is specified in logical terms within a Horn fragment of affine logic. Among other things, the advantage of linear logic approach is that we can easily capture ‘preemptive/anticipative’ plans (in which a new action β may be taken at some moment within the running time of an action α being carried out, in order to be prepared before completion of action α).In this paper we propose a comprehensive and adequate logical model of strong planning under temporal uncertainty which addresses infinity concerns. In particular, we establish a direct correspondence between linear logic proofs and plans, or winning strategies, for the actions with quantitative delayed effects.     

Fuzzy fault tree analysis based on T–S model with application to INS/GPS navigation system

A novel fault tree analysis (FTA) technique based on the Takagi and Sugeno (T–S) model is proposed in this paper. In the proposed technique, referred to as the TS-FTA, the events in the conventional FTA can be expressed in terms of fuzzy possibilities, and the gates that represent the relations among the top event and the primary events are replaced by T–S fuzzy gates derived from the T–S model. The magnitudes of the faults in the system are expressed in term of fuzzy variables. Since the proposed TS-FTA is derived from fuzzy logic and the T–S model, it can readily handle fuzzy information and uncertainties in the relationships among events. Therefore, the TS-FTA is suitable for systems where exact information on the fault probabilities of the components and the failure mechanisms are not available. The proposed TS-FTA is applied to analyze the reliability of an Inertial Navigation System and Global Position System (INS/GPS) integrated navigation system.     

An implementation of inference in temporal branching time models

Issues concerning the implementation of temporal reasoning (inference) for models based on branching time logic as applied to intelligent decision support systems are considered. The focus is on the construction of a qualitative (interval) and quantitative (metric) branching time model. The inference is reduced to solving the temporal constraint satisfaction problem, and the corresponding procedures (algorithms) are proposed. An example of the practical application of the proposed techniques in a prototype of a real-time intelligent decision support system is described.     

A logical foundation for the case‐based reasoning cycle

Case‐based reasoning (CBR) has drawn considerable attention in artificial intelligence (AI) fields with many successful applications in systems such as e‐commerce and multiagent systems. For the moment, research and development of CBR basically follows the traditional process model of CBR, i.e., the R⁴ model and problem space model introduced in 1994 and 1996, respectively. However, there has been no logical analysis for this popular CBR model. This article will fill this gap by providing a unified logical foundation for the CBR cycle. The proposed approach is based on an integration of traditional mathematical logic, fuzzy logic, and similarity‐based reasoning. At the same time, we examine the CBR cycle from the knowledge‐based (KB) viewpoint. The proposed logical approach can facilitate research and development of CBR. © 2003 Wiley Periodicals, Inc.     

模糊交互时态逻辑的模型检测

交互时态逻辑已被广泛应用于开放系统的规范描述,交互时态逻辑的模型检测技术是一个比较重要的验证方法。为了形式化描述和验证具有模糊不确定性信息的开放系统的性质,提出了一种模糊交互时态逻辑,并讨论了它的模型检测问题。首先,引入了模糊交互时态逻辑的基于路径和基于不动点的两种语义,证明了其等价性。然后,基于其等价性,给出了模糊交互时态逻辑的模型检测算法和复杂性分析。     

随机时序逻辑的模糊时间扩展方法

基于随机时序逻辑(SQTL),通过扩展模糊时间来表达系统的模糊时间关系,并实现一种表达能力更强的时序逻辑——模糊随机时序逻辑(FSQTL)。FSQTL能够建模实时系统中的确定时间、概率时间、随机时间和模糊时间,并利用可能性实现对性能需求的分析。     

一个带有相似性关系的模糊逻辑

模糊集与模糊逻辑是处理模糊性与不确定性信息的重要数学工具，相似性关系是模糊集的一个基本概念。为了在模糊逻辑中集成相似性关系并考虑其模糊推理，提出了一个带有相似性关系的模糊逻辑，给出了其语法及语义描述，在模糊谓词逻辑情形下，讨论并证明了基于归结与调解方法的模糊推理的有关属性，考虑到许多定理证明器和问题解决系统均是基于否证法，证明了归结与调解方法对模糊谓词演算的反驳完备性定理。     

不确定时态信息表示的统一模型

时态信息表示和推理是人工智能研究中的一个重要课题,现有的模型大多只能表示确定时态信息,然而现实生活中很多事件的发生结束等时态信息都是不确定的。故提出了一个表示不确定时态信息的统一模型,可用于描述各种具有确定或不确定时态信息的事件。该模型首先定义各类时态对象(如时间点、时间区间)以及它们之间的关系,并给出时态对象间的传递关系表,利用该表能进行时态一致性约束满足问题的求解。最后,给出了两个不确定时态推理的例子,表明了该模型的实际应用意义。     

Linear, Branching Time and Joint Closure Semantics for Temporal Logic

Temporal logic can be used to describe processes: their behaviour ischaracterized by a set of temporal models axiomatized by a temporaltheory. Two types of models are most often used for this purpose: linearand branching time models. In this paper a third approach, based onsocalled joint closure models, is studied using models which incorporateall possible behaviour in one model. Relations between this approach andthe other two are studied. In order to define constructions needed torelate branching time models, appropriate algebraic notions are defined(in a category theoretical manner) and exploited. In particular, thenotion of joint closure is used to construct one model subsuming a setof models. Using this universal algebraic construction we show that aset of linear models can be merged to a unique branching time model.Logical properties of the described algebraic constructions are studied.The proposed approach has been successfully aplied to obtain anappropriate semantics for non-monotonic reasoning processes based ondefault logic. References are discussed that show the details of theseapplications.     

A sound and complete fuzzy temporal constraint logic.

In this work, we define an extended fuzzy temporal constraint logic (EFTCL) based on possibilistic logic. EFTCL allows us to handle fuzzy temporal constraints between temporal variables and, therefore, enables us to express interrelated events through fuzzy temporal constraints. EFTCL is compatible with a theoretical temporal reasoning model: the fuzzy temporal constraint networks (FTCN). The syntax, the semantics and the deduction and refutation theorems for EFTCL are similar to those defined for the sound and noncomplete fuzzy temporal constraint logic (FTCL). In this paper, a resolution principle for performing inferences which take these constraints into account is proposed for EFTCL. Moreover, we prove the soundness and the completeness of the refutation by resolution in EFTCL.     

基本并行进程活性的限界模型检测

基本并行进程是一个用于描述和分析并发程序的模型,是Petri网的一个重要子类.EG逻辑是一种在Hennessy-Milner Logic的基础上增加EG算子的分支时间逻辑,其中的AF算子表示从当前的状态出发性质最终会被满足,因此EG逻辑是能够表达活性的逻辑.然而,基于基本并行进程的EG逻辑的模型检测问题是不可判定的.由此,本文提出了基本并行进程上EG逻辑的限界模型检测方法.首先,给出了基本并行进程上EG逻辑的限界语义,然后采用基于约束的方法,将基本并行进程上EG逻辑的限界模型检测问题转化为线性整数算术公式的可满足性问题,最后利用SMT求解器进行求解.     

A survey on temporal logics for specifying and verifying real-time systems

Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.     

模糊计算树逻辑的符号模型检测

对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题.将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储.对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性.该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围.     

Fuzzifying Allen's Temporal Interval Relations

When the time span of an event is imprecise, it can be represented by a fuzzy set, called a fuzzy time interval. In this paper, we propose a framework to represent, compute, and reason about temporal relationships between such events. Since our model is based on fuzzy orderings of time points, it is not only suitable to express precise relationships between imprecise events (ldquoRoosevelt died before the beginning of the Cold Warrdquo) but also imprecise relationships (ldquoRoosevelt died just before the beginning of the Cold Warrdquo). We show that, unlike previous models, our model is a generalization that preserves many of the properties of the 13 relations Allen introduced for crisp time intervals. Furthermore, we show how our model can be used for efficient fuzzy temporal reasoning by means of a transitivity table. Finally, we illustrate its use in the context of question answering systems.     

Modeling and Analysis of Real-Time Cooperative Systems Using Petri Nets

The existing formal techniques are not suitable for elegantly modeling passing value indeterminacy and describing batch processing function in real-time cooperative systems. Moreover, the correct behavior of the systems depends on not only the logical correctness of the results obtained through running workflows but also the time of producing them before critical deadlines. For these purposes, this paper proposes an interorganizational logical workflow net (ILWN) for modeling and analyzing real-time cooperative systems based on time Petri nets, workflow techniques, and temporal logic. Through attaching logical expressions to some actions of an ILWN model, the size of the model is reduced. Thus, ILWNs can efficiently mitigate the state explosion problem to some extent. Also, this paper analyzes the soundness of a subclass of ILWNs: the or-restricted ILWNs. A rigorous analysis approach is given based on their static net structures only. The concepts and techniques proposed in this paper are illustrated with a seller-buyer example in electronic commerce.     

基于组合逻辑的故障诊断方法

针对复杂系统故障传播和故障分析的模糊性和不确定性,首先,在逻辑Petri网和模糊Petri网的理论基础上,根据逻辑Petri网的传值不确定性以及模糊Petri网对模糊信息的表示和推理能力的特点,提出模糊逻辑Petri网的概念及推理规则,考虑不同故障源对故障的影响程度,将概率信息引入模糊逻辑Petri网,对故障源赋予置信度,使故障诊断过程更符合实际。其次,利用模糊逻辑Petri网对故障诊断系统进行建模,用模糊逻辑Petri网描述了系统故障状态组合的逻辑关系,并进一步简化了系统模型的表达形式,具有良好的封装性、重构性和可维护性,在一定程度上缓解了状态组合空间爆炸问题。针对故障的传播性,采用可达性分析方法对故障信息的传播路径进行模拟论证,提高了故障诊断效率。最后,通过离心式压缩机故障诊断过程实例分析,验证了该方法的有效性和可行性,提高了故障诊断过程的准确性和高效性。     

Analysis of stability and robust stability of polynomial fuzzy model-based control systems using a sum-of-squares approach

The well known Takagi–Sugeno (T–S) fuzzy model can be extended in different ways including the polynomial fuzzy model, whose consequent parts are polynomial sub-systems. Compared with the traditional T–S fuzzy model, the polynomial fuzzy model can represent a nonlinear system more accurately with a smaller number of fuzzy logic rules. It is worth emphasizing that the stability analysis and controller design of polynomial fuzzy model-based (PFMB) control systems are not based on the linear matrix inequalities but the recently developed sum-of-squares decompositions. In this paper, based on an existing result for traditional fuzzy control systems, we propose a new stability condition for the stability analysis of PFMB control systems. Furthermore, the stability of PFMB control systems with parameter uncertainties is investigated. The popular inverted pendulum and an unstable nonlinear system are employed to demonstrate the quality of the proposed stability conditions.