基于时序逻辑的3种网络攻击建模

与其他检测方法相比,基于时序逻辑的入侵检测方法可以有效地检测许多复杂的网络攻击。然而,由于缺少网络攻击的时序逻辑公式, 该方法不能检测 出常见的back,ProcessTable以及Saint 3种攻击。因此,使用命题区间时序逻辑(ITL)和实时攻击签名逻辑(RASL)分别对这3种攻击建立时序逻辑公式。首先,分析这3种攻击的攻击原理;然后,将攻击的关键步骤分解为原子动作,并定义了原子命题;最后,根据原子命题之间的逻辑关系分别建立针对这3种攻击的时序逻辑公式。根据模型检测原理,所建立的时序逻辑公式可以作为模型检测器(即入侵检测器)的一个输入,用自动机为日志库建模,并将其作为模型检测器的另一个输入,模型检测的结果即为入侵检测的结果,从而给出了针对这3种攻击的入侵检测方法。     

基于线性时序逻辑的最优巡回路径规划

基于线性时序逻辑(Linear temporal logic, LTL)的路径规划方法中, 多点巡回路径规划问题尚无有效解决方案. 为了在道路网络中实现最优巡回监测, 提出了基于LTL的最优巡回路径规划方法. 首先, 将环境建模成一个切换系统, 用LTL语言描述包含多个巡回点和障碍物的任务需求; 接着, 利用循环移位法构建能够融合任务需求和环境模型的扩展乘机自动机, 以建立路径信息完整的网络拓扑; 最后, 采用基于迪科斯彻法的最优综合算法搜索扩展乘机自动机网络上的最优路径, 从而获得能够满足复杂任务需求的最优巡回路径. 仿真结果表明, 该方法能够有效实现最优巡回路径规划.     

网络协议形式化模型的分析与应用

网络协议的形式化模型是协议分析和设计的核心技术之一。论文在简要分析当前的几种常用网络协议形式化模型之后,指出时序逻辑作为网络协议形式化模型的独特优越性,然后给出用一种线性时序逻辑MPTL描述IGMP协议的具体实例。     

Alternating-time stream logic for multi-agent systems

Constraint automata have been introduced to provide a uniform operational model for specifying service interfaces of components, the network that yields the glue code for the components, and the operational behavior of the composite system. Constraint automata have been used as the basis for equivalence checking and model checking temporal logical properties. This paper presents a multi-player semantics for constraint automata which serves to reason about controllability, interaction and cooperation facilities of individual components or coalitions of components in a given network. We introduce a temporal logic framework, called alternating-time stream logic, that combines classical features of alternating-time logic (ATL) for concurrent games with special operators for specifying regular conditions on the data streams in the network and on the write and read operations at the I/O-ports of the components. Since constraint automata support any kind of synchronous and asynchronous peer-to-peer communication, the resulting game structure is non-standard and requires a series of nontrivial adaptations to the semantics and verification algorithms for classical alternating-time approaches.     

一种基于并发命题投影时序逻辑模型检测的入侵检测方法

基于投影时序逻辑模型检测的入侵检测方法具有描述网络入侵者分段攻击的能力,然而对并发攻击仍无能为力,因为该逻辑无法直接描述并发。针对此问题,在该逻辑的基础上定义了一种新的并发算子,并给出基于并发投影时序逻辑模型检测的入侵检测方法。对复杂攻击实例的检测表明,新方法可有效提高对并发攻击的检测能力。     

实现并行搜索和符号逻辑算法的高阶二维时态－竞争激励神经网络方法

本文提出并行搜索和规划算法，以及实现它们的高阶二维时态－竟争激励神经网络．这种网络还能实现基于传统符号逻辑的许多问题求解算法．本文的方法克服了通常的神经网络求解优化问题的缺陷．同时，也避免了符号逻辑算法的串行性及符号逻辑Ｓｙｓｔｏｌｉｃ结构复杂性等问题．给出了求解隐式图搜索、ＬＣＳ问题、ＴＳＰ问题及０－１背包问题的实例．     

Representing and Reasoning about Motion in a Two-Dimensional World

We present a point-based spatiotemporal first-order logic for representing the qualitative and quantitative spatial temporal knowledge needed to reason about motion in a two-dimensional space. A feature of the logic is the uniform treatment of space and time. The knowledge of a simplified world, a two-dimensional street network with active traffic lights, is represented, and the reasoning problem of how a robot moves from one place to another in the world is formalized with the proposed logic.     

High-Order Two-Dimension Cluster Competitive Activation Mechanisms Used for Performing Symbolic Logic Algorithms of Problem Solving

This paper presents a neural network approach,based on high-order twodimension temporal and dynamically clustering competitive activation mechanisms,to implement parallel searching algorithm and many other symbolic logic algorithms.This approach is superior in many respects to both the common sequential algorithms of symbolic logic and the common neural network used for optimization problems.Simulations of problem solving examples prove the effectiveness of the approach.     

基于粗糙描述逻辑的不精确时态知识表示研究

在粗糙描述逻辑基础上扩充不精确时态关系,以满足不精确时态知识表示与推理的需要。首先给出了粗糙集及粗糙描述逻辑的相关概念;接着通过定义粗糙时态描述逻辑不精确时态关系,扩展了粗糙描述逻辑中具体域,并给出了可靠性和完备性证明;最后通过实际例子说明粗糙时态描述逻辑的知识表示和应用,结果表明扩展后的粗糙时态描述逻辑可以实现不精确时态知识的表示与推理。     

Fuzzy branching temporal logic

Intelligent systems require a systematic way to represent and handle temporal information containing uncertainty. In particular, a logical framework is needed that can represent uncertain temporal information and its relationships with logical formulae. Fuzzy linear temporal logic (FLTL), a generalization of propositional linear temporal logic (PLTL) with fuzzy temporal events and fuzzy temporal states defined on a linear time model, was previously proposed for this purpose. However, many systems are best represented by branching time models in which each state can have more than one possible future path. In this paper, fuzzy branching temporal logic (FBTL) is proposed to address this problem. FBTL adopts and generalizes concurrent tree logic (CTL*), which is a classical branching temporal logic. The temporal model of FBTL is capable of representing fuzzy temporal events and fuzzy temporal states, and the order relation among them is represented as a directed graph. The utility of FBTL is demonstrated using a fuzzy job shop scheduling problem as an example.     

多智体系统时序认知规范的SPIN模型检测

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。     

基于强相关逻辑的不精确应急时态知识表示

在强相关逻辑基础上扩展不精确时态关系,以满足不精确应急时态知识表示与推理的需要。给出了粗糙集及强相关逻辑的相关概念;通过定义不精确时态关系扩展了强相关逻辑,形成了粗糙时态强相关逻辑,给出了可靠性和完备性证明;通过实际例子说明粗糙时态强相关逻辑的知识表示和应用。结果表明扩展后的粗糙时态强相关逻辑可以实现不精确时态知识的表示与推理。     

Temporal Connectives versus Explicit Timestamps to Query Temporal Databases

Temporal databases can be queried either by query languages working directly on a timestamp representation or by languages using an implicit access to time via temporal connectives. We study the differences in expressive power between these two approaches. First, we consider temporal and first-order logic. We show that future temporal logic is strictly less powerful than past–future temporal logic and also that there are queries expressible in first-order logic with explicit timestamps that are not expressible in extended temporal logic. Our proof technique is novel and based on communication complexity. Then, we consider extensions of first-order logic with fixpoints or while-loops. Again the explicit temporal version of these languages, using timestamps, is compared with an implicit one, using instructions for moving in time. We also compare the temporal versions of the fixpoint language with those of the while language.     

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).     

Web服务组合的马氏策略规划

针对Web服务存在的业务逻辑与服务质量的不确定性,以及时序、时间窗约束,本文提出了利用马尔可夫决策理论来解决Web服务组合中最优策略规划问题的方法。该方法首先将Web服务组合描述为有向无环图表示的任务网络,网络中每个节点代表一个任务。任务是由相应的Web服务来实现,任务之间的弧线代表任务间时序的约束,任务执行应满足时间窗的约束。在此基础上,建立Web服务组合的马尔可夫决策模型,从而获得Web服务组合的最优策略。     

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

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

基于直觉模糊集的不确定时序逻辑模型

针对现有时序逻辑在描述复杂不确定时间信息方面的局限性,提出了一种基于直觉模糊集的不确定时序逻辑模型。该模型分别定义了离散论域和连续论域下的不确定点时序逻辑、点-时段时序逻辑以及时段时序逻辑的判定公式;引入直觉模糊集的犹豫度参数,使得推理结果更加精确。最后通过实例对两类不确定时间信息进行描述,并对其时序逻辑关系的可能性进行度量。通过分析表明该模型是比较优越的。     

Decidable metric logics

The common metric temporal logic for continuous time were shown to be insufficient, when it was proved that they cannot express a modality suggested by Pnueli. Moreover no finite temporal logic can express all the natural generalizations of this modality. It followed that if we look for an optimal decidable metric logic we must accept infinitely many modalities, or adopt a different formalism.Here we identify a fragment of the second order monadic logic of order with the “+1” function, that expresses all the Pnueli modalities and much more. Its main advantage over the temporal logics is that it enables us to say not just that within prescribed time there is a point where some punctual event will occur, but also that within prescribed time some process that starts now (or that started before, or that will start soon) will terminate. We prove that this logic is decidable with respect to satisfiability and validity, over continuous time. The proof depends heavily on the theory of compositionality. In particular every temporal logic that has truth tables in this logic is automatically decidable. We extend this result by proving that any temporal logic, that has all its modalities defined by means more general than truth tables, in a logic stronger than the one just described, has a decidable satisfiability problem. We suggest that this monadic logic can be the framework in which temporal logics can be safely defined, with the guarantee that their satisfiability problem is decidable.     

工作流时序约束模型分析与验证方法

为了解决工作流时间建模与时序一致性验证问题,以时序逻辑和模型检查为基础,提出了一种工作流时间建模与时序一致性验证方法.该方法用一阶逻辑描述工作流模型及其时间信息,用时序逻辑描述工作流的时序约束,用模型检查算法对时序约束进行验证与分析.该方法不是针对某一种时序约束提出来的,而是能够验证任何用时序逻辑描述的工作流时序约束.该方法还能够对未通过验证的时序约束提供工作流运行实例作为反例,帮助用户定位模型的问题.以一个工作流时间建模和时序一致性验证的实例证实了所提出方法的有效性.