没有合适的资源?快使用搜索试试~ 我知道了~
Introduction to process algebra.pdf
需积分: 10 11 下载量 87 浏览量
2015-03-14
18:45:42
上传
评论
收藏 1005KB PDF 举报
温馨提示
试读
174页
Introduction to process algebra.pdf,英文原版,学习算法的入门教材
资源推荐
资源详情
资源评论
Wan Fokkink
Introduction to Process Algebra
Computer Science – Monograph (English)
2nd edition
April 10, 2007
Springer-Verlag
Berlin Heidelberg NewYork
London Paris Tokyo
Hong Kong Barcelona
Budapest
Preface
Computer software and network protocols are increasingly important in daily
life. At the same time the complexity of software has rocketed, so that its
correctness is at stake. New methodologies and disciplines are being devel-
oped to bring structure to the ever growing jungle of computer technology.
(Semi-)automated manipulation has become an important means in discover-
ing flaws in software and hardware systems. Process algebra is a mathematical
framework in which system behaviour is expressed in the form of algebraic
terms, enhancing the available techniques for manipulation.
Concurrency is omnipresent in system behaviour, and in a large part
responsible for its complexity: even simple behaviours become wildly compli-
cated when they are executed in parallel. In order to study such systems in
detail, it is imperative that they are dissected into their concurrent compo-
nents. Fundamental to process algebra is a parallel operator, to break down
systems into their concurrent components. A set of equations is imposed
to derive whether two terms are behaviourally equivalent. In this framework,
non-trivial properties of systems can be established in an elegant fashion. For
example, it may be possible to equate an implementation to the specification
of its required input/output relation. In recent years a variety of automated
tools have been developed to facilitate the derivation of such properties.
Applications of process algebra exist in diverse fields such as safety criti-
cal systems, network protocols, and biology. In the educational vein, process
algebra has been recognised to teach skills to deal with complex concurrent
systems, by representing and reasoning about such systems in a mathemati-
cally clear and precise manner.
This text developed from an undergraduate course on process algebra at
the computer science department of the University of Wales Swansea during
the autumn of 1997 and of 1998. Chapters 2-7 contain sufficient material
for more than twenty hours of lecturing; a set of slides and further mate-
rial to support such a course are available from my homepage (currently
at http://www.cwi.nl/∼wan). It is recommended to use a tool set based on
process algebra, such as the µCRL tool set, the Concurrency Workbench Ed-
inburgh, or the Labelled Transition System Analyser to enliven the course.
µCRL specifications of the protocols in Chapter 6 can be obtained from the
VI Preface
author. Appendices A and B provide useful background information; they
are not intended to be included in the course.
I am grateful to John Tucker for his encouragement to further develop a
raw set of lecture notes, and to Judi Romijn for her support. Over the years
I have benefited from discussions with Jan Bergstra, Rob van Glabbeek, Jan
Friso Groote, Frits Vaandrager, Alban Ponse, Chris Verhoef, Jaco van de
Pol, Jos Baeten, Luca Aceto, Jos van Wamel, Steven Klusener, Bas Luttik,
Dennis Dams, and many others.
Amsterdam, November 1999 Wan Fokkink
Contents
1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
2. Basic Process Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.1 Basic Process Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.2 Transition Rules for BPA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.3 Bisimulation Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.4 Axioms for BPA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3. Algebra of Communicating Processes . . . . . . . . . . . . . . . . . . . . . 19
3.1 Parallelism and Communication . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.2 Left Merge and Communication Merge . . . . . . . . . . . . . . . . . . . . 21
3.3 Axioms for PAP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3.4 Deadlock and Encapsulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4. Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.1 Guarded Recursive Specifications . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.2 Transition Rules for Guarded Recursion . . . . . . . . . . . . . . . . . . . 35
4.3 Recursive Definition and Specification Principles . . . . . . . . . . . 38
4.4 Completeness for Regular Processes . . . . . . . . . . . . . . . . . . . . . . . 41
4.5 Approximation Induction Principle . . . . . . . . . . . . . . . . . . . . . . . 44
5. Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
5.1 Rooted Branching Bisimulation Equivalence . . . . . . . . . . . . . . . 49
5.2 Guarded Linear Recursion Revisited . . . . . . . . . . . . . . . . . . . . . . 53
5.3 Axioms for the Silent Step . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
5.4 Abstraction Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.5 An Example with Buffers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
5.6 Cluster Fair Abstraction Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
6. Protocol Verifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.1 Alternating Bit Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.2 Bounded Retransmission Protocol . . . . . . . . . . . . . . . . . . . . . . . . 80
6.3 Verification Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
6.4 Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
VIII Contents
7. Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
7.1 Renaming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
7.2 State Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
7.3 Priorities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
7.4 Further Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
A. Equational Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
A.1 Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
A.2 Axiomatisations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
A.3 Initial Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
A.4 Term Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
B. Structural Operational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 123
B.1 Transition System Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . 123
B.2 The Meaning of Negative Premises . . . . . . . . . . . . . . . . . . . . . . . 125
B.3 Bisimulation as a Congruence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
B.4 Branching Bisimulation as a Congruence . . . . . . . . . . . . . . . . . . 132
B.5 Conservative Extension . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136
B.6 Modal Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
Solutions to Selected Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
剩余173页未读,继续阅读
资源评论
Sidney_VonWunderland
- 粉丝: 10
- 资源: 8
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功