Algebraic Theory for True Concurrency

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. Introduces algebraic properties and laws for true concurrency, one of the foundational concepts of computer science Presents all aspects of algebraic true concurrency, including the basis of semantics, calculi for true concurrency and for axiomatization Integrates all aspects of algebraic theory for true concurrency, along with extensions and applications Algebraic Theory for True Concurrency, First edition (2023) 228pp. 978-0-443-18912-8 Front Cover 1 Algebraic Theory for True Concurrency 4 Copyright 5 Contents 8 1 Introduction 10 2 Backgrounds 16 2.1 Process algebra 16 2.1.1 CCS 16 2.1.2 ACP 16 2.1.3 π-calculus 17 2.1.4 Guards 18 2.2 Operational semantics 18 2.3 Proof techniques 19 2.4 True concurrency 20 2.4.1 Event structure 20 2.4.2 Concurrent behavioral equivalences 21 3 A calculus for true concurrency 24 3.1 Syntax and operational semantics 24 3.1.1 Syntax 24 3.1.2 Operational semantics 25 3.1.3 Properties of transitions 25 3.2 Strongly truly concurrent bisimulations 27 3.2.1 Laws and congruence 27 3.2.2 Recursion 45 3.3 Weakly truly concurrent bisimulations 47 3.3.1 Laws and congruence 49 3.3.2 Recursion 52 3.4 Applications 54 3.5 Conclusions 56 4 Algebraic laws for true concurrency 58 4.1 Basic algebra for true concurrency 58 4.1.1 Axiom system of BATC 58 4.1.2 Properties of BATC 58 4.1.3 Structured operational semantics of BATC 60 4.2 Algebra for parallelism in true concurrency 79 4.2.1 Parallelism as a fundamental computational pattern 79 4.2.2 Axiom system of parallelism 81 4.2.3 Properties of parallelism 86 4.2.4 Structured operational semantics of parallelism 88 4.2.5 Encapsulation 104 4.3 Recursion 110 4.3.1 Guarded recursive specifications 110 4.3.2 Recursive definition and specification principles 112 4.3.3 Approximation induction principle 115 4.4 Abstraction 122 4.4.1 Rooted branching truly concurrent bisimulation equivalences 123 4.4.2 Guarded linear recursion 125 4.4.3 Algebraic laws for the silent step 126 4.4.4 Abstraction 130 4.5 Applications 139 4.6 Extensions 142 4.6.1 Placeholder 143 4.6.2 Renaming 148 4.6.3 States 153 4.7 Axiomatization for hhp-bisimilarity 160 4.7.1 APTC with left parallel composition 160 4.7.2 Recursion 163 4.7.3 Abstraction 165 4.8 Conclusions 167 5 Mobility 168 5.1 Syntax and operational semantics 168 5.1.1 Syntax 168 5.1.2 Operational semantics 170 5.1.3 Properties of transitions 170 5.2 Strongly truly concurrent bisimilarities 172 5.2.1 Basic definitions 172 5.2.2 Laws and congruence 174 5.2.3 Recursion 185 5.3 Algebraic theory 186 5.4 Conclusions 188 6 Guards 190 6.1 Operational semantics 190 6.2 BATC with guards 192 6.3 APTC with guards 197 6.4 Recursion 207 6.5 Abstraction 210 6.6 Hoare logic for APTCG 218 6.7 Conclusions 221 References 222 Index 224 Back Cover 230