Chapter 1 Introduction ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 1
Chapter 2 Backgrounds ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 3
2．1 Operational Semantics ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 3
2．2 Proof Techniques ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．5
2．3 Truly Concurrent Process Algebra - APTC． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 5
2．3．1 Basic Algebra for True Concurrency ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 6
2．3．2 APTC with Left Parallel Composition ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 9
2．3．3 Recursion ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 13
2．3．4 Abstraction ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 15
2．3．5 Placeholder． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．19
2．3．6 Applications ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 21
2．4 Truly Concurrent Process Algebra with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 27
2．4．1 Operational Semantics with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 27
2．4．2 BATC with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 31
2．4．3 APTC with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 34
2．4．4 Recursion with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 39
2．4．5 Abstraction with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 41
Chapter 3 An Axiomatization of Discrete Event Processes． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．46
3．1 Basic Algebra for True Concurrency - BATC ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 46
3．1．1 Axiom System of BATC． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 46
3．1．2 Properties of BATC． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 46
3．1．3 Structured Operational Semantics of BATC ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 47
3．2 Algebra for Parallelism in True Concurrency ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 53
3．2．1 Parallelism as a Fundamental Computational Pattern ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 53
3．2．2 Axiom System of Parallelism ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．55
3．2．3 Properties of Parallelism． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．56
3．2．4 Structured Operational Semantics of Parallelism ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．58
3．2．5 Encapsulation ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 63
3．3 Recursion ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 67
3．3．1 Guarded Recursive Specifications ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．68
3．3．2 Recursive Definition and Specification Principles． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．69
3．3．3 Approximation Induction Principle ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 72
3．4 Silent Step and Abstraction ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 77
3．4．1 Guarded Linear Recursion ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 77
3．4．2 Algebraic Laws for the Silent Step ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．78
3．4．3 Abstraction ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 81
Chapter 4 An Axiomatization of Distributed Discrete Event Processes ． ． ． ． ． ． ． ． ． 87
4．1 BATC with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 87
4．1．1 Axiom System of BATC with Static Localities． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．87
4．1．2 Properties of BATC with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 88
4．1．3 Structured Operational Semantics of BATC with Static Localities． ． ． ． ． ． ．89
4．2 APTC with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 94
4．2．1 Properties of Parallelism with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 97
4．2．2 Structured Operational Semantics of Parallelism with
Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 100
4．2．3 Encapsulation with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 105
4．3 Recursion with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 109
4．3．1 Guarded Recursive Specifications with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 110
4．3．2 Recursive Definition and Specification Principles with
Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 112
4．3．3 Approximation Induction Principle with Static Localities． ． ． ． ． ． ． ． ． ． ． ． ． ．114
4．4 Silent Step and Abstraction with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 118
4．4．1 Guarded Linear Recursion with Static Localities． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．119
4．4．2 Algebraic Laws for the Silent Step with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． 120
4．4．3 Abstraction with Static Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 123
Chapter 5 Hybrid Process Algebra ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．128
5．1 Truly Concurrent Semantics． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．128
5．2 Hybrid BATC ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 132
5．2．1 Axiom System of Hybrid BATC． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．132
5．2．2 Properties of Hybrid BATC． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．134
5．2．3 Structured Operational Semantics of Hybrid BATC． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．136
5．3 Hybrid APTC ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 138
5．3．1 Properties of Parallelism of Hybrid APTC ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 141
5．3．2 Structured Operational Semantics of Parallelism of Hybrid APTC ． ． ． ． ． 144
5．3．3 Encapsulation of Hybrid APTC． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 145
5．4 Recursion of Hybrid APTC ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 148
5．4．1 Guarded Recursive Specifications ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 148
5．4．2 Recursive Definition and Specification Principles of Hybrid APTC ． ． ． ． ． 150
5．4．3 Approximation Induction Principle of Hybrid APTC． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．150
5．5 Silent Step and Abstraction of Hybrid APTC ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 152
5．5．1 Guarded Linear Recursion of Hybrid APTC． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．152
5．5．2 Algebraic Laws for the Silent Step of Hybrid APTC ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 153
5．5．3 Abstraction ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 154
5．6 Application of Hybrid APTC in Modelling Neural Networks ． ． ． ． ． ． ． ． ． ． ． ． 155
5．6．1 Modelling of Neurons ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 156
5．6．2 Modelling of Neural Networks． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．158
Chapter 6 Hybrid Process Algebra with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 161
6．1 Locality Semantics ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 161
6．2 Hybrid BATC with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 165
6．2．1 Axiom System of Hybrid BATC with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 165
6．2．2 Properties of Hybrid BATC With Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．166
6．2．3 Structured Operational Semantics of Hybrid BATC with Localities ． ． ． ． 168
6．3 Hybrid APTC with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 171
6．3．1 Properties of Parallelism of Hybrid APTC with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． 175
6．3．2 Structured Operational Semantics of Parallelism of Hybrid APTC
with Localities． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．178
6．3．3 Encapsulation of Hybrid APTC with Localities． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．179
6．4 Recursion of Hybrid APTC with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 182
6．4．1 Guarded Recursive Specifications of Hybrid APTC with Localities ． ． ． ． ． 183
6．4．2 Recursive Definition and Specification Principles of Hybrid APTC
with Localities． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ．184
6．4．3 Approximation Induction Principle of Hybrid APTC with Localities ． ． ． 185
6．5 Silent Step and Abstraction of Hybrid APTC with Localities ． ． ． ． ． ． ． ． ． ． ． 186
6．5．1 Guarded Linear Recursion of Hybrid APTC with Localities ． ． ． ． ． ． ． ． ． ． ． 187
6．5．2 Algebraic Laws for the Silent Step of Hybrid APTC with Localities ． ． ． ． 188
6．5．3 Abstraction of Hybrid APTC with Localities ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 189
6．6 Application of Hybrid APTC with Localities in Modelling
Distributed/Federated Neural Networks ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 190
6．6．1 Modelling of Distributed/Federated Neurons ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 190
6．6．2 Modelling of Distributed/Federated Neural Networks ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 192
Bibliography ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． ． 194
展开
