Algebraic Theory for True Concurrency

Concurrency is one of the foundational concepts of Computer Science, and 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. Concurrency 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. CCS (Calculus of Communicating Systems) is a calculus based on the bisimulation semantics model. Hennessy and Milner (HM) logic is also designed for bisimulation equivalence. Later, algebraic laws to capture computational properties modulo bisimulation equivalence were introduced. 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. These truly concurrent bisimulations are studied in different structures: Petri nets, event structures, domains, and also a uniform form called TSI (Transition System with Independence). There are also several logics based on different truly concurrent bisimulation equivalences, for example, SFL (Separation Fixpoint Logic) and TFL (Trace Fixpoint Logic). These are extensions on true concurrency of mu-calculi on bisimulation equivalence, and also a logic with reverse modalities based on the so-called reverse bisimulations with a reverse flavor. It must be pointed out that a uniform logic for true concurrency was represented several years ago, which used a logical framework to unify several truly concurrent bisimulation equivalences, including pomset bisimulation, step bisimulation, hp-bisimulation and hhp-bisimulation.Algebraic Theory for True Concurrency introduces readers to the algebraic properties and laws for true concurrency. The book provides readers with all aspects of algebraic theory for true concurrency, including the basis of semantics, calculi for true concurrency, axiomatization for true concurrency, as well as extensions and applications. 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 axiomatization for True Concurrency Integrates all aspects of algebraic theory for True Concurrency, along with extensions and applications