Testing Theory of Truly Concurrent Processes
Pith reviewed 2026-06-27 05:42 UTC · model grok-4.3
The pith
Truly concurrent processes admit testing semantics that inherit the operational-axiomatic-denotational trinity.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The paper establishes testing semantics for truly concurrent processes that follows Hennessy's approach and thereby provides operational semantics, axiomatic semantics, and denotational semantics for these processes.
What carries the argument
The adapted testing semantics that defines process equivalence based on the ability to pass or fail certain tests, extended to capture true concurrency behaviors.
If this is right
- Operational semantics for truly concurrent processes can be defined through testing.
- Algebraic axioms can be derived for the testing equivalence.
- Denotational models can be constructed using the testing preorder.
- This framework allows for the analysis of true concurrent systems using established techniques from interleaving concurrency.
Where Pith is reading between the lines
- The semantics could support direct transfer of testing-based verification methods to domains that require true concurrency.
- It may reduce the practical gap between true concurrency and interleaving models when equivalence is defined by tests.
- Alignment with specific models such as event structures could be checked by applying the same tests.
Load-bearing premise
The testing framework developed for interleaving concurrency can be directly adapted to truly concurrent processes while preserving the operational-axiomatic-denotational trinity.
What would settle it
A concrete truly concurrent process for which the adapted testing equivalence fails to match either its operational behavior, its algebraic axioms, or its denotational model would settle the claim.
Figures
read the original abstract
A process is able to execute a set of actions with a predefined manner, while a truly concurrent process executes this set of actions with a manner with the flavour of true concurrency. The so-called truly concurrent process algebras bridge the true concurrency (such as Petri nets, event structures, etc), and the interleaving concurrency (such as CCS, CSP, ACP, etc). In this paper, we give truly concurrent processes testing semantics followed by Hennessy's great work, which inherits the trinity of operational semantics, axiomatic semantics and denotational semantics.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper claims to develop testing semantics for truly concurrent processes by extending Hennessy's framework from interleaving concurrency, asserting that the resulting semantics inherits the trinity of operational, axiomatic, and denotational semantics.
Significance. If the inheritance of the trinity is demonstrated with explicit definitions and proofs, the work could bridge true-concurrency models (Petri nets, event structures) with interleaving models (CCS, CSP, ACP), extending classical testing theory in process algebra.
major comments (1)
- [Abstract] Abstract: the claim that the testing semantics 'inherits the trinity of operational semantics, axiomatic semantics and denotational semantics' is asserted without any definitions, proofs, or examples, leaving the central claim without visible support or derivation steps.
Simulated Author's Rebuttal
We thank the referee for the careful reading and the constructive comment on the abstract. We address it point by point below.
read point-by-point responses
-
Referee: [Abstract] Abstract: the claim that the testing semantics 'inherits the trinity of operational semantics, axiomatic semantics and denotational semantics' is asserted without any definitions, proofs, or examples, leaving the central claim without visible support or derivation steps.
Authors: The abstract is a concise summary of the paper's main contribution. The full manuscript extends Hennessy's testing framework to truly concurrent process algebras by defining an operational testing semantics (via may- and must-testing preorders on processes), providing an axiomatic semantics (a sound and complete equational theory), and developing a corresponding denotational semantics (using event structures or similar truly concurrent models). We include proofs that the three semantics coincide, thereby inheriting the trinity. We will revise the abstract to make this structure explicit and to reference the sections where the definitions and proofs appear. revision: yes
Circularity Check
No circularity; direct adaptation of external Hennessy framework
full rationale
The paper states it gives testing semantics for truly concurrent processes 'followed by Hennessy's great work' and inherits the operational-axiomatic-denotational trinity. No equations, definitions, or claims in the provided material reduce any result to a self-fit, self-citation chain, or renaming of inputs. The central step is an explicit extension of an independent external source (Hennessy), with no load-bearing self-referential steps or uniqueness theorems imported from the authors' prior work. The derivation is therefore self-contained against external benchmarks.
Axiom & Free-Parameter Ledger
Reference graph
Works this paper leans on
-
[1]
Wang, Algebraic theory for true concurrency, Elsevier AP, 2023
Y. Wang, Algebraic theory for true concurrency, Elsevier AP, 2023
2023
-
[2]
Wang, Handbook of truly concurrent process algebra, Elsevier MK, 2023
Y. Wang, Handbook of truly concurrent process algebra, Elsevier MK, 2023
2023
-
[3]
C. A. Petri, Non-sequential processes, GMD-ISF Report 77 (5) (1977)
1977
-
[4]
C. A. Petri, General net theory. communication disciplines, in: proc. Joint IBM University of Newcastle Seminar, B. Shaw ed., Newcastle GB, 1976
1976
-
[5]
C. A. Petri, Concurrency as a basis of systems thinking, in: Proc. from 5th Scandinavian Logic Symposium, 1979, pp. 143–162
1979
-
[6]
Winskel, Event structures, in: advanced course on Petri nets, Springer, 1986, pp
G. Winskel, Event structures, in: advanced course on Petri nets, Springer, 1986, pp. 325– 392
1986
-
[7]
Milner, A calculus of communicating systems, Springer, 1980
R. Milner, A calculus of communicating systems, Springer, 1980
1980
-
[8]
C. A. R. Hoare, Communicating sequential processes, Communications of the ACM 21 (8) (1978) 666–677. doi:10.1145/359576.359585
-
[9]
C. A. R. Hoare, Communicating sequential processes, Prentice Hall International Series in Computer Science, Prentice-Hall, 1985
1985
-
[10]
Fokkink, Introduction to process algebra, 2nd Edition, Springer-Verlag, 2007
W. Fokkink, Introduction to process algebra, 2nd Edition, Springer-Verlag, 2007
2007
-
[11]
Hennessy, Algebraic theory of processes, Foundations of Computing, MIT Press, Cam- bridge, MA, 1988
M. Hennessy, Algebraic theory of processes, Foundations of Computing, MIT Press, Cam- bridge, MA, 1988
1988
-
[12]
Kapp´ e, Concurrent kleene algebra: completeness and decidability (doctoral dissertation, Ph.D
T. Kapp´ e, Concurrent kleene algebra: completeness and decidability (doctoral dissertation, Ph.D. thesis, UCL (University College London) (2020)
2020
-
[13]
Scott, C
D. Scott, C. Strachey, Towards a mathematical semantics for computer languages, in: J. Fox (Ed.), Proceedings of the Symposium on Computers and Automata, Vol. 21 of MRI Sym- posium Proceedings, Polytechnic Press, Brooklyn, New York, 1971, pp. 19–46
1971
-
[14]
J. A. Goguen, J. W. Thatcher, E. G. Wagner, J. B. Wright, Initial algebra semantics and continuous algebras, J. ACM 24 (1) (1977) 68–95. doi:10.1145/321992.321997
-
[15]
Guessarian, Algebraic Semantics, Vol
I. Guessarian, Algebraic Semantics, Vol. 99 of Lecture Notes in Computer Science, Springer,
-
[16]
doi:10.1007/3-540-10284-7. 63
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.