没有合适的资源?快使用搜索试试~ 我知道了~
资源推荐
资源详情
资源评论
Lecture Notes in
Computer Science
Edited by G. Goos and J. Hartmanis
92
IIII
Robin Milner
A Calculus of
Communicating
Systems
Springer-Verlag
Berlin Heidelberg
New York 1980
Editorial Board
W. Brauer P. Brinch Hansen D. Gries C. Moler G. SeegmiJIler
J..q;toer N. Wirth
Author
Robin Milner
University of Edinburgh
Dept. of Computer Science
James Clerk Maxwell Building
The King's Buildings
Mayfield Road
Edinburgh EH9 3JZ
Great Britain
AMS Subject Classifications (1979): 68-02
CR Subject Classifications (1974): 4.30, 5.20, 5.22, 5.24
ISBN 3-540-10235-3 Springer-Verlag Berlin Heidelberg New York
ISBN
0-38?-10235-3
Springer-Verlag NewYork Heidelberg Berlin
Library of Congress Cataloging in Publication Data. Milner, Robin. A calculus of
communicating systems. (Lecture notes in computer science; 92) Bibliography: p.
Includes index, t. Machine theory. 2. Formal languages. I. Title. 11. Series.
CIA26?.M53. 511.3 80-21068
This work is subject to copyright. All rights are reserved, whether the whole or part
of the material is concerned, specifically those of translation, reprinting, re-use of
illustrations, broadcasting, reproduction by photocopying machine or similar means,
and storage in data banks. Under § 54 of the German Copyright Law where copies
are made for other than private use, a fee is payable to the publisher, the amount of
the fee to be determined by agreement with the publisher.
© by Springer-Verlag Berlin Heidelberg 1980
Printed in Germany
Printing and binding: Beltz Offsetdruck, Hemsbach/Bergstr.
9145/3140-543210
work was mainly done during my six-month appo_ in--t, frcm
~t 1979 to January 1980, at the Ommouter Science deoalb~ent in
Aarhus University, ~k. Although much of the ground work had been
done previously it was mainly in response to their encouragement (to
make the theory more accessible and related to practice), and to their
informed criticism, that the material reached a scmewhat coherent form.
I an deeply grateful to them and their students for allowing me to
lecture once a week on what was, at first, a loosely connected set of
ideas, and for the welccming enviromnent in which I was able to put
the ideas in order. I also thank Edinburgh University for awarding me
five months sabbatical leave subsequently, which helped me to cc~plete
the task in a reasonable time.
The calculus presented here 9~ew out of work which was inspired
by Dana Scott's theory of computation, though it has since diverged
in some respects. At every stage I have been influenced by Gordon
Plotkin; even where I cannot trace particular ideas to him I have
been greatly illtmlinated by our discussions and by his chance remarks,
and without them the outccme would certainly be less than it is. I
would also like to thank others with whom I have worked: George Milne,
with whom I worked out the Laws of Flow Algebra; Matthew Hennessy, with
whcm the notion of observation equivalence developed; and Tony Hoare,
whose parallel work cn different but strongly related ideas, expressed
in his "Ccamtmicating Sequential Processes", has been a strong stimulus.
Many people have given detailed and helpful criticisms of the manu-
script, and thus improved its final form. In particular I thank Michael
Gordon and David MacQueem, who went through it all in detail in a Seminar
at the Information Sciences Institute, University of California; this
not only exposed same mistakes and obscurities but gave me more csnfidence
in the parts they didn't criticise.
Finally, I am very thank~=ul to Dorothy McKie and Gina Temple for
their patience and skill in the long and involved task of typing.
O.
!.
2.
3.
Introduction
Purpose - Character - Related ~rk - Evolution - Outline.
Emperimentin 9 on Nondeterministic Machines
Traditional equivalence of finite state acceptors - Exper~ting
upon acceptors - Behaviour as a tree - Algebra of RSTs -
Unobservable acticns.
S[nchronizaticn
Mutual experimentation - Composition, restriction and relabelling -
Extending the Algebra of STs - A sinple ~le: binary semaphores -
The ST Expansion Theorem.
A case study in synchronizaticn and proof te~iques
A scheduling problem - Building the scheduler as a Petri Net -
Observation equivalence - Proving the scheduler.
4. Case studies in value-cc~6~1~dnication
5.
6.
7.
Review - Passing values - An exanple:
An example: Zero searching.
Data Flow - Derivations -
Syntax and Semantics of CCS
Introduction - Syntax - Semantics by derivations - Defining behaviour
identifiers - Sorts and programs - Direct equivalence of behaviour
programs - Congruence of behaviour programs - Congruence of behaviour
expressions and the Expansion ~neorem.
Cu,,~!~cation Trees (CTs) as a model of CCS
CTs and the dynamic operaticns- C'fs and the static operations -
CTs defined by recursion - A~c actions and derivations of CTs -
Strong equivalence of CTs - Equality in the CT model - S~.
Cb~ticn ~_iivalence and its properties
Review - Observation equi%ralence in CCS - Observation oongruence -
Laws of observation congruence - Proof ted%niques - Proof of Theor~n
7.7 - Further exercises.
19
33
47
65
84
98
8.
9.
i0.
II.
VJ
Some proofs about Data Structures
Introduction - Registers and mamories - Chaining operations -
Pushdc~s and queues.
Translaticn into CCS
Discussion - The language P - Sorts and auxiliary definiticns -
Translation of P - Adding pzocedures to P - Protection of resources.
~tezminacy and Confluence
Discussion - Strong confluence - ~ite guards and the use of
ccnfluence - Strcng determinacy: Confluent detezminate CCS -
Proof in DCCS: the scheduler again - abservaticn confluence and
detezminacy.
Conclusion
What has been achieved? - Is OCS a programming language? -
The question of fairness - The notion of behaviour - Directions
for further work.
~: Properties of cc~gruence and equivalence.
111
126
138
158
166
References 16 9
剩余175页未读,继续阅读
资源评论
jiangdmdr
- 粉丝: 57
- 资源: 774
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功