Distributed Branching Bisimulation Reduction of State Spaces

Enumerative model checking tools are limited by the size of the state space to which they can be applied. Reduction modulo branching bisimulation usually results in a much smaller state space and therefore enables model checking of much larger state spaces. We present an algorithm for reducing state spaces modulo branching bisimulation which is suitable for distributed implementation. The target architecture is a cluster with a high bandwidth interconnect. The algorithm is based on partition refinement and it works on transition systems which contain cycles of invisible steps, without eliminating strongly connected components first. To avoid fine grained parallelism, the algorithm refines the whole partition instead of just a single block in the partition. We prove correctness and also present some experimental results obtained with single threaded and distributed prototypes.     

Distributed Partial Order Reduction of State Spaces

State space explosion is a fundamental obstacle in formal verification of concurrent systems. Several techniques for combating this problem have emerged in the past few years, among which the two we are interested in are: partial order reduction and distributed memory state exploration. While the first one tries to reduce the problem to a smaller one, the other one tries to extend the computational power to solve the same problem. In this paper, we consider a combination of these two approaches and propose a distributed memory algorithm for partial order reduction.     

Bisimulation, the Supervisory Control Problem and Strong Model Matching for Finite State Machines

A fundamental relationship between the controllability of a language with respect to another language and a set of uncontrollable events in the Supervisory Control Theory initiated by (Ramadge and Wonham, 1989) and bisimulation of automata models is derived. The theoretical results relating bisimulation to controllability support an efficient solution to the Basic Supervisory Control Problem. Using (Fernandez, 1990) generalization of the partition refinement algorithm of (Paige and Tarjan, 1987), it is possible to find a partition which represents the supremal controllable sublanguage of an automaton with respect to the language of another automaton and a set of events in a worst-case running time of O( m log(n)), where m is the number of transitions and n is the number of states. Utilizing the bisimulation property of language controllability and derived relationships between automata languages and input/output finite-state machine behaviors, a precise relationship is formally derived between Supervisory Control Theory and the system-theoretic problem posed by (DiBenedetto et al., 1994) called Strong Input/Output FSM Model Matching. Specifically, it is proven that in deterministic settings instances of each problem can be mapped to the other framework and solved.     

有适应力的分布式状态估计方法

为提高智能体系统对攻击的免疫力,研究了测量攻击下的适应力分布式状态估计方法.每个智能体对系统状态进行连续的本地线性测量.由于不同智能体的本地测量模型相互异构,对系统状态可能不具有本地可观测性,且攻击者能够操控部分智能体的测量数据,随意改变其测量结果.而智能体的目标是协同处理本地测量数据,并正确估计出未知的系统状态.因此...     

分布式状态空间生成的有色petri网模型

该文旨在为分布式的状态空间生成系统设计一个有色petri网模型,并对模型进行性能分析,得出状态空间的分割对分布式系统性能的影响。基于通信时延是系统的性能瓶颈,必须使用与模型结构属性相适应的分割算法,以提高系统的加速比及分布式状态空间生成的性能。     

约简的一种启发式算法

本文揭示了约简在数量上的蕴涵的一个重要性质,由此给出又一种属性重要性的定义及相应的启发式算法,并对算法进行了详细的分析。文章最后还类似地讨论了相对约简。     

一个适用于分布式系统的快照算法

本文论述一个记录分布式系统状态的快照算法.     

分布式状态机的代数模型及其模型检验算法

分布式状态机（DSM）是一个分布式计算模型，特别适用于反应系统，有广泛的用途，但一般其正确性证明与模型检验的复杂性却很高，不易实用。作者曾提出了一个DSM的代数模型及其模型检验算法，复杂较低，但模型推导过程有点问题。该文加强了对DSM模型检验问题的提法，研究了解的结构特征，证明了可将DSM模型检验问题归结为不动点计算问题，并将Cleaveland和Steffen求不动点的方法用于同步模型不动点计算过程，然后将Bertsekas关于欧氏空间上的异步收敛定理推广到完备格上，从而将求解异步DSM方程不动点问题转化为求解同步方程不动点问题，证明了在适当的条件下，有vgEA＝vgES,vgES与vgEA分别是DSM同步方程与异步方程的大不同动点，该同步算法的复杂性为O（|S|log|TRAN|),S为状态集，TRAN为转移关系式集，利用本文结果，可以有效地克服了DSM进程之间的并发干扰所带来的各种困难，对分布式反应系统的可靠设计有很大的帮助。     

分布式系统中的全局状态算法及实现

1.引言全局状态是分布式系统中的一个关键概念,分布式系统同样需要处理在一个集中式环境中出现的如并发、互斥、死锁等问题,在分布式系统中对这些问题的处理变得更为复杂。比如在一个交易中,由于缺少全局状态信息,对可能出现的失败提供一个回滚所需的检查点(checkpoint)就变得很困难。本文将对使用全局状态的必要性及其在基于消息中间件中使用的     

属性约简的新算法

属性约简是粗糙集理论中一个核心研究问题,在对粗糙集中属性约简相关理论研究的基础上,提出了一种新的基于随机决策信息系统的属性约简算法。新算法充分利用属性依赖度所提供的信息对属性进行排序,并以一定的优化顺序来计算属性子集的信任函数或似真函数。计算结果表明:改进后的新算法计算量大大减小,尤其是当条件属性较多时,计算量的减少更加明显,从而大大提高了计算效率。计算实例验证了该算法的有效性,具有很强的优越性。     

LEO卫星网络中的一种分布式路由算法

在LEO卫星网络中,由于卫星高速运动导致的网络拓扑变化和不同卫星覆盖城内流量的非规整性给设计其特殊路由算法带来很大挑战。结合卫星网络的固有特点,本文提出一种基于路径信息压缩的分布式路由算法CPDR（Compressed Path Information based Distributed Routing）。该算法使用分布式分层链路状态收集策略和简洁的路径信息编码机制,能够在不引入额外信令开销基础之上提供多路径路由能力,实现卫星网路中的流量负载平衡、优化网络带宽应用、提高星际链路利用率。     

A Distributed Drafting Algorithm for Load Balancing

It is desirable for the load in a distributed system to be balanced evenly. A dynamic process migration protocol is needed in order to achieve load balancing in a user transparent manner. A distributed algorthim for load balancing which is network topology independent is proposed in this paper. Different network topologies and low-level communications protocols affect the choice of only some system design parameters. The "drafting" algorithm attempts to compromise two contradictory goals: maximize the processor utilization and minimize the communication overhead. The main objective of this paper is to describe the dynamic process migration protocol based on the proposed drafting algorithm. A sample distributed system is used to further illustrate the drafting algorithm and to show how to define system design parameters. The system performance is measured by simulation experiments based on the sample system.     

A Distributed Memory Algorithm for Lexicon Building

A parallel algorithm for preparing word frequency concordances over two specified sets of documents from a collection is presented. Good parallel efficiency is demonstrated on a 128-node distributed memory machine using sets whose combined size exceeds one gigabyte. It is demonstrated that efficiency is heavily influenced by hashing and communication strategies. A two-stage hashing algorithm is proposed to reduce communication overhead. Ways of increasing capacity are considered, and the applicability of the algorithm to other text-processing functions such as index and symbol-table building is outlined.     

分布式系统中的一类任务分配算法

本文提出了分布式系统中各独立结点根据自身状态和系统反馈进行自适应，以使系统达到最优状态的一种机制。它突破了以往相关工作的一些重要限制，性能得到了很大的改善。     

求解有度约束多播路由问题的分布式算法

在应用多播(multicast)时,有效的多播路由是关键.现有的多播路由算法一般假定每个节点都支持multicast,但在实际网络中,某些节点并不支持多播,而为了保证网络速度,需限制进行多播所要复制信息的数量.为此,采用度约束来表示每个节点的多播能力,提出了一种有度约束的分布式多播路由算法.算法的复杂度和所需传递信息的数量都低于已有的同类算法.     

一种快速求强规划解的算法

为提高求解效率,设计一种求强规划解的简化分层算法。以传统分层算法为基础,引入贪心选择策略,对每个非目标状态的动作进行筛选,去除对求解强规划解无益的动作,加快状态向下搜索的速度,并在改进分层的基础上,优化求强规划解策略,由于在求解过程中会存在大量重复搜索,因此建立一个集合保存已访问状态的信息,避免对状态的重复搜索。分析结果表明,在初始状态到达目标状态路径都不重合的情况下,改进算法的时间复杂度为O( nm)( n为初始状态个数,m为层数),在都重合情况下为O( m),优于普通正向搜索算法与反向搜索算法。     

一个移动进程演算的互模拟同余定义框架

并发计算模型是理论计算机科学研究的重要领域之一。以π演算为代表的移动进程演算是目前并发理论的研究热点。互模拟等价定义是移动进程演算研究中的核心概念和问题,而传名机制使得移动进程演算中的互模拟同余关系更加复杂和有趣。本文在分析了常见的互模拟同余定义的基础上,通过抽取定义的核心要素,提出了一个三维的互模拟同余定义模型,从而将一般文献中常见的互模拟定义纳入到一个统一的框架中来,加深了我们对移动进程演算中互模拟概念的理解;同时本文利用这个模型,系统分析了各种互模拟之阿的关系。模型的优点在于它的普适性和开放性。     

一种求上近似约简的快速启发式算法

利用时间复杂度为O(|C||U|求U/C的快速算法,设计了一种基于属性重要度的上近似约简快速启发式算法,将时间复杂度降为O(|C|2|D||U|),该算法在处理拥有海量数据的决策表时,具有高效性.     

A Polynomial-Time Algorithm for Memory Space Reduction

Reducing memory space requirement is important to many applications. For data-intensive applications, it may help avoid executing the program out-of-core. For high-performance computing, memory space reduction may improve the cache hit rate as well as performance. For embedded systems, it can reduce the memory requirement, the memory latency and the energy consumption. This paper investigates program transformations which a compiler can use to reduce the memory space required for storing program data. In particular, the paper uses integer programming to model the problem of combining loop shifting, loop fusion and array contraction to minimize the data memory required to execute a collection of multi-level loop nests. The integer programming problem is then reduced to an equivalent network flow problem which can be solved in polynomial time.     

一种条件向量约简的启发式算法

粗糙决策支持方法是一组用于决策支持的粗糙分析方法,该方法能够充分挖掘决策表的决策能力,以提供强有力的决策支持,并且本质上提供容错的决策支持,条件向量约简是这一方法的重要研究内容。论文以决策强度、条件向量的覆盖度和属性的重要性为启发式信息,提出了条件向量约简的一种启发式算法,通过实验验证了该算法是有效的。