Algebraic Theory for True Concurrency

1. Introduction

2. Semantics and Logic for True Concurrency

2.1 Process algebras

2.1.1 CCS, ACP and CSP

2.1.2 Operational semantics

2.1.3 Proof techniques

2.2 true concurrency

2.2.1 Event structure

2.2.2 Concurrent Bisimilarities

3. A Calculus for True Concurrency

3.1 Syntax and operational semantics

3.1.1 Syntax

3.1.2 Operational semantics

3.2.3 Properties of transitions

3.2 Strongly truly concurrent bisimulations

3.2.1 Basic definitions

3.2.2 Laws and congruence

3.2.3 Recursion

3.3 Weakly truly concurrent bisimulations

3.3.1 Basic definitions

3.3.2 Laws and congruence

3.3.3 Recursion

3.4 Applications

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 equivalence

4.4.2 Guarded linear recursion

4.4.3 Algebraic laws for the silent step

4.4.4 Abstraction

4.4.5 Applications

4.4.6 Extensions

4.4.6.1 Placeholder

4.4.6.2 Renaming

4.4.6.3 States

5. A Calculus for Truly Concurrent Mobile Processes

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 bisimularities

5.2.1 Basic definitions

5.2.2 Laws and congruence

5.2.3 Recursion

5.3 Algebraic Theory

6. Guards

7. Timing

7.1 Discrete relative timing

7.1.1 Basic definitions

7.1.2 Basic algebra for true concurrency with discrete relative timing

7.1.3 Algebra for parallelism in true concurrency with discrete relative timing

7.2 Discrete absolute timing

7.2.1 Basic definitions

7.2.2 Basic algebra for true concurrency with discrete absolute timing

7.2.3 Algebra for parallelism in true concurrency with discrete absolute timing

7.2.4 Discrete Initial Abstraction

7.2.5 Time-dependent conditions

7.3 Continuous relative timing

7.3.1 Basic definitions

7.3.2 Basic algebra for true concurrency with continuous relative timing

7.3.3 BATCSRT with integration

7.3.4 Algebra for parallelism in true concurrency with continuous relative timing

7.3.5 APTCSRT with integration

7.4 Continuous absolute timing

7.4.1 Basic definitions

7.4.2 Basic algebra for true concurrency with continuous absolute timing

7.4.3 BATCSAT with integration

7.4.4 Algebra for parallelism in true concurrency with continuous absolute timing

7.4.5 APTCSAT with integration

7.4.6 Standard initial abstraction

7.4.7 Time-dependent conditions

7.5 Recursion

7.5.1 Discrete relative timing

7.5.2 Discrete absolute timing

7.5.3 Continuous relative timing

7.5.4 Continuous absolute timing

7.6 Abstraction

7.6.1 Discrete relative timing

7.6.2 Discrete absolute timing

7.6.3 Continuous relative timing

7.6.4 Continuous absolute timing

7.7 Applications

7.8 Extensions