有限公平环境下双相似性的公理化系统研究

19 浏览量更新于2024-08-30 收藏 412KB PDF 举报

本文探讨了"有限公平环境过程中的双相似性公理系统"这一主题。作者Han Zhu来自上海交通大学计算机科学系的基本实验室，主要聚焦于分布式并发系统行为的数学模型——过程计算。在该领域中，公平性是衡量并发系统的一个关键概念，因为它关注的是进程间的公平交互和资源分配。卡内尔利和戈德提出的移动代理计算（Calculus of Mobile Ambients, MA）是一个重要的理论框架，它扩展了传统的并发模型，引入了动态环境的概念，使得进程能够在环境中移动并进行交互。有限公平环境（Finite Fair Ambient）是对MA的特定限制，其中考虑的是有限资源下的公平行为。在研究中，作者的目标是为有限公平Ambient过程的双相似性提供一个有效的公理系统。双相似性是一种过程间的关系，当两个过程在所有可能的行为观察下表现得完全相同时，它们被认为是双相似的。这在确定进程是否具有相同性质、以及在设计和分析系统时确定何时可以替换进程方面至关重要。为了达到这个目标，作者扩展了Fair Ambient的语法，允许嵌套的环境结构被组织成前缀形式。这样的结构改进有助于简化对过程行为的分析，并且有助于构造一个直观且易于验证的公理系统。这个公理系统的核心在于提出一组明确的规则，使得判断两个有限公平Ambient过程是否等价成为一种可计算的过程，从而避免了不必要的复杂性和无穷递归。具体来说，文章可能包含了以下内容： 1. 公理系统的定义：阐述了双相似性的基本属性和定义，以及如何通过公理来刻画这种关系。 2. 语法扩展的细节：解释了如何通过添加嵌套环境结构到前缀形式，以便更好地表达有限过程的行为。 3. 有效性证明：展示了如何通过公理系统中的推理规则来证明两个过程的双相似性。 4. 应用示例：给出了几个实际的例子，展示公理系统在处理有限公平Ambient过程中的应用和效率。 5. 相关工作对比：讨论了现有方法与本文贡献的差异，以及公理系统的优点和局限性。总结起来，这篇文章为理解和验证有限公平Ambient过程中的双相似性提供了一个坚实的理论基础，对于理解和控制复杂的并发系统行为具有重要意义。通过严格的公理化方法，研究人员可以更精确地分析和比较这些系统的性质。

Axiomatic Systems for the Bisimilarity on Finite

Fair Ambient Processes

Han Zhu

Basics Lab, Department of Computer Science

Shanghai Jiao Tong University, Shanghai, China

Email: zhu-h@sjtu.edu.cn

Abstract—In this paper, we study an axiom system for the

bisimilarity on ﬁnite Fair Ambient processes. In order to

obtain normal forms of ﬁnite processes, we extended the

syntax of Fair Ambient to put the nested ambient structure

into preﬁxes. Upon our axiom system, if two ﬁnite Fair

Ambient processes are equivalent can be effectively checked.

Index Terms—Fair Ambient, Axiomatization, Bisimilarity

I. INTRODUCTION

Process calculi are mathematical models for describ-

ing and analyzing properties of distributed concurrent

systems. As a result of it, concurrent processes exhibit

more complicated behavior than traditional sequential

processes. Bisimulation relations have attracted a lot of

attention paid to giving process calculi a reasonable equiv-

alence relation. These equivalence relations are subject to

the examinations of a process’s internal states.

The Calculus of Mobile Ambients, MA for short, is

introduced by Cardelli and Gordon [1], [2], [3] as a

model that provides a uniform account for both mobile

computation and mobile computing [4]. The apparatus

introduced by MA is ambient, a piece of program residing

in a speciﬁed location. A piece of resource may move

from one ambient to another. Several variants of MA, like

Safe Ambients [5], Safe Ambients with Passwords [6],

Controlled Ambients [7] and ROAM (The Calculus of

Robust Ambients) [8] to name a few, have been proposed

to enhance the control power of MA. The Calculus of

Fair Ambient [9], or FA, has the most strict rules about

when ambients may interact. It achieves that by sticking

to the following principles:

1) First Class Citizenship: All actions are interactions

between ambients.

2) Authorization: The two ambients involved in an

interaction must obtain the authorizations from each

other.

3) Authentication: The two ambients involved in an

interaction must know each other’s identities.

It is proved in [9] that the π-calculus [10], [11] is a sub-

calculus of FA.

This work is supported by the National 973 Project (2003CB317005)

and the National Nature Science Foundation of China (60573002,

60703033).

The Turing completeness of ambient calculi defeats any

attempt to obtain a sound and complete axiom system. But

if we restrict our consideration to ﬁnite processes, some-

thing positive can be achieved. Now we are interesting

in axiomatizing the bisimilarity relation ≈ on ﬁnite Fair

Ambient processes.

Fair Ambient uses an interleaving semantics of con-

currency, just as other members of process calculi family

do. By the notion of “+”, the nondeterministic choice we

will introduce, along with the well-known expansion law,

any ﬁnite process can be rewritten into a normal form,

which in turn has the same behaviors as the original one.

That is to say, they are equivalent with respect to the

speciﬁc equivalence relation we are axiomatizing. Then an

equational theory on normal forms is given. This is the

common approach towards axiomatizing an equivalence

relation.

We adopt the common approach, but also are ex-

posed to some issues speciﬁc to FA. Besides the need

to introduce an additional operator “+”, which is not

deﬁned in the original FA, we should tackle higher order

communications, parallel operators in normal form, etc.

Fair Ambient, like its predecessor Mobile Ambient,

is inherently higher order, where processes can move

in or move out from one position (ambient) to another

position (ambient). Higher order communications, i.e.

processes can be communicated, are adopted to achieve

these movement capabilities.

To avoid introducing higher order labels in the opera-

tional semantics, we use contexts and concretions. They

are all intermediate forms of an ambient in an interaction,

not ﬁnal forms after an interaction. But in axiomatizing,

they are all required to construct the normal form of an

ambient. So we borrow them from the operational seman-

tics of FA (labeled transition system). Due to the existence

of contexts and concretions, the parallel operators can not

be fully eliminated by the expansion law in the normal

form.

Ambient capabilities should also be extended to contain

action labels from labeled transition system, and the non-

deterministic choice will be deﬁned as a guarded choice

among them to eliminate parallel composition operators to

some extent. These considerations lead to an extended fair

ambient calculi, in which each ﬁnite fair ambient will have

JOURNAL OF COMPUTERS, VOL. 4, NO. 6, JUNE 2009 469

下载后可阅读完整内容，剩余7页未读，立即下载

weixin_38502814

粉丝: 5
资源: 927

有限公平环境下双相似性的公理化系统研究

数据库armstrong公理系统，函数依赖学习攻略

用MSVL公理系统验证分布式系统

验证PPTL公理系统中的安全关键任务计划系统

多标度数据轮廓相似性的度量公理与计算 (2012年)

小学数学数学故事算术公理系统的无矛盾性

PPTL公理系统中期限驱动调度程序的形式证明

轮廓相似性度量新公理与多标度数据分析

数据库系统概论：Armstrong公理系统解析

轮廓相似性度量新探：多标度数据的公理与计算

GeoCoq: 在Coq中运用Tarski公理系统实现几何证明

最新资源