Topology in Process Calculus

by Ying, Mingsheng

• ISBN13: 9780387950921
• ISBN10: 0387950923
• Format: Hardcover
• Copyright: 2001-04-01
• Publisher: Springer Verlag

Summary

Process calculi are among the most successful models of concurrent systems. Various behavior equivalences between processes are central notions in CCS (calculus of communicating systems) and other process calculi. In the real applications, specification and implementation are described as two processes, and correctness of programs is treated as a certain behavior equivalence between them.The purpose of this book is to establish a theory of approximate correctness and infinite evolution of concurrent programs by employing some notions and tools from point-set topology. This book is restricted to CCS for simplicity, but the main idea also applies to some other process calculi. The concept of bisimulation limits, useful for the understanding and analysis of infinite evolution of processes, is introduced. In addition, the notions of near bisimulations and bisimulation indexes, suitable in describing approximate correctness of concurrent programs, are proposed.The book will be of particular interest to researchers in the fields of theoretical computer science, especially theory of concurrency and hybrid systems, and graduate students in related disciplines. It will also be valuable to practical system designers developing concurrent and/or real-time systems.

Table of Contents

Preface	v
Introduction	1	(10)
Process Calculus	11	(26)
Transition Systems	11	(4)
Hennessy-Milner Logic	15	(4)
Basic Language	19	(2)
Transitional Semantics	21	(3)
Strong Bisimulations	24	(5)
Bisimulations	29	(8)
Bisimulation and Trace Limits of Agents	37	(58)
Strong Bisimulation Limits	37	(32)
Strong Limit Bisimulations	38	(8)
Strong Bisimulation Limits	46	(7)
Strong Bisimulation Topology	53	(5)
Strong Limit Bisimulations Up to ~	58	(2)
Continuity of Combinators	60	(6)
Limit Representations of Solutions of Equations	66	(2)
Determinacy Preserved by Strong Bisimulation Limits	68	(1)
*-Strong Bisimulation Limits	69	(9)
Bisimulation Limits	78	(8)
Trace Limits	86	(9)
Limit Behavior of Agents	95	(18)
Modifications of Topologies on Actions	96	(4)
Topologies on Agents	100	(2)
Several Limit Theorems	102	(11)
Near Bisimulations Defined by Closures	113	(26)
Near Bisimulations in Transition Systems	113	(12)
Near Strong Bisimulations	125	(6)
Near (Weak) Bisimulations	131	(8)
Bisimulation Indexes Induced by Metrics on Actions	139	(68)
Bisimulation Indexes in Transition Systems	140	(14)
Hennessy-Milner Logical Characterization of Bisimulation Indexes	154	(4)
Strong Bisimulation Indexes	158	(11)
(Weak) Bisimulation Indexes	169	(8)
Approximate Communication	177	(5)
Some Applications: Two Examples in Timed CCS	182	(16)
Some Applications: An Example in Real Time ACP	198	(9)
Conclusion	207	(6)
References	213	(6)
Index	219