A Coalgebraic View of Infinite Trees and Iteration

The algebra of infinite trees is, as proved by C. Elgot, completely iterative, i.e., all ideal recursive equations are uniquely solvable. This is proved here to be a general coalgebraic phenomenon: let H be an endofunctor such that for every object X a final coalgebra, TX, of H(_) + X exists. Then TX is an object-part of a monad which is completely iterative. Moreover, a similar contruction of a “completely iterative monoid” is possible in every monoidal category satisfying mild side conditions.     

Substitution in Non-wellfounded Syntax with Variable Binding

Inspired from the recent developments in theories of non-wellfounded syntax (coinductively defined languages) and of syntax with binding operators, the structure of algebras of wellfounded and non-wellfounded terms is studied for a very general notion of signature permitting both simple variable binding operators as well as operators of explicit substitution. This is done in an extensional mathematical setting of initial algebras and final coalgebras of endofunctors on a functor category. In the non-wellfounded case, the fundamental operation of substitution is more beneficially defined in terms of primitive corecursion than coiteration.     

Trace Machines for Observing Continuous-Time Markov Chains

In this paper, we study several linear-time equivalences (Markovian trace equivalence, failure and ready trace equivalence) for continuous-time Markov chains that refer to the probabilities for timed execution paths. Our focus is on testing scenarios by means of push-button experiments with appropriate trace machines and a discussion of the connections between the equivalences. For Markovian trace equivalence, we provide alternative characterizations, including one that abstracts away from the time instances where actions are observed, but just reports on the average sojourn times in the states. This result is used for a reduction of the question whether two finite-state continuous-time Markov chains are Markovian trace equivalent to the probabilistic trace equivalence problem for discrete-time Markov chains (and the latter is known to be solvable in polynomial time).     

子共代数与共同余共关系

共代数方法是近几年来理论计算机科学的研究热点之一,在并行计算模型、自动机及面向对象技术的理论基础方面有着广泛的应用.以范畴理论为工具讨论子共代数的性质,特别是集合范畴上的子共代数的性质,证明了集合范畴上的子共代数都是正则子共代数.进一步利用共同余共关系与子共代数之间的对应,给出了集合范畴上共生成子共代数的一种构造方式.     

Generic Composition

This paper presents a technique called generic composition to provide a uniform basis for modal operators, sequential composition, different kinds of parallel compositions and various healthiness conditions appearing in a variety of semantic theories. The weak inverse of generic composition is defined. A completeness theorem shows that any predicate can be written in terms of generic composition and its weak inverse. A number of algebraic laws that support reasoning are derived. Received May 2000 / Accepted in revised form May 2002     

消息序列图的范畴论语义描述

消息序列图(MSC)作为一种描述和规范系统部件之间交互行为的图文语言,对实例和消息等元素本身没有相应的描述结构,使得描述功能扩展有诸多限制.为了增强MSC描述的精确性与灵活性,对其进行语义形式化.在原有消息机制的基础上,采用范畴论的数学方法,给出MSC的语义描述结构,并对其结构进行扩展,增强带时间概念的MSC描述功能.     

基于迹语义的网络安全协议形式化分析

形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段.本文提出了一种新的简单的迹语义,用于刻画协议部分安全性质,即只针对协议规约的单个主体,此技术支持协议设计者对安全性质进行形式化规约.运用此技术和模型检测器SPIN找到了两种针对TMN协议的攻击,证明了此方法的实用性,可方便地用于其它网络安全协议验证.     

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.     

针对LBlock算法的踪迹驱动Cache攻击

LBlock是一种轻量级分组密码算法,其由于优秀的软硬件实现性能而备受关注。目前针对LBlock的安全性研究多侧重于抵御传统的数学攻击。缓存( Cache)攻击作为一种旁路攻击技术,已经被证实对密码算法的工程实现具有实际威胁,其中踪迹驱动Cache攻击分析所需样本少、分析效率高。为此,根据LBlock的算法结构及密钥输入特点,利用访问Cache过程中密码泄露的旁路信息,给出针对LBlock算法的踪迹驱动Cache攻击。分析结果表明,该攻击选择106个明文,经过约27.71次离线加密时间即可成功恢复LBlock的全部密钥。与LBlock侧信道立方攻击和具有Feistel结构的DES算法踪迹驱动Cache攻击相比,其攻击效果更明显。     

Trace representation and linear complexity of binary sequences derived from Fermat quotients

We describe the trace representations of two families of binary sequences derived from the Fermat quotients modulo an odd prime p （one is the binary threshold sequences and the other is the Legendre Fermat quotient sequences） by determining the defining pairs of all binary characteristic sequences of cosets, which coincide with the sets of pre-images modulo p2 of each fixed value of Fermat quotients. From the defining pairs, we can obtain an earlier result of linear complexity for the binary threshold sequences and a new result of linear complexity for the Legendre Fermat quotient sequences under the assumption of 2p-1≠ 1 mod p2.     

Software Trace Cache for Commercial Applications

In this paper we address the important problem of instruction fetch for future wide issue superscalar processors. Our approach focuses on understanding the interaction between software and hardware techniques targeting an increase in the instruction fetch bandwidth. That is the objective, for instance, of the Hardware Trace Cache (HTC). We design a profile based code reordering technique which targets a maximization of the sequentiality of instructions, while still trying to minimize instruction cache misses. We call our software approach, Software Trace Cache (STC). We evaluate our software approach, and then compare it with the HTC and the combination of both techniques. Our results on PostgreSQL show that for large codes with few loops and deterministic execution sequences the STC offers better results than a HTC. Also, both the software and hardware approaches combine well to obtain improved results.     

Agent的遗传理论

Agent是指具有智能的人或其它智能物．它有自治、推测、反响、协作、自学习和相互学习等能力，基于此，本文借助数学工具，对Agent进行深入研究，给出Agent的遗传理论，进一步丰富Agent的理论内容．     

基于Agent的分布式模型形式化语义描述

为解决分布式系统构建过程中系统组合和语义验证等方面的问题,基于范畴理论和进程代数,为基于Agent的分布式系统模型提出了一种形式化的语义描述框架。范畴图表用于描述整个系统的结构模型,态射用来表示系统各组成部分之间的交互和协作机制。在此基础上,对Agent规范的描述、组合、精化以及迁移过程中的语义保持问题进行了探讨。应用研究表明,该框架适用于分布式系统模型的描述和构建,有助于分析系统分解和组合的正确性。     

基于变维分形理论的卡尔曼滤波实时跟踪预测模型在股票价格预测中的应用

基于卡尔曼滤波的动态、实时性以及股票市场的分形特性,论文首创利用变维分形理论来建立关于股票市场的卡尔曼滤波状态方程和观测方程,提出了一种新的基于变维分形理论的卡尔曼滤波实时跟踪预测模型和算法。实例仿真结果分析表明,论文提出的算法具有可靠、计算简便、快速等特点,模型预测精度较高,并可实现实时跟踪预测,具有一定的理论价值和实用价值。     

PID控制的应用与理论依据

PID控制是自动控制中产生最早,应用最广的一种控制方法,从PID控制的结构形式,实际控制工程需求和实现条件分析了PID控制的独特优点,同时又介绍了二阶线性定常系统PID控制器的设计方法,叙述了高阶线性定常系统的特征建模原理,重点分析和推导了基于特征模型的带消除静差的二次型最优控制设计方法,证明了高阶线性定常系统和一大批非线性系统能用PID控制器实现位置恒值控制的基本原理,为随输出状态不同而选择不同P,I,D参数等各种人工调节方法提供了合理性解释,最后说明了PID控制器结构是智能控制的一种最基础单元。     

基于EXT3系统的文件内容操作痕迹提取软件设计

EXT3文件系统是大多数Linux主机的默认硬盘分区格式,EXT3格式的硬盘中可能存储了大量涉案文件,识别出嫌疑人对这些涉案文件内容执行的增、删、改操作行为,提取出被修改的相关数据对公安机关的调查、取证工作有重要意义。文章对不同类型文件的操作痕迹进行了分析;介绍了EXT3日志文件的基本结构;研究了从日志中提取出文件名称和inode结点信息的方法;提出了基于inode编号链表的操作痕迹提取方法;设计了用于痕迹提取的状态转换机。设计的操作痕迹提取软件可以直接运行在Linux主机上,通过扫描日志文件完成痕迹提取,经过大量实际测试,软件可以有效提取EXT3文件系统中未被覆盖的操作痕迹。     

嵌入式处理器中跟踪缓冲的设计考虑

跟踪缓冲可以记录程序执行的历史轨迹,这在各种在线仿真器(ICE)和逻辑分析仪中得到了广泛的应用．文章主要讲述了嵌入式系统中的跟踪缓冲的设计思想。并介绍了嵌入式系统领域中的不同架构处理器中跟踪缓冲的设计方法,对它们所表现的性能差异也进行了简单的评估．