进程代数入门：理解系统行为的数学框架

5星 · 超过95%的资源需积分: 19 60 浏览量更新于2023-03-03 收藏 1005KB PDF 举报

"Introduction to Process Algebra by Wan Fokkink" 进程代数，也称为过程代数，是一种数学框架，主要用于描述和分析系统的行为，特别是并发系统的行为。在计算机科学领域，"过程"通常指的是软件系统执行的动作或发生的事件。一个系统可能包含一系列的动作，如转换文件格式，或者一连串的事件，如格式转换完成的通知。系统的行为可以从多个角度进行观察和抽象，这有助于研究人员理解和简化复杂的系统。《Introduction to Process Algebra》是由Wan Fokkink撰写的一本关于该主题的计算机科学专著。这本书的第二版于2007年由Springer-Verlag出版社出版，它提供了一个深入学习进程代数的平台。随着计算机软件和网络协议在日常生活中的重要性日益增加，以及软件复杂度的迅速增长，正确性变得至关重要。为了应对这些挑战，新的方法和技术，如进程代数，被发展出来以结构化不断增长的计算机技术领域。并发性是系统行为的关键特征，也是造成复杂性的一个主要原因。当简单的行为在并行执行时，其复杂性可能会急剧增加。因此，进程代数的核心是将系统分解为并发组件，以便详细研究这些行为。通过代数表达式，它提供了操纵和分析系统行为的有效工具，这在发现软件和硬件系统的缺陷中起着关键作用。在这个框架下，进程代数引入了一种平行操作的概念，允许同时处理多个行为。此外，它还涵盖了通信和同步机制，这些都是并发系统设计中的重要方面。例如，Communicating Sequential Processes (CSP) 是一种流行的过程代数理论，它强调了进程之间的通信如何影响整体系统的行为。标签“ccs”可能指的是蔡斯-斯科特进程代数（ CCS，Calculus of Communicating Systems），这是一种简洁的过程代数形式，用于描述分布式计算系统。而“csp”则直接与亨尼翁的CSP理论相关，它提供了一种形式化的语言来表达并发系统的交互和同步。进程代数是理解、建模和验证并发系统行为的重要工具。通过代数公式，可以更清晰地表达系统动态，并进行形式验证，确保系统的正确性和可靠性。《Introduction to Process Algebra》作为一本专业书籍，为读者提供了深入了解这一领域的基础和深入洞察。

2.3 Bisimulation Equivalence 11

The ﬁrst process reads datum d, and then decides whether it writes d on

disc 1 or on disc 2. The second process makes a choice for disc 1 or disc

2 before it reads datum d. Both processes display the same strings of ac-

tions, read(d)write

(d) and read(d)write

(d), so they are trace equivalent.

Still, there is a crucial distinction between the two processes, which becomes

apparent if for instance disc 1 crashes. In this case the ﬁrst process always

saves datum d on disc 2, while the second process may get into a deadlock

(i.e., may get stuck).

Bisimulation equivalence (see Deﬁnition B.3.2) discriminates more pro-

cesses than trace equivalence. Namely, if two processes are bisimilar, then

not only they can execute exactly the same strings of actions, but also they

have the same branching structure. For example, the two processes in Exam-

ple 2.3.1 are not bisimilar. Deﬁnition B.3.2 is presented below for the relations

→ and the predicates

→

√

, for a ∈ A.

Deﬁnition 2.3.1 (Bisimulation). A bisimulation relation B is a binary

relation on processes such that:

1. if p Bq and p

→ p

, then q

→ q

with p

;

2. if p Bq and q

→ q

, then p

→ p

with p

;

3. if p Bq and p

→

√

, then q

→

√

;

4. if p Bq and q

→

√

, then p

→

√

Two processes p and q are bisimilar, denoted by p ↔

q, if there is a bisimu-

lation relation B such that p Bq.

Example 2.3.2. (a + a)b ↔ ab + a(b + b).

A bisimulation relation that relates these two basic process terms is deﬁned

by (a + a)b Bab + a(b + b), b Bb, and b Bb + b. This bisimulation relation can

be depicted as follows:

b b + b

(a + a)b ab + a(b + b)

√ √

a a

Exercise 2.3.1. Say for each of the following pairs of basic process terms

whether they are bisimilar:

- (b + c)a + ba + ca and ba + ca;

- a(b + c) + ab + ac and ab + ac;

- (a + a)(bc) + (ab)(c + c) and (a(b + b))(c + c).

2.4 Axioms for BPA 13

Table 2.2 presents an axiomatisation E

BPA

for BPA modulo bisimulation

equivalence. The variables x, y, and z in the axioms range over the collection

of basic process terms. The equality relation on basic process terms induced

by the axiomatisation E

BPA

is obtained by taking the set of closed substitu-

tion instances (see Deﬁnition A.1.3) of axioms in E

BPA

, and closing it under

equivalence and contexts; see Deﬁnition A.2.2.

Exercise 2.4.1. Prove that the axioms A1-3 are equivalent to axiom A3

together with

(x + y) + z = y + (z + x).

The equality relation that E

BPA

induces on BPA is closed under contexts.

So in order to conclude that this equality relation is sound and complete

for BPA modulo bisimulation, we need to know that this equivalence is a

congruence (see Deﬁnition B.3.3) with respect to BPA. That is, if s ↔

and

t ↔ t

, then s + t ↔ s

+ t

and s·t ↔ s

·t

Theorem 2.4.1. Bisimulation equivalence is a congruence with respect to

BPA.

Proof. The transition rules in Table 2.1 are in panth format (see Deﬁnition

B.3.4). So the bisimulation equivalence that they induce is a congruence; see

Theorem B.3.1. 2

Exercise 2.4.2. Verify that the TSS of BPA is in panth format.

Theorem 2.4.2. E

BPA

is sound for BPA modulo bisimulation equivalence.

Proof. Since bisimulation is both an equivalence and a congruence for BPA,

we only need to check that the ﬁrst clause in the deﬁnition of the relation =

is sound. That is, if s = t is an axiom in E

BPA

and σ a closed substitution

that maps the variables in s and t to basic process terms, then we need to

check that σ(s) ↔

σ(t). We only provide some intuition for soundness of the

axioms in Table 2.2:

• A1 (commutativity of +) says that both s+t and t+s represent a choice

between s and t;

• A2 (associativity of +) says that both (s + t) + u and s + (t + u)

represent a choice between s, t, and u;

• A3 (idempotency of +) says that a choice between t and t amounts to a

choice for t;

• A4 (right distributivity of ·) says that both (s + t)·u and s·u + t·u

represent a choice between s and t, followed by u;

• A5 (associativity of ·) says that both (s·t)·u and s·(t·u) represent s

followed by t followed by u.

14 2. Basic Process Algebra

These intuitions can be made rigorous by means of explicit bisimulation re-

lations between the left- and right-hand sides of closed instantiations of the

axioms in E

BPA

. Hence, all such instantiations are sound modulo bisimulation

equivalence. 2

Note that left distributivity of sequential composition, i.e., x·(y + z) =

x·y + x·z, is in general not sound modulo bisimulation equivalence; see Ex-

ercise 2.3.2.

Exercise 2.4.3. Prove that s + t ↔

t + s, (s + t)u ↔ su + tu, and (st)u ↔

s(tu) for all basic process terms s, t, and u.

It remains to prove that E

BPA

is complete for BPA modulo bisimulation

equivalence, meaning that s ↔ t implies s = t. The following completeness

proof is based on turning the axiomatisation E

BPA

into a TRS (see Deﬁnition

A.4.1), by directing the axioms from left to right.

Theorem 2.4.3. E

BPA

is complete for BPA modulo bisimulation equiva-

lence.

Proof. We consider basic process terms modulo associativity and commuta-

tivity (AC) of the +, and this equivalence relation is denoted by =

; see

Section A.4. That is, s =

t if and only if s and t can be equated by axioms

A1 and A2. A basic process term s then represents the collection of basic

process terms t such that s =

t. Each equivalence class s modulo AC of

the + can be represented in the form s

+ ··· + s

with each s

either an

atomic action or of the form t

·t

; we refer to the subterms s

, . . . , s

as the

summands of s.

The three remaining axioms A3-5 are turned into rewrite rules, by direct-

ing them from left to right:

x + x → x

(x + y)·z → x·z + y·z

(x·y)·z → x·(y·z)

These rewrite rules are applied to basic process terms modulo AC of the +.

For example, none of the three rewrite rules applies to (a + b) + a, but

(a + b) + a =

b + (a + a) → b + a.

The TRS is terminating (see Deﬁnition A.4.4) modulo AC of the +. That

is, each reduction of a basic process term ends up in a normal form n (see

Deﬁnition A.4.3), meaning that the rewrite rules do not apply to any of the

basic process terms that are equivalent to n modulo AC of the +. This follows

from the weight function (cf. Example A.4.2) on basic process terms that is

deﬁned inductively as follows, where v ranges over A. The symbol

∆

= stands

for “equals by deﬁnition”.

2.4 Axioms for BPA 15

weight(v)

∆

= 2

weight(s + t)

∆

= weight(s) + weight(t)

weight(s·t)

∆

= weight(s)

·weight(t).

(Here, + and · refer to addition and multiplication on the natural numbers,

respectively.) It is not hard to see that each application of a rewrite rule

strictly decreases the weight of a basic process term, and that moreover basic

process terms that are equivalent modulo AC of the + have the same weight.

Since each sequence of natural numbers k

> k

> ··· is ﬁnite, it follows

that the TRS is terminating modulo AC of the +.

Owing to the forms of the left-hand sides of the three rewrite rules, normal

forms are built from distinct summands a and as, with a an atomic action

and s a normal form. We prove for normal forms n and n

that n ↔

implies

n =

. The proof is based on induction with respect to the sizes of n and

, meaning the number of function symbols that they contain. Let n ↔ n

• Consider a summand a of n. Then n

→

√

, so n ↔ n

implies n

→

√

meaning that n

also contains the summand a.

• Consider a summand as of n. Then n

→ s, so n ↔

implies n

→ t with

s ↔

t, meaning that n

contains a summand at. Since s and t are normal

forms and have sizes smaller than n and n

, respectively, by induction s ↔ t

implies s =

Hence, each summand of n is also a summand of n

. Vice versa, each summand

of n

is also a summand of n. In other words, n =

Finally, let the basic process terms s and t be bisimilar. The TRS is

terminating modulo AC of the +, so it reduces s and t to normal forms n

and n

, respectively. Since the rewrite rules and equivalence modulo AC of

the + can be derived from the axioms, s = n and t = n

. Soundness of the

axioms then yields s ↔

n and t ↔ n

, so n ↔ s ↔ t ↔ n

. We showed that

n ↔ n

implies n =

. Hence, s = n =

= t. 2

The proof of Theorem 2.4.3 points out a mechanised way to verify whether

two basic process terms are bisimilar. First, reduce both basic process terms

to a normal form, by means of the rewrite rules. Next, check whether the two

resulting normal forms are equivalent modulo AC of the +. If so, then the

original terms are bisimilar; if not, then the original terms are not bisimilar.

Exercise 2.4.4. Verify for the TRS in the proof of Theorem 2.4.3 that if

s → t then weight(s) > weight(t), and if s =

t then weight(s) ≡ weight(t).

Exercise 2.4.5. Suppose the deﬁnition of the weight function in the proof of

Theorem 2.4.3 would be adapted by putting weight(s·t)

∆

= weight(s)·weight(t).

Give basic process terms s and t of the same weight such that s → t.

Example 2.4.1. We equate the bisimilar basic process terms (a + b) + a and

(b + a) + b. First, they are reduced to normal form:

剩余173页未读，继续阅读

wofy2008

粉丝: 3
资源: 14

进程代数入门：理解系统行为的数学框架

进程代数入门教材

一份对进程代数的简要介绍

进程代数入门（第二版）

Introduction to Process Algebra

Introduction to process algebra.pdf

introduction to linear algebra线性代数pdf

Introduction to Linear Algebra 麻省理工线性代数答案

矩阵代数简介Introduction to Matrix Algebra

从几何到代数-线性代数简介From Geometry to Algebra - An Introduction to Linear Algebra

introduction to linear algebra

最新资源