Algebraic Theory for True Concurrency
By Yong Wang
()
About this ebook
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
Yong Wang
Dr. Yong Wang is an Associate Professor of Computer Science and Technology, Faculty of Information, at Beijing University of Technology. He holds a PhD in Computer Science from Beihang University, China. He has more than 20 years of research and teaching experience in parallel and distributed computing. Dr. Wang’s research interests include Theory of Parallel Computing, including algebraic theory for true concurrency and its extensions and applications, algebraic theory for reversible computing, and quantum process algebra and its application in quantum communication protocol. Dr. Wang’s other research interests include SOA, grid computing, cloud computing, and big data. Dr. Wang has published more than 120 research papers in leading Computer Science journals, including Wiley-Blackwell International Journal of Communication Systems, Springer International Journal of Theoretical Physics, and IEEE Transactions on Network and Service Management.
Related to Algebraic Theory for True Concurrency
Related ebooks
A Relaxation-Based Approach to Optimal Control of Hybrid and Switched Systems: A Practical Guide for Engineers Rating: 0 out of 5 stars0 ratingsComputability Theory: An Introduction to Recursion Theory Rating: 0 out of 5 stars0 ratingsGeometric Optimal Control: Theory, Methods and Examples Rating: 0 out of 5 stars0 ratingsModern Anti-windup Synthesis: Control Augmentation for Actuator Saturation Rating: 5 out of 5 stars5/5Intelligent Coordinated Control of Complex Uncertain Systems for Power Distribution and Network Reliability Rating: 0 out of 5 stars0 ratingsHybrid Dynamical Systems: Modeling, Stability, and Robustness Rating: 0 out of 5 stars0 ratingsTheory and Computation of Tensors: Multi-Dimensional Arrays Rating: 0 out of 5 stars0 ratingsUncertainty Quantification and Stochastic Modeling with Matlab Rating: 0 out of 5 stars0 ratingsStability and Controls Analysis for Delay Systems Rating: 0 out of 5 stars0 ratingsLogical Modeling of Biological Systems Rating: 0 out of 5 stars0 ratingsEquilibrium Statistical Mechanics Rating: 4 out of 5 stars4/5From Dimension-Free Matrix Theory to Cross-Dimensional Dynamic Systems Rating: 0 out of 5 stars0 ratingsAnalysis and Synthesis of Singular Systems Rating: 0 out of 5 stars0 ratingsSystems Dependability Assessment: Modeling with Graphs and Finite State Automata Rating: 0 out of 5 stars0 ratingsFractional Evolution Equations and Inclusions: Analysis and Control Rating: 5 out of 5 stars5/5Introduction to Probability Models Rating: 0 out of 5 stars0 ratingsThe Partition Method for a Power Series Expansion: Theory and Applications Rating: 0 out of 5 stars0 ratingsThe Systems Thinker - Dynamic Systems: Make Better Decisions and Find Lasting Solutions Using Scientific Analysis. Rating: 0 out of 5 stars0 ratingsTheory of Linear Physical Systems: Theory of physical systems from the viewpoint of classical dynamics, including Fourier methods Rating: 0 out of 5 stars0 ratingsAnalysis and Control of Polynomial Dynamic Models with Biological Applications Rating: 0 out of 5 stars0 ratingsIntroduction to Stochastic Processes Rating: 4 out of 5 stars4/5Interpolation and Extrapolation Optimal Designs 2: Finite Dimensional General Models Rating: 0 out of 5 stars0 ratingsDynamics of Cyclic Machines Rating: 0 out of 5 stars0 ratingsComputational Methods for Nonlinear Dynamical Systems: Theory and Applications in Aerospace Engineering Rating: 0 out of 5 stars0 ratingsStochastic Analysis of Mixed Fractional Gaussian Processes Rating: 0 out of 5 stars0 ratingsStochastic Structural Dynamics: Application of Finite Element Methods Rating: 0 out of 5 stars0 ratingsGenetic Optimization Techniques for Sizing and Management of Modern Power Systems Rating: 0 out of 5 stars0 ratingsApproximation and Optimization of Discrete and Differential Inclusions Rating: 0 out of 5 stars0 ratingsA Generalized Framework of Linear Multivariable Control Rating: 1 out of 5 stars1/5Neural Network Modeling and Identification of Dynamical Systems Rating: 0 out of 5 stars0 ratings
Computers For You
Deep Search: How to Explore the Internet More Effectively Rating: 5 out of 5 stars5/5SQL QuickStart Guide: The Simplified Beginner's Guide to Managing, Analyzing, and Manipulating Data With SQL Rating: 4 out of 5 stars4/5Mastering ChatGPT: 21 Prompts Templates for Effortless Writing Rating: 5 out of 5 stars5/5How to Create Cpn Numbers the Right way: A Step by Step Guide to Creating cpn Numbers Legally Rating: 4 out of 5 stars4/5Network+ Study Guide & Practice Exams Rating: 4 out of 5 stars4/5Procreate for Beginners: Introduction to Procreate for Drawing and Illustrating on the iPad Rating: 0 out of 5 stars0 ratingsThe ChatGPT Millionaire Handbook: Make Money Online With the Power of AI Technology Rating: 0 out of 5 stars0 ratings101 Awesome Builds: Minecraft® Secrets from the World's Greatest Crafters Rating: 4 out of 5 stars4/5Creating Online Courses with ChatGPT | A Step-by-Step Guide with Prompt Templates Rating: 4 out of 5 stars4/5Ultimate Guide to Mastering Command Blocks!: Minecraft Keys to Unlocking Secret Commands Rating: 5 out of 5 stars5/5AP Computer Science Principles Premium, 2024: 6 Practice Tests + Comprehensive Review + Online Practice Rating: 0 out of 5 stars0 ratingsCompTIA Security+ Practice Questions Rating: 2 out of 5 stars2/5Grokking Algorithms: An illustrated guide for programmers and other curious people Rating: 4 out of 5 stars4/5Everybody Lies: Big Data, New Data, and What the Internet Can Tell Us About Who We Really Are Rating: 4 out of 5 stars4/5CompTIA IT Fundamentals (ITF+) Study Guide: Exam FC0-U61 Rating: 0 out of 5 stars0 ratingsChildhood Unplugged: Practical Advice to Get Kids Off Screens and Find Balance Rating: 0 out of 5 stars0 ratingsChatGPT Ultimate User Guide - How to Make Money Online Faster and More Precise Using AI Technology Rating: 0 out of 5 stars0 ratingsPractical Lock Picking: A Physical Penetration Tester's Training Guide Rating: 5 out of 5 stars5/5Elon Musk Rating: 4 out of 5 stars4/5Dark Aeon: Transhumanism and the War Against Humanity Rating: 5 out of 5 stars5/5The Professional Voiceover Handbook: Voiceover training, #1 Rating: 5 out of 5 stars5/5Master Builder Roblox: The Essential Guide Rating: 4 out of 5 stars4/5Hacking: Ultimate Beginner's Guide for Computer Hacking in 2018 and Beyond: Hacking in 2018, #1 Rating: 4 out of 5 stars4/5
Reviews for Algebraic Theory for True Concurrency
0 ratings0 reviews
Book preview
Algebraic Theory for True Concurrency - Yong Wang
1: Introduction
Abstract
Parallelism and concurrency are the core concepts within computer science. There are mainly two camps in capturing concurrency: the interleaving concurrency and the true concurrency. This chapter gives an introduction to the interleaving concurrency and the true concurrency, especially true concurrency.
Keywords
Parallelism; Concurrency; Interleaving; True concurrency; Algebraic theory; Process algebra
Parallelism and concurrency [7] are the core concepts within computer science. There are mainly two camps in capturing concurrency: the interleaving concurrency and the true concurrency.
The situation for interleaving concurrency is as Fig. 1.1 illustrated. In this situation, there are m concurrent processes (programs) with each process consists of a set of atomic actions and their execution logic (modeled by sequential composition, alternative composition, and recursion or iteration), and each two actions within two processes may communicate. And there are only single thread within single core, single processor and single computer. All the actions (including the new communication actions caused by two actions within two processes) of m concurrent processes are laid on the single thread to be executed. The equivalent execution logic of all actions is the main research contents of interleaving concurrency.
Figure 1.1 Interleaving concurrency.
The situation for true concurrency is as Fig. 1.2 illustrated. In this situation, there are also m concurrent processes with each process consists of a set of atomic actions and their execution logic (but modeled by causality and conflicts, these causality and conflicts may exist within two actions in the same process and between actions in two processes). All the m processes actually construct a graph by causality and conflict relations. And there are n threads within multi-cores, multi-processors or multi-computers. All the actions of m concurrent processes are laid on the n threads to be executed. The equivalent execution logic of all actions is the corresponding main research contents of true concurrency.
Figure 1.2 True concurrency.
The representative of interleaving concurrency is bisimulation/rooted branching bisimulation equivalences. CCS (Calculus of Communicating Systems) [3] is a calculus based on bisimulation semantics model. Hennessy and Milner (HM) logic for bisimulation equivalence is also designed. Later, algebraic laws to capture computational properties modulo bisimulation equivalence was introduced in [1], and eventually founded the comprehensive axiomatization modulo bisimulation equivalence – ACP (Algebra of Communicating Processes) [4].
The other camp of concurrency is true concurrency. The researches on true concurrency are still active. Firstly, there are several truly concurrent bisimulation equivalences, the representatives are: pomset bisimulation equivalence, step bisimulation equivalence, history-preserving (hp-) bisimulation equivalence, and especially hereditary history-preserving (hhp-) bisimulation equivalence [8,9], the well-known finest truly concurrent bisimulation equivalence. These truly concurrent bisimulations are studied in different structures [5–7]: Petri nets, event structures, domains, and also a uniform form called TSI (Transition System with Independence) [13]. There are also several logics based on different truly concurrent bisimulation equivalences, for example, SFL (Separation Fixpoint Logic) and TFL (Trace Fixpoint Logic) [13] are extensions on true concurrency of mu-calculi [10] on bisimulation equivalence, and also a logic with reverse modalities [11,12] based on the so-called reverse bisimulations with a reverse flavor. It must be pointed out that, a uniform logic for true concurrency [14,15] was represented, which used a logical framework to unify several truly concurrent bisimulation equivalences, including pomset bisimulation, step bisimulation, hp-bisimulation and hhp-bisimulation.
There are simple comparisons between HM logic for bisimulation equivalence and the uniform logic [14,15] for truly concurrent bisimulation equivalences, the algebraic calculus CCS, algebraic laws [1], ACP [4], π calculus [23,24], guards [21] for bisimulation equivalence, and those for truly concurrent bisimulation equivalences, are still void.
Yes, we try to find the algebraic theory for true concurrency following the way paved by CCS, ACP, π, guards for bisimulation equivalence. And finally, we establish a whole algebraic theory for true concurrency called CTC (Calculus for True Concurrency), (Algebra for Processes in True Concurrency), (π for True Concurrency), ( with Guards), respectively.
This book is organized as follows.
In Chapter 2, we introduce some preliminaries to make this book self-satisfied, including brief introduction to process algebra, preliminaries on structured operational semantics and proof techniques, and preliminaries on true concurrency.
In Chapter 3, we introduce CTC, which is a calculus of truly concurrent systems. It includes syntax and semantics:
1. Its syntax includes actions, process constant, and operators acting between actions, like Prefix, Summation, Composition, Restriction, Relabeling.
2. Its semantics is based on labeled transition systems, Prefix, Summation, Composition, Restriction, Relabeling have their transition rules. CTC has good semantic properties based on the truly concurrent bisimulations. These properties include monoid laws, static laws, new expansion law for strongly truly concurrent bisimulations, τ laws for weakly truly concurrent bisimulations, and full congruences for strongly and weakly truly concurrent bisimulations, and also unique solution for recursion.
In Chapter 4, we introduce , which captures several computational properties in the form of algebraic laws, and proves the soundness and completeness modulo truly concurrent bisimulation/rooted branching truly concurrent bisimulation equivalences. These computational properties are organized in a modular way by use of the concept of conservational extension, which include the following modules, note that, every is composed of constants and operators, the constants are the computational objects, while operators capture the computational properties.
1. (Basic Algebras for True Concurrency). has sequential composition ⋅ and alternative composition + to capture causality computation and conflict. The constants are ranged over , the set of atomic events. The algebraic laws on ⋅ and + are sound and complete modulo truly concurrent bisimulation equivalences, such as pomset bisimulation , step bisimulation , history-preserving (hp-) bisimulation and hereditary history-preserving (hhp-) bisimulation .
2. (Algebra for Parallelism in True Concurrency). uses the whole parallel operator ≬, the parallel operator ∥ to model parallelism, and the communication merge | to model causality (communication) among different parallel branches. Since a communication may be blocked, a new constant called deadlock δ is extended to , and also a new unary encapsulation operator is introduced to eliminate δ, which may exist in the processes. And also a conflict elimination operator Θ to eliminate conflicts existing in different parallel branches. The algebraic laws on these operators are also sound and complete modulo truly concurrent bisimulation equivalences, such as pomset bisimulation , step bisimulation , history-preserving (hp-) bisimulation . Note that, these operators in a process except the parallel operator ∥ can be eliminated by deductions on the process using axioms of , and eventually be steadied by ⋅, + and ∥, this is also why bisimulations are called a truly concurrent semantics.
3. Recursion. To model infinite computation, recursion is introduced into . In order to obtain a sound and complete theory, guarded recursion and linear recursion are needed. The corresponding axioms are RSP (Recursive Specification Principle) and RDP (Recursive Definition Principle), RDP says the solutions of a recursive specification can represent the behaviors of the specification, while RSP says that a guarded recursive specification has only one solution, they are sound with respect to with guarded recursion modulo truly concurrent bisimulation equivalences, such as pomset bisimulation , step bisimulation , history-preserving (hp-) bisimulation , and they are complete with respect to with linear recursion modulo truly concurrent bisimulation equivalence, such as pomset bisimulation , step bisimulation , history-preserving (hp-) bisimulation .
4. Abstraction. To abstract away internal implementations from the external behaviors, a new constant τ called silent step is added to , and also a new unary abstraction operator is used to rename actions in I into τ (the resulted with silent step and abstraction operator is called ). The recursive specification is adapted to guarded linear recursion to prevent infinite τ-loops specifically. The axioms for τ and are sound modulo rooted branching truly concurrent bisimulation equivalences (a kind of weak truly concurrent bisimulation equivalence), such as rooted branching pomset bisimulation , rooted branching step bisimulation , rooted branching history-preserving (hp-) bisimulation . To eliminate infinite τ-loops caused by and obtain the completeness, (Cluster Fair Abstraction Rule) is used to prevent infinite τ-loops in a constructible way.
In Chapter 5, we introduce , which is an extension of CTC and a generalization of π calculus.
1. It treats names, variables and substitutions more carefully, since names may be free or bound.
2. Names are mobile by references, rather than by values.
3. There are three kinds of prefixes, τ prefix , output prefix and input prefix , which are most distinctive to CTC.
4. has good semantic properties based on the truly concurrent bisimulations. These properties include summation laws, identity laws, restriction laws, parallel laws, new expansion law for strongly truly concurrent bisimulations, and full congruences for truly concurrent bisimulations, and also unique solution for recursion.
In Chapter 6, to support data manipulation, we introduce , which is an extension of with guards.
1. It has a sound and complete theory of concurrency and parallelism with guards.
2. It has a sound and complete theory of recursion including concurrency with guards.
3. It has a sound and complete theory of abstraction with guards.
4. It has a sound Hoare logic [20] including concurrency and parallelism, recursion, and abstraction.
References
[1] M. Hennessy, R. Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM 1985;32:137–161.
[3] R. Milner, A Calculus of Communicating Systems. Lecture Notes in Computer Science. Springer; 1980;vol. 92.
[4] W. Fokkink, Introduction to Process Algebra. 2nd ed. Springer-Verlag; 2007.
[5] M. Nielsen, G.D. Plotkin, G. Winskel, Petri nets, event structures and domains, Part I, Theoretical Computer Science 1981;13:85–108.
[6] G. Winskel, Event structures, Wilfried Brauer, Wolfgang Reisig, Grzegorz Rozenberg, eds. Petri Nets: Applications and Relationships to Other Models of Concurrency. Lecture Notes in Computer Science. Berlin: Springer; 1987;vol. 255:325–392.
[7] G. Winskel, M. Nielsen, Models for concurrency, Samson Abramsky, Dov M. Gabbay, Thomas S.E. Maibaum, eds. Handbook of logic in Computer Science, vol. 4. Oxford, UK: Clarendon Press; 1995.
[8] M.A. Bednarczyk, Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. [Tech. Rep. Polish Academy of Sciences] 1991.
[9] S.B. Fröschle, T.T. Hildebrandt, On plain and hereditary history-preserving bisimulation, Miroslaw Kutylowski, Leszek Pacholski, Tomasz Wierzbicki, eds. Proceedings of MFCS'99. Lecture Notes in Computer Science. Berlin: Springer; 1999;vol. 1672:354–365.
[10] J. Bradfield, C. Stirling, Modal mu-calculi, Patrick Blackburn, Johan van Benthem, Franck Wolter, eds. Handbook of Modal Logic. Amsterdam, the Netherlands: Elsevier; 2006:721–756.
[11] I. Phillips, I. Ulidowski, Reverse bisimulations on stable configuration structures, B. Klin, P. Sobociǹski, eds. Proceedings of SOS'09. Electronic Proceedings in Theoretical Computer Science. Amsterdam, the Netherlands: Elsevier; 2010;vol. 18:62–76.
[12] I. Phillips, I. Ulidowski, A logic with reverse modalities for history-preserving bisimulations, Bas Luttik, Frank Valencia, eds. Proceedings of EXPRESS'11. Electronic Proceedings in Theoretical Computer Science. Amsterdam, the Netherlands: Elsevier; 2011;vol. 64:104–118.
[13] J. Gutierrez, On bisimulation and model-checking for concurrent systems with partial order semantics. [Ph.D. dissertation] LFCS – University of Edinburgh; 2011.
[14] P. Baldan, S. Crafa, A logic for true concurrency, Paul Gastin, François Laroussinie, eds. Proceedings of CONCUR'10. Lecture Notes in Computer Science. Berlin: Springer; 2010;vol. 6269:147–161.
[15] P. Baldan, S. Crafa, A logic for true concurrency, Journal of the ACM 2014;61(4) 36 pages.
[20] C.A.R. Hoare, An axiomatic basis for computer programming, Communications of the ACM October 1969;12(10).
[21] J.F. Groote, A. Ponse, Process algebra with guards: combining hoare logic with process algebra, Formal Aspects of Computing 1994;6(2):115–164.
[23] R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, Part I, Information and Computation 1992;100(1):1–40.
[24] R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, Part II, Information and Computation 1992;100(1):41–77.
2: Backgrounds
Abstract
To make this book self-satisfied, we introduce some preliminaries in this chapter, including some introductions on process algebra and true concurrency.
Keywords
Process algebra; Operational semantics; Proof techniques; True concurrency; Behavioral equivalences
To make this book self-satisfied, we introduce some preliminaries in this chapter, including some introductions on process algebra and true concurrency.
2.1 Process algebra
In this subsection, we introduce the preliminaries on process algebra CCS, ACP, mobility, guards which are based on the interleaving bisimulation semantics.
2.1.1 CCS
A crucial initial observation that is at the heart of the notion of process algebra is due to Milner, who noticed that concurrent processes have an algebraic structure. CCS [2,3] is a calculus of concurrent systems. It includes syntax and semantics:
1. Its syntax includes actions, process constant, and operators acting between actions, like Prefix, Summation, Composition, Restriction, Relabeling.
2. Its semantics is based on labeled transition systems, Prefix, Summation, Composition, Restriction, Relabeling have their transition rules. CCS has good semantic properties based on the interleaving bisimulation. These properties include monoid laws, static laws, expansion law for strongly interleaving bisimulation, τ laws for weakly interleaving bisimulation, and full congruences for strongly and weakly interleaving bisimulations, and also unique solution for recursion.
CCS can be used widely in verification of computer systems with an interleaving concurrent flavor.
2.1.2 ACP
ACP captures several computational properties in the form of algebraic laws, and proves the soundness and completeness modulo bisimulation/rooted branching bisimulation equivalences. These computational properties are organized in a modular way by use of the concept of conservational extension, which include the following modules, note that, every algebra is composed of constants and operators, the constants are the computational objects, while operators capture the computational properties.
1. BPA(Basic Process Algebras). BPA has sequential composition ⋅ and alternative composition + to capture sequential computation and nondeterminacy. The constants are ranged over A, the set of atomic actions. The algebraic laws on ⋅ and + are sound and complete modulo bisimulation equivalence.
2. ACP(Algebra of Communicating Processes). ACP uses the parallel operator ∥, the auxiliary binary left merge to model parallelism, and the communication merge | to model communications among different parallel branches. Since a communication may be blocked, a new constant called deadlock δ is extended to A, and also a new unary encapsulation operator is introduced to eliminate δ, which may exist in the processes. The algebraic laws on these operators are also sound and complete modulo bisimulation equivalence. Note that, these operators in a process can be eliminated by deductions on the process using axioms of ACP, and eventually be steadied by ⋅ and +, this is also why bisimulation is called an interleaving semantics.
3. Recursion. To model infinite computation, recursion is introduced into ACP. In order to obtain a sound and complete theory, guarded recursion and linear recursion are needed. The corresponding axioms are RSP (Recursive Specification Principle) and RDP (Recursive Definition Principle), RDP says the solutions of a recursive specification can represent the behaviors of the specification, while RSP says that a guarded recursive specification has only one solution, they are sound with respect to ACP with guarded recursion modulo bisimulation equivalence, and they are complete with respect to ACP with linear recursion modulo bisimulation