Communication and concurrency are essential in understanding complex dynamic systems, and there have been many theories to deal with them such as Petri nets, CSP and ACP. Among them, CCS (process calculus is one of the most important and mathematically developed models of communication and concurrency. Various behavior equivalences between agents, such as (strong and weak) bisimilarity, observation congruence, trace equivalence, testing equivalence and failure equivalence, are central notions in process calculus. In the real applications of process calculus, specification and implementation are described as two agents, correctness of programs is treated as a certain behavior equivalence between specification and implementation, and then the proof of correctness of programs is a task to establish some behavior equivalence between them. The goal of this book is to provide some suitable and useful concepts and tools for the understanding and analysis of approximate correctness of programs in concurrent systems. Throughout this book the focus is on the framework of process calculus, and the main idea is to construct some natural and reasonable topological structures which can reveal suitably a mechanism of approximate computation in process calculus and to work out various relationships among processes which are compatible with these topological structures.
Les mer
Intends 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 suitable for professionals, researchers and graduate students in theoretical computer science and formal methods.
Les mer
1 Introduction.- 2 Process Calculus.- 2.1 Transition Systems.- 2.2 Hennessy-Mi lner Logic.- 2.3 Basic Language.- 2.4 Transitional Semantics.- 2.5 Strong Bisimulations.- 2.6 Bisimulations.- 3 Bisimulation and Trace Limits of Agents 37.- 3.1 Strong Bisimulat ion Limits.- 3.2 *-Strong Bisi mulation Limits.- 3.3 Bisimulati on Limits.- 3.4 Trace Limits.- 4 Limit Behavior of Agents.- 4.1 Modifications of Topologies on Actions.- 4.2 Topologies on Agents.- 4.3 Several Limit Theorems.- 5 Near Bisimulations Defined by Closures.- 5.1 Near Bisimulations in Transition Systems.- 5.2 Near Strong Bisimulations.- 5.3 Near (Weak) Bisimulations.- 6 Bisimulation Indexes Induced by Metrics on Actions.- 6.1 Bisimulation Indexes in Transition Systems.- 6.2 Hennessy-Milner Logical Characterization of Bisimulation Indexes.- 6.3 Strong Bisimulation Indexes.- 6.4 (Weak) Bisimulation Indexes.- 6.5 Approximate Communication.- 6.6 Some Applications: Two Examples in Timed CCS.- 6.7 Some Appli cations: An Example in Real Time ACP.- 7 Conclusion.- References.
Les mer
Springer Book Archives
GPSR Compliance
The European Union's (EU) General Product Safety Regulation (GPSR) is a set of rules that requires consumer products to be safe and our obligations to ensure this.
If you have any concerns about our products you can contact us on ProductSafety@springernature.com.
In case Publisher is established outside the EU, the EU authorized representative is:
Springer Nature Customer Service Center GmbH
Europaplatz 3
69115 Heidelberg, Germany
ProductSafety@springernature.com
Les mer
Produktdetaljer
ISBN
9780387950921
Publisert
2001-03-30
Utgiver
Vendor
Springer-Verlag New York Inc.
Høyde
235 mm
Bredde
155 mm
Aldersnivå
Research, UU, UP, P, 05, 06
Språk
Product language
Engelsk
Format
Product format
Innbundet
Forfatter