Algebraic Theory for True Concurrency presents readers with the algebraic laws for true concurrency. Parallelism and concurrency are two of the core concepts within computer science. This book covers the different realms of concurrency, which enables programs, algorithms or problems to be broken out into order-independent or partially ordered components to improve computation and execution speed. There are two primary approaches for executing concurrency: interleaving concurrency and true concurrency. The main representative of interleaving concurrency is bisimulation/rooted branching bisimulation equivalences which is also readily explored.
This work eventually founded the comprehensive axiomatization modulo bisimulation equivalence -- ACP (Algebra of Communicating Processes).The other approach to concurrency is true concurrency. Research on true concurrency is active and includes many emerging applications. First, there are several truly concurrent bisimulation equivalences, including: pomset bisimulation equivalence, step bisimulation equivalence, history-preserving (hp-) bisimulation equivalence, and hereditary history-preserving (hhp-) bisimulation equivalence, the most well-known truly concurrent bisimulation equivalence.
Author(s): Yong Wang
Publisher: Academic Press
Year: 2023
Language: English
Pages: 227
City: London
Front Cover
Algebraic Theory for True Concurrency
Copyright
Contents
1 Introduction
2 Backgrounds
2.1 Process algebra
2.1.1 CCS
2.1.2 ACP
2.1.3 π-calculus
2.1.4 Guards
2.2 Operational semantics
2.3 Proof techniques
2.4 True concurrency
2.4.1 Event structure
2.4.2 Concurrent behavioral equivalences
3 A calculus for true concurrency
3.1 Syntax and operational semantics
3.1.1 Syntax
3.1.2 Operational semantics
3.1.3 Properties of transitions
3.2 Strongly truly concurrent bisimulations
3.2.1 Laws and congruence
3.2.2 Recursion
3.3 Weakly truly concurrent bisimulations
3.3.1 Laws and congruence
3.3.2 Recursion
3.4 Applications
3.5 Conclusions
4 Algebraic laws for true concurrency
4.1 Basic algebra for true concurrency
4.1.1 Axiom system of BATC
4.1.2 Properties of BATC
4.1.3 Structured operational semantics of BATC
4.2 Algebra for parallelism in true concurrency
4.2.1 Parallelism as a fundamental computational pattern
4.2.2 Axiom system of parallelism
4.2.3 Properties of parallelism
4.2.4 Structured operational semantics of parallelism
4.2.5 Encapsulation
4.3 Recursion
4.3.1 Guarded recursive specifications
4.3.2 Recursive definition and specification principles
4.3.3 Approximation induction principle
4.4 Abstraction
4.4.1 Rooted branching truly concurrent bisimulation equivalences
4.4.2 Guarded linear recursion
4.4.3 Algebraic laws for the silent step
4.4.4 Abstraction
4.5 Applications
4.6 Extensions
4.6.1 Placeholder
4.6.2 Renaming
4.6.3 States
4.7 Axiomatization for hhp-bisimilarity
4.7.1 APTC with left parallel composition
4.7.2 Recursion
4.7.3 Abstraction
4.8 Conclusions
5 Mobility
5.1 Syntax and operational semantics
5.1.1 Syntax
5.1.2 Operational semantics
5.1.3 Properties of transitions
5.2 Strongly truly concurrent bisimilarities
5.2.1 Basic definitions
5.2.2 Laws and congruence
5.2.3 Recursion
5.3 Algebraic theory
5.4 Conclusions
6 Guards
6.1 Operational semantics
6.2 BATC with guards
6.3 APTC with guards
6.4 Recursion
6.5 Abstraction
6.6 Hoare logic for APTCG
6.7 Conclusions
References
Index
Back Cover
