Petri网弱公平性的判断

本文提出了弱公平网的概念，并给出了判断一个Ｐｅｔｒｉ网是否是弱公平同的一组充分必要条件。

对等网络中的基本弱公平资源交换协议

对等计算(P2P)可在Internet或者自组网边界进行计算,从而可提供一种全新的应用模式。从对等计算与公平交换的基本概念入手,讨论了协议中的基本假设,设计了一个适合于对等网络的基本弱公平交换协议(BWFEP),并对协议的交互过程做了详尽分析。对BWFRP协议公平性的分析结果表明,该协议具有无需可信第三方(TTP)、简单、弱公平性的特点,从而适合于对等网络中用户之间直接资源交换的需要。

Petri网系统的弱公平性判定

本文首先给出了一个Petri网系统的有效可重复向量的两个性质.随后,又给出了用有效可重复向量判断Petri网系统弱公平性相关问题的一个充分必要条件.在一个Petri网系统中,任意的两个变迁ti,tj,则tj弱公平依赖于ti,当且仅当不存在这样的有效可重复向量X,使得X(j)>0且X(i)=0.最后,用一个实例展示结论的应用过程.

Petri网弱公平性和公平性关系的进一步研究

在Petri网中,公平性概念的引入是为了讨论网系统中两个变迁发生之间的相互关系。这种关系可以很好地反映出模拟系统的各个事件在资源竞争中的有无饥饿性问题。文中基于弱公平性和公平性的定义与联系,证明了对于有界Petri网,满足弱公平性就满足公平性;同时证明了在两类无界Petri网中,可由弱公平性推导出公平性。并进一步证明其他类型的无界Petri网是不满足公平性的,即无法从弱公平性直接推导出公平性。

行为时态逻辑TLA定理系统证明及公平性研究

行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向。为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统。在此基础上严格的证明了TLA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件。最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型。

Petri网中亚公平关系与亚公平网

Petri网中的弱公平但不公平的关系称为亚公平公系 ,由此可引伸出亚公平Petri网和亚公平网等概念。本文证明了一个重要性质 :亚公平Petri网中一定存在着公平关系 ,并在此基础上讨论了亚公平网中的公平分支划分。此外 。

公平性分类及其分析

本文对不同通信及协调机制的程序设计语言的公平性问题进行了讨论。本文的讨论基于一般的转换系统模型，此模型为我们统一地处理不同机制的语言提供了一个基础。文中给出了三类公平性概念：弱公平性、进程公平性和强公平性。我们进一步对每一类公平性进行了分析，特别，我们对它们的实现及它们对程序验证的影响进行了讨论。文中最后，我们得到结论：不同通信及协调机制需要不同的公平性假设。为了便于实现以及得到更一般的结论，我们应该尽可能使用较弱的公平性假设。

Petri网中的公平依赖体系研究

本文给出了弱公平依赖的严格定义 ,及亚公平依赖、弱公平依赖关系的判定条件 .从而使了公平依赖关系也同公平关系一样成为一个严格体系 ,并给出了公平依赖体系的图形表示 .使公平依赖关系的研究可部分的借鉴公平体系研究的成果 。

Petri网并运算的性质研究

进一步研究了Petri网的并运算,讨论了这种运算保持网的动态及结构性质的条件。

Petri网的依赖关系

为了分析变迁不处于公平关系或弱公平关系时在运行中的依赖关系 ,本文提出了公平依赖和弱公平依赖的概念 .研究了伪可重复向量的性质及在判断公平依赖关系时起的作用 .给出了判断变迁处于公平依赖关系和弱公平依赖关系的充分必要条件 .

带抑制弧Petri网的保性变换

Petri网的保性化简是Petri网分析的一种重要途径。带抑制弧的增广Petri网在计算能力上与图灵机等价。针对带抑制的增广Petri网中串联变迁和串联库所两类情况进行了较深入的分析,在给出了相关化简方法的基础上,证明了通过这些化简规则所得到的网系统与原网在活性、有界性、弱公平性等动态性质上仍保持一致。