Computation and Concurrency

TL;DR

The work develops a unified framework linking computation and true concurrency through pomset-based models, introducing Series-Communication-Parallelism and the pomsetc language to capture parallelism, communication, and concurrency. It builds scr-expressions and BKAC-based algebras, proving soundness and completeness results for language equivalence and several true-concurrency bisimilarities, and extends these with prefix, recursion, encapsulation, silent steps, and abstraction. Reduction techniques (reification, lifting, decomposition) and exchange laws are developed to enable modular reasoning and to relate different semantic equivalences, including proofs about completeness and decidability. Overall, the paper offers a comprehensive algebraic and operational treatment of computation and concurrency in a true-concurrency setting, providing tools for formal verification and synthesis of concurrent systems.

Abstract

We try to clarify the relationship between computation and concurrency. Base on the so-called pomsetc automata, we introduce communication and more operators, and establish the algebras modulo language equivalence and truly concurrent bisimilarities.

Figures (5)

• Figure 1: PA accepting $a \cdot (b \parallel c) \cdot d$.
• Figure 2: PA accepting $a \cdot (b \mid c) \cdot d$.
• Figure 3: PA accepting $a \cdot (b \between c) \cdot d$.
• Figure 4: PA accepting $(a \cdot b\cdot c) \between (d \cdot e\cdot f)$ with $\rho(b,e)$ defined.
• Figure 5: Equivalent PA accepting $(a \cdot b\cdot c) \between (d \cdot e\cdot f)$ with $\rho(b,e)$ defined.

Theorems & Definitions (425)

• Definition 2.1: Set
• Definition 2.2: Set composition
• Definition 2.3: Tuple
• Definition 2.4: Relation
• Definition 2.5: Preorder, partial order, strict order
• Definition 2.6: Equivalence
• Definition 2.7: Relation composition
• Definition 2.8: Function
• Definition 2.9: Poset morphism
• Definition 2.10: Multiset