機率進程語義（英文版）

《機率進程語義（英文版）》是2015年上海交通大學出版社出版的圖書，作者是鄧玉欣。

基本介紹

• 中文名：機率進程語義（英文版）
• 作者：鄧玉欣
• 出版社：上海交通大學出版社
• 出版時間：2015年11月1日
• ISBN：9787313138217

內容簡介

隨著計算機網路和通信技術的發展，對並發分散式系統的研究變得越來越重要。作為一種描述並發計算的模型，進程演算受到廣泛研究並被成功套用到實際系統的規範、設計、分析及驗證中。近些年來，人們提出機率進程演算用來描述和分析並發系統的量化行為，這要求對機率進程的語義基礎進行深入研究。

　　《機率進程語義（英文版）》中，以操作語義的方式把進程行為表示成機率標號遷移系統。不同遷移系統通過一些適當的行為等價或前序關係進行比較。

圖書目錄

1 Introduction

1．1 Background

1．2 Synopsis

References

2 Mathematical Preliminaries

2．1 Lattice Theory

2．2 Induction and Coinduction

2．3 Topological Spaces

2．4 Metric Spaces

2．5 Probability Spaces

2．6 Linear Programming

References

3 Probabilistic Bisimulation

3．1 Introduction

3．2 Probabilistic Labelled Transition Systems

3．3 Lifting Relations

3．4 Justifving the Lifting Operation

3．4．1 Justification by the Kantorovich Memc

3．4．2 Justification by Network Flow

3．5 Probabilistic Bisimulation

3．6 Logical Characterisation

3．6．1 An Adequate Logic

3．6．2 An Expressive Logic

3．7 Metric Characterisation

3．8 Algorithmic Characterisation

3．8．1 A Partition Refinement Algorithm

3．8．2 An“On—the—Fly”Algorithm

3．9 Bibliographic Notes

3．9．1 Probabilistic Models

3．9．2 Probabilistic Bisimulation

References

4 Probabilistic Testine Semantics

4．1 A General Testing Framework

4．2 Testing Probabilistic Processes

4．3 Bounded Continuity

4．4 Reward Testing

4．4．1 A Geometric Property

4．4．2 Nonnegative Rewards

4．5 Extremal Reward Testing

4．6 Extremal Reward Testing Versus Resolution—Based Reward Testing

4．6．1 Must Testing

4．6．2 May Testing

4．7 Vector—Based Testing Versus Scalar Testin~

4．8 Bibliographic Notes

References

5 Testing Finite Probabilistic Processes

5．1 Introduction

5．2 The Language pCSP

5．2．1 The Syntax

5．2．2 The Operational Semantics

5．2．3 The Precedence of Probabilistic Choice

5．2．4 Graphical representation of pCSP processes

5．2．5 Testing pCSP Processes

5．3 Counterexamples

5．4 Must Versus May Testing

5．5 Forward and Failure Simulation

5．5．1 The Simulation Preorders

5．5．2 The Simulation Preorders are Precongruences

5．5．3 Simulations Are Sound for Testing Preorders

5．6 A Modal Logic

5．7 Characteristic Tests

5．8 Equational Theories

5．9 Inequational Theories

5．10 Comoletenes

5．11 Bibliographic Notes

5．11．1 Probabilistic Equivalences

5．11．2 Probabilistic Simulations

References

6 Testing Finitary Probabilistic Processes

6．1 IntrOduction

6．2 The Language rpCSP

6．3 A General Definition of Weak Derivations

6．3．1 Lifting Relations

6．3．2 Weak Transitions

6．3．3 Properties of Weak Transitions

6．4 Testing rpCSP Processes

6．4．1 Testing with Extremal Derivatives

6．4．2 Comparison with Resolution—Based Testing

6．5 Generatinz Weak Derivatives in a Finitary pLTS

6．5．1 Finite Generability

6．5．2 Realising Payoffs

6．5．3 Conseauences

6．6 The Failure Simulation Preorder

6．6．1 Two Equivalent Definitions and Their Rationale

6．6．2 A Simple Failure Similarity for Finitary Processes

6．6．3 Precongruence

6．6．4 Soundness

6．7 Failure Simulation is Complete for Must Testing

6．7．1 Inductive Characterisatior

6．7．2 The Modal Logic

6．7．3 Characteristic Tests for Formulae

6．8 Simulations and May Testing

6．8．1 Soundness

6．8．2 Completeness

6．9 Real—Reward Testing

6．10 Summary

References

7 Weak Probabilistic Bisimulation

7．1 Introduction

7．2 A Simple Bisimulation

7．3 Compositionality

7．4 Reduction Barbed Congruence

7．5 Bibliographic Notes

References

Index