基于时态的模糊描述逻辑初探

针对现实生活中,有许多的信息都是具有时间属性并且带有模糊、不精确的特点,在时态逻辑和模糊描述逻辑基础上,利用vager集概念,对基于时态的模糊描述逻辑系统进行了初步的研究,并给出了时态模糊描述逻辑的语法和语义的相关说明.与模糊描述逻辑FALC相比,该系统的提出在一定程度上弥补了FALC作为语义Web逻辑基础在表达时序上的空白.     

模糊时态数据库关系代数演算规则分析

为了解决时态数据库对客观世界更符合实际抽象描述,能有效表示和处理复杂对象的模糊时态特性,从基本模糊时态数据模型入手,定义了一系列模糊时态关系操作元素,并论证了模糊时态区间关系代数的语法和语义,建立了一个能描述模糊时态信息的关系代数理论体系.避免了时态数据库不能提供表达模糊时态信息的环境设施,也增强了现有的时态数据库描述模糊事物特性的能力.     

间断区间时态逻辑的语义

区间逻辑不能模拟自然语言中与,或,非时态关系,其公理系统的完备性不易保证。我们建立的间断区间时态知脚注可以克服区间逻辑的上述缺点,本文给出了间断区间逻辑的语法,语义及公理,即描述了间断区间时态逻辑的语义。     

程序推理

前文“结构式时态语义”中定义了程序语言的一种时态语义,这种语义是语法引导的(Syntax Directed),保持语言的结构。本文中讨论在这种语义基础上的程序推理问题。因为这是时态语义,故在程序描述中可使用时态逻辑的丰富的表达力;又因为它是结构式的,故关于各种语句已有的推理方法,都可以翻译为时态逻辑中的定理,随意应用。     

DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述

Object-Z语言缺乏完整的时态描述能力,如无法表达操作在特定时间之后执行或按某种周期执行等,也不具有操作补偿等概念。针对这些问题,在Object-Z中集成实时概念和分布式时态逻辑,提出DTL-Real-Time Object-Z规格语言,该语言能有效地描述操作的时态驱动、事件驱动、操作补偿等因素,分析和说明了该语言的语法和语义,最后通过对责任授权模型的形式化描述说明了该语言的表达能力和应用。     

基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,适合于在语义Web环境下对相关系统的时态性质进行刻画.为了对这些时态性质进行高效的验证,在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题.一方面,使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范;另一方面,在对系统建模时借助描述逻辑ALC对领域知识进行刻画.针对上述扩展后得到的模型检测问题,提出了基于自动机的ALC-LTL模型检测算法.模型检测算法由3个阶段组成:首先将时态规范的否定形式和系统模型分别构造成标记büchi自动机;接下来构造这两个自动机的乘积自动机,并将关于ALC的推理机制融入到乘积自动机的构造过程中;最后对该乘积自动机进行判空检测.与LTL模型检测相比,时态描述逻辑ALC-LTL的模型检测引入了描述逻辑的刻画和推理机制,可以在语义Web环境下对语义Web服务等复杂系统的时态性质进行刻画和验证.     

线性时态逻辑中的特性模式

在模型检查应用中,需要使用线性时态逻辑对软件具备的特性进行描述。虽然,不同应用背景涉及不同方面的特性描述,但是线性时态逻辑描述软件特性方式上具有共性。本文从两个方面抽取这种共性,首先,按照线性时态逻辑所描述性质划分,常见性质包括活性、安全性等;其次,按照线性时态逻辑公式的作用范围划分。通过对共同问题,找到共同的描述方法得到线性时态逻辑的特性模式。最后介绍了线性时态逻辑特性模式在SPIN中的应用。     

描述逻辑的动态时序扩展*

在一些基于本体的动态应用中,需要描述组合动作和变化域的时间特性。为了对这类应用建模,通过整合动态时序逻辑和描述逻辑,提出一类描述逻辑扩展。分析了该类扩展的基本形式DLTLALC的语法和语义,并提出一种可终止的tableau算法判别DLTLALC公式可满足性。利用该类扩展,可以表达组合动作执行过程中域变化的时间特性,该类扩展为语义Web服务等动态应用建模和推理提供了一条有效途径。     

一种面向DRM的责任授权模型及其实施框架

针对现有的DRM(digital rights management)机制缺乏真正的责任描述和实施能力问题,提出一种应用于DRM的责任授权模型及其实施框架.该模型基于分布式时态逻辑和Active-U-Datalog语法规则,具有表达事件驱动、时间驱动和责任补偿等各类责任授权的语义能力,并具有良好的可实施性.对该模型的语法语义进行了分析和说明,描述了责任实施机制,并对该模型的实现、应用和表达力进行了说明和示例.该模型提高了DRM系统对数据使用控制的灵活性和能力.     

可更新Datalog的分布式时态逻辑扩展及应用

针对现有的分布式逻辑语言缺乏完整时态表达力等问题,将分布式时态逻辑谓词引入Datalog规则,提出TU-Datalog语言。该语言通过融入U-Datalog的非即时性更新语义,形成完全声明式具有强大时态表达力的逻辑编程语言和环境。通过扩展U-Datalog逻辑固定点语义,提出TU-Datalog语言的固定点时态演化规则,并对该语言的语法、语义、评价算法进行了研究,最后对该语言的应用做了说明和示例。     

An Optimal Decision Procedure for Right Propositional Neighborhood Logic

Propositional interval temporal logics are quite expressive temporal logics that allow one to naturally express statements that refer to time intervals. Unfortunately, most such logics turn out to be (highly) undecidable. In order to get decidability, severe syntactic or semantic restrictions have been imposed to interval-based temporal logics to reduce them to point-based ones. The problem of identifying expressive enough, yet decidable, new interval logics or fragments of existing ones that are genuinely interval-based is still largely unexplored. In this paper, we focus our attention on interval logics of temporal neighborhood. We address the decision problem for the future fragment of Neighborhood Logic (Right Propositional Neighborhood Logic, RPNL for short), and we positively solve it by showing that the satisfiability problem for RPNL over natural numbers is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure, and we prove its optimality.     

Hierarchies of modal and temporal logics with reference pointers

We introduce and study hierarchies of extensions of the propositional modal and temporal languages with pairs of new syntactic devices: point of reference-reference pointer which enable semantic references to be made within a formula. We propose three different but equivalent semantics for the extended languages, discuss and compare their expressiveness. The languages with reference pointers are shown to have great expressive power (especially when their frugal syntax is taken into account), perspicuous semantics, and simple deductive systems. For instance, Kamp's and Stavi's temporal operators, as well as nominals (names, clock variables), are definable in them. Universal validity in these languages is proved undecidable. The basic modal and temporal logics with reference pointers are uniformly axiomatized and a strong completeness theorem is proved for them and extended to some classes of their extensions.     

On the intertranslatability of non‐monotonic logics

This paper concentrates on comparing the expressive powers of five non‐monotonic logics that have appeared in the literature. For this purpose, the concept of a polynomial, faithful and modular (PFM) translation function is adopted from earlier work by Gottlob, but a weaker notion of faithfulness is proposed. The existence of a PFM translation function from one non‐monotonic logic to another is interpreted to indicate that the latter logic is capable of expressing everything that the former logic does. Several translation functions are presented in the paper and shown to be PFM. Moreover, it is shown that PFM translation functions are impossible in certain cases, which indicates that the expressive powers of the logics involved differ strictly. The comparisons made in terms of PFM translation functions give rise to an exact classification of non‐monotonic logics, which is then named as the expressive power hierarchy (EPH) of non‐monotonic logics. Three syntactically restricted variants of default logic are also analyzed, and EPH is refined accordingly. Most importantly, the classes of EPH indicate some astonishing relationships in light of earlier results on the expressive power of non‐monotonic logics presented by Gottlob as well as Bonatti and Eiter: Moore’s autoepistemic logic and prerequisite‐free default logic are of equal expressive power and less expressive than Reiter’s default logic and Marek and Truszczyński’s strong autoepistemic logic. This revised version was published online in June 2006 with corrections to the Cover Date.     

An Infinite Hierarchy of Temporal Logics over Branching Time

Many temporal logics have been suggested as branching time specification formalisms during the past 20 years. These logics were compared against each other for their expressive power, model checking complexity, and succinctness. Yet, unlike the case for linear time logics, no canonical temporal logic of branching time was agreed upon. We offer an explanation for the multiplicity of temporal logics over branching time and provide an objective quantified yardstick to measure these logics. We define an infinite hierarchy BTL_k of temporal logics and prove its strictness. We examine the expressive power of commonly used branching time temporal logics. We show that CTL* has no finite base, and that almost all of its many sublogics suggested in the literature are inside the second level of our hierarchy. We introduce new Ehrenfeucht–Fraissé games on trees and use them as our main tool to prove inexpressibility.     

时态认知逻辑CTL＊K的符号化模型检查算法

时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑,主要应用于多主体系统的规范定义.大多数时序认知逻辑是基于CTL的,表达能力有限.并且已知的一些模型检查算法存在内存不足和状态爆炸等问题.讨论了基于CTL*的时态认知逻辑cTL*K的语法、语义和模型,它能够在表达力很强的时态逻辑CTL*基础上描述智能体的知识、目标等意向特征.并给出了CTL*K的模型检查算法,其核心思想就是将CTL*K公式的检查问题转化为CTL*公式的模型检查问题,可以使检查的系统规模得以大幅度提高.并且将算法编码后容易集成到NuSMV模型检查器.     

The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT

Decidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the recent years. Even though most interval logics turn out to be undecidable, meaningful exceptions exist, such as the logics of temporal neighborhood and (some of) the logics of the subinterval relation. In this paper, we explore a different path to decidability: instead of restricting the set of modalities or imposing severe semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema’s CDT, and we suitably limit the negation depth of modalities. The decidability of the satisfiability problem for the resulting fragment, called CDT_BS, over the class of all linear orders, is proved by embedding it into a well-known decidable quantifier prefix class of first-order logic, namely, Bernays-Schönfinkel class. In addition, we show that CDT_BS is in fact NP-complete (Bernays-Schönfinkel class is NEXPTIME-complete), and we prove its expressive completeness with respect to a suitable fragment of Bernays-Schönfinkel class. Finally, we show that any increase in the negation depth of CDT_BS modalities immediately yields undecidability.     

Specification Diagrams for Actor Systems

Specification diagrams (SD's) are a novel form of graphical notation for specifying open distributed object systems. The design goal is to define notation for specifying message-passing behavior that is expressive, intuitively understandable, and that has formal semantic underpinnings. The notation generalizes informal notations such as UML's Sequence Diagrams and broadens their applicability to later in the design cycle. Specification diagrams differ from existing actor and process algebra presentations in that they are not executable per se; instead, like logics, they are inherently more biased toward specification. In this paper we rigorously define the language syntax and semantics and give examples that show the expressiveness of the language, how properties of specifications may be asserted diagrammatically, and how it is possible to reason rigorously and modularly about specification diagrams.     

基于本体语言OWL的模糊扩展

本体能够对特定领域的概念、术语以及关系提供一种形式化的描述方法.尽管本体在知识表示上有很强的能力,但是有一个缺陷,即不能表达不确定和不精确的信息.而这些信息在语义网和多媒体应用中,又是至关重要的.针对模糊信息的本体表示问题,本文对本体语言OWL DL进行了基于模糊逻辑的扩展,给出了形式化的语法和语义,并通过一个实例说明了该方法在表达能力上的灵活性. .     

First-Order Temporal Verification in Practice

First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems specified in other logics. The monodic fragment of first-order temporal logic is a useful fragment that possesses good computational properties such as completeness and sometimes even decidability. Temporal logics of knowledge are useful for dealing with situations where the knowledge of agents in a system is involved. In this paper we present a translation from temporal logics of knowledge into the monodic fragment of first-order temporal logic. We can then use a theorem prover for monodic first-order temporal logic to prove properties of the translated formulas. This allows problems specified in temporal logics of knowledge to be verified automatically without needing a specialized theorem prover for temporal logics of knowledge. We present the translation, its correctness, and examples of its use. Partially supported by EPSRC project: Analysis and Mechanisation of Decidable First-Order Temporal Logics (GR/R45376/01).