Handbook of Truly Concurrent Process Algebra provides readers with a detailed and in-depth explanation of the algebra used for concurrent computing. This complete handbook is divided into five Parts: Algebraic Theory for Reversible Computing, Probabilistic Process Algebra for True Concurrency, Actors – A Process Algebra-Based Approach, Secure Process Algebra, and Verification of Patterns. The author demonstrates actor models which are captured using the following characteristics: Concurrency, Asynchrony, Uniqueness, Concentration, Communication Dependency, Abstraction, and Persistence.
Truly concurrent process algebras are generalizations of the corresponding traditional process algebras. Handbook of Truly Concurrent Process Algebra introduces several advanced extensions and applications of truly concurrent process algebras. Part 1: Algebraic Theory for Reversible Computing provides readers with all aspects of algebraic theory for reversible computing, including the basis of semantics, calculi for reversible computing, and axiomatization for reversible computing. Part 2: Probabilistic Process Algebra for True Concurrency provides readers with all aspects of probabilistic process algebra for true concurrency, including the basis of semantics, calculi for probabilistic computing, axiomatization for probabilistic computing, as well as mobile calculi for probabilistic computing. Part 3: Actors - A Process Algebra-Based Approach bridges the two concurrent models, process algebra and actors, by capturing the actor model in the following characteristics: Concurrency, Asynchrony, Uniqueness, Concentration, Communication Dependency, Abstraction, and Persistence. Part 4: Secure Process Algebra demonstrates the advantages of process algebra in verifying security protocols – it has a firmly theoretic foundation and rich expressive powers to describe security protocols. Part 5: Verification of Patterns formalizes software patterns according to the categories of the patterns and verifies the correctness of patterns based on truly concurrent process algebra. Every pattern is detailed according to a regular format to be understood and utilized easily, which includes introduction to a pattern and its verifications. Patterns of the vertical domains are also provided, including the domains of networked objects and resource management. To help readers develop and implement the software patterns scientifically, the pattern languages are also presented.
1. Chapter 1. Introduction to algebraic theory for reversible computing - p. 1 2. Chapter 2. Backgrounds - p. 5 3. Abstract - p. 5 4. 2.1 Operational semantics - p. page5 5. 2.2 Proof techniques - p. page5 6. 2.3 CTC - p. page5 7. 2.4 πtcπtc - p. page6 8. 2.5 APTC - p. page6 9. 2.6 Forward–reverse truly concurrent bisimulations - p. 19 10. References - p. 23 11. Chapter 3. Reversible calculus - p. 25 12. Abstract - p. 25 13. 3.1 Syntax and operational semantics - p. page25 14. 3.2 Strongly forward–reverse truly concurrent bisimulations - p. 29 15. 3.3 Weakly forward–reverse truly concurrent bisimulations - p. 54 16. Chapter 4. Algebraic laws for reversible computing - p. 59 17. Chapter 5. Partially reversible calculus - p. 121 18. Chapter 6. Algebraic laws for partially reversible computing - p. 157 19. Partially reversible πtcπtc - p. 189 20. Chapter 8. Introduction to probabilistic process algebra for true concurrency - p. 206 21. Chapter 9. Backgrounds - p. 209 22. Chapter 10. A calculus for probabilistic true concurrency - p. 225 23. Chapter 11. Algebraic laws for probabilistic true concurrency - p. 239 24. Chapter 12. Mobility - p. 267 25. Chapter 13. Guards - p. 279 26. Chapter 14. CTC with probability and guards - p. 303 27. πtcπtc with probability and guards - p. 333 28. Chapter 16. Introduction to actors - p. 351 29. Chapter 17. Truly concurrent process algebra - p. 353 30. Chapter 18. Process algebra based actor model - p. 359 31. Chapter 19. Process algebra based actor model of Map–Reduce - p. 361 32. Chapter 20. Process algebra based actor model of the Google File System - p. 367 33. Chapter 21. Process algebra based actor model of cloud resource management - p. 371 34. Chapter 22. Process algebra based actor model of the Web Service composition - p. 377 35. Chapter 23. Process algebra based actor model of the QoS-aware Web Service orchestration engine - p. 401 36. Chapter 24. Introduction to secure process algebra - p. 418 37. Chapter 25. Secure APTC - p. 421 38. Chapter 26. Analyses of key exchange protocols - p. 429 39. Chapter 27. Analyses of authentication protocols - p. 441 40. Chapter 28. Analyses of practical protocols - p. 447 41. Chapter 29. Analyses of other protocols - p. 473 42. Chapter 30. Analyses of digital cash protocols - p. 481 43. Chapter 31. Analyses of secure elections protocols - p. 491 44. Chapter 32. Introduction to verification of patterns - p. 512 45. Chapter 33. Verification of architectural patterns - p. 517 46. Chapter 34. Verification of design patterns - p. 547 47. Chapter 35. Verification of idioms - p. 563 48. Chapter 36. Verification of patterns for concurrent and networked objects - p. 567 49. Chapter 37. Verification of patterns for resource management - p. 601 50. Chapter 38. Composition of patterns - p. 623 51. References - p. 629 52. Index - p. 631
Handbook of Truly Concurrent Process Algebra provides readers with a detailed and in-depth explanation of the algebra used for concurrent computing. This complete handbook is divided into five Parts: Algebraic Theory for Reversible Computing, Probabilistic Process Algebra for True Concurrency, Actors – A Process Algebra-Based Approach, Secure Process Algebra, and Verification of Patterns. The author demonstrates actor models which are captured using the following characteristics: Concurrency, Asynchrony, Uniqueness, Concentration, Communication Dependency, Abstraction, and Persistence.
Truly concurrent process algebras are generalizations of the corresponding traditional process algebras. Handbook of Truly Concurrent Process Algebra introduces several advanced extensions and applications of truly concurrent process algebras. Part 1: Algebraic Theory for Reversible Computing provides readers with all aspects of algebraic theory for reversible computing, including the basis of semantics, calculi for reversible computing, and axiomatization for reversible computing. Part 2: Probabilistic Process Algebra for True Concurrency provides readers with all aspects of probabilistic process algebra for true concurrency, including the basis of semantics, calculi for probabilistic computing, axiomatization for probabilistic computing, as well as mobile calculi for probabilistic computing. Part 3: Actors - A Process Algebra-Based Approach bridges the two concurrent models, process algebra and actors, by capturing the actor model in the following characteristics: Concurrency, Asynchrony, Uniqueness, Concentration, Communication Dependency, Abstraction, and Persistence. Part 4: Secure Process Algebra demonstrates the advantages of process algebra in verifying security protocols – it has a firmly theoretic foundation and rich expressive powers to describe security protocols. Part 5: Verification of Patterns formalizes software patterns according to the categories of the patterns and verifies the correctness of patterns based on truly concurrent process algebra. Every pattern is detailed according to a regular format to be understood and utilized easily, which includes introduction to a pattern and its verifications. Patterns of the vertical domains are also provided, including the domains of networked objects and resource management. To help readers develop and implement the software patterns scientifically, the pattern languages are also presented.
1. Chapter 1. Introduction to algebraic theory for reversible computing - p. 1 2. Chapter 2. Backgrounds - p. 5 3. Abstract - p. 5 4. 2.1 Operational semantics - p. page5 5. 2.2 Proof techniques - p. page5 6. 2.3 CTC - p. page5 7. 2.4 πtcπtc - p. page6 8. 2.5 APTC - p. page6 9. 2.6 Forward–reverse truly concurrent bisimulations - p. 19 10. References - p. 23 11. Chapter 3. Reversible calculus - p. 25 12. Abstract - p. 25 13. 3.1 Syntax and operational semantics - p. page25 14. 3.2 Strongly forward–reverse truly concurrent bisimulations - p. 29 15. 3.3 Weakly forward–reverse truly concurrent bisimulations - p. 54 16. Chapter 4. Algebraic laws for reversible computing - p. 59 17. Chapter 5. Partially reversible calculus - p. 121 18. Chapter 6. Algebraic laws for partially reversible computing - p. 157 19. Partially reversible πtcπtc - p. 189 20. Chapter 8. Introduction to probabilistic process algebra for true concurrency - p. 206 21. Chapter 9. Backgrounds - p. 209 22. Chapter 10. A calculus for probabilistic true concurrency - p. 225 23. Chapter 11. Algebraic laws for probabilistic true concurrency - p. 239 24. Chapter 12. Mobility - p. 267 25. Chapter 13. Guards - p. 279 26. Chapter 14. CTC with probability and guards - p. 303 27. πtcπtc with probability and guards - p. 333 28. Chapter 16. Introduction to actors - p. 351 29. Chapter 17. Truly concurrent process algebra - p. 353 30. Chapter 18. Process algebra based actor model - p. 359 31. Chapter 19. Process algebra based actor model of Map–Reduce - p. 361 32. Chapter 20. Process algebra based actor model of the Google File System - p. 367 33. Chapter 21. Process algebra based actor model of cloud resource management - p. 371 34. Chapter 22. Process algebra based actor model of the Web Service composition - p. 377 35. Chapter 23. Process algebra based actor model of the QoS-aware Web Service orchestration engine - p. 401 36. Chapter 24. Introduction to secure process algebra - p. 418 37. Chapter 25. Secure APTC - p. 421 38. Chapter 26. Analyses of key exchange protocols - p. 429 39. Chapter 27. Analyses of authentication protocols - p. 441 40. Chapter 28. Analyses of practical protocols - p. 447 41. Chapter 29. Analyses of other protocols - p. 473 42. Chapter 30. Analyses of digital cash protocols - p. 481 43. Chapter 31. Analyses of secure elections protocols - p. 491 44. Chapter 32. Introduction to verification of patterns - p. 512 45. Chapter 33. Verification of architectural patterns - p. 517 46. Chapter 34. Verification of design patterns - p. 547 47. Chapter 35. Verification of idioms - p. 563 48. Chapter 36. Verification of patterns for concurrent and networked objects - p. 567 49. Chapter 37. Verification of patterns for resource management - p. 601 50. Chapter 38. Composition of patterns - p. 623 51. References - p. 629 52. Index - p. 631
