pith. machine review for the scientific record. sign in

arxiv: 2605.07373 · v1 · submitted 2026-05-08 · 💻 cs.LO

Recognition: no theorem link

Finitary Truly Concurrent Bisimulations

Yong Wang
Authors on Pith no claims yet

Pith reviewed 2026-05-11 01:53 UTC · model grok-4.3

classification 💻 cs.LO
keywords finitary bisimulationtruly concurrent processesprebisimulation preorderdenotational semanticsbehavioural semanticsfull abstractionprocess algebra
0
0 comments X

The pith

Truly concurrent prebisimulations require finitary versions to align denotational models with finite process observations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines truly concurrent prebisimulations and their finitary forms by extending the behavioural version of finitary bisimulation. This step is taken because denotational interpretations of processes only guarantee matching finite observations, while full prebisimulation can separate behaviours using infinite observations. Without the finitary restriction, full abstraction between the denotational model and the preorder fails. A reader would care because the finitary definitions restore the ability to prove that two processes are equivalent exactly when their denotational meanings coincide.

Core claim

Following the behavioural form of finitary bisimulation, definitions are given for truly concurrent prebisimulations and their finitary counterparts. These definitions are introduced to support a full abstract denotational model based on the prebisimulation preorder for a process language. The need arises because standard denotational interpretations afford the same finite observations to related processes, yet prebisimulation can still distinguish them on the basis of infinite observations.

What carries the argument

truly concurrent prebisimulations and their finitary versions, which restrict distinctions to finite observations while preserving the concurrent structure.

If this is right

  • Full abstraction holds between the denotational model and the prebisimulation preorder once the finitary restriction is applied.
  • Process equivalences can be decided using only finite observations without losing the concurrent character of the semantics.
  • The prebisimulation preorder admits a finitary approximation that matches the observable behaviour exactly.
  • Existing results on finitary bisimulation extend directly to the truly concurrent case via the behavioural form.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The definitions may serve as a template for finitary versions in other true-concurrency models such as event structures.
  • Practical tools could implement these finitary relations to check equivalence on finite-state concurrent systems.
  • Combining the finitary behavioural definitions with logical characterisations could yield completeness theorems for the preorder.

Load-bearing premise

The behavioural form of finitary bisimulation supplies the correct basis for defining the finitary part of truly concurrent prebisimulation.

What would settle it

Two processes that the finitary truly concurrent prebisimulation equates but whose denotational interpretations under the prebisimulation preorder differ, or vice versa.

read the original abstract

To develop a full abstract denotational model of a process language based on prebisimulation preorder, its behavioural semantics has two problems: (1) Two processes related by a standard denotational interpretation afford the same finite observations. (2) Prebisimulation can make distinctions between the behaviours of two processes based on infinite observations. So, finitary part of prebisimulation is needed to obtain full abstract results. There existed two main results on finitary bisimulation: the logical form and the behavioural form. Following the latter one, we give the definitions of truly concurrent prebisimulations and their finitary ones.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 1 minor

Summary. The paper addresses challenges in obtaining full abstraction for denotational models of process languages based on the prebisimulation preorder. It identifies two problems: denotational interpretations equate processes that afford identical finite observations, while prebisimulations may distinguish behaviours using infinite observations. To resolve this, the authors follow the behavioural form of finitary bisimulation and supply definitions of truly concurrent prebisimulations together with their finitary restrictions.

Significance. If the supplied definitions are sound and indeed yield full abstraction, the work would usefully extend existing finitary-bisimulation results to the truly concurrent setting. This could strengthen the correspondence between denotational and behavioural semantics for true-concurrency models, supporting more precise equivalence checking in process algebra. The choice of the behavioural route is consistent with prior literature and directly addresses the stated motivation.

minor comments (1)
  1. [Abstract] The abstract states that definitions are given but does not indicate whether any accompanying theorems (e.g., congruence properties or full-abstraction proofs) are established; a brief statement of the main results would clarify the scope of the contribution.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our manuscript and the recommendation for minor revision. The summary accurately captures our motivation and approach in defining finitary truly concurrent prebisimulations via the behavioural form.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper's contribution consists of supplying definitions for truly concurrent prebisimulations and their finitary variants by direct reference to the pre-existing behavioural form of finitary bisimulation. No equations, parameter fittings, predictions, or derivations appear that reduce by construction to the paper's own inputs or to a self-referential chain. The approach is self-contained: it adopts an established external behavioural template and extends it to the truly concurrent setting without invoking load-bearing self-citations, uniqueness theorems, or ansatzes that collapse into the target result.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on domain assumptions about the suitability of prebisimulation preorder for full abstraction and the existence of prior logical/behavioural forms of finitary bisimulation. No free parameters or invented entities are evident from the abstract.

axioms (2)
  • domain assumption Prebisimulation preorder can form the basis for a full abstract denotational model of a process language.
    Stated as the development goal in the abstract, with problems (1) and (2) identified as barriers.
  • domain assumption Finitary part of prebisimulation is needed to obtain full abstract results.
    Directly asserted to resolve the mismatch between finite observations and infinite distinctions.

pith-pipeline@v0.9.0 · 5383 in / 1290 out tokens · 36530 ms · 2026-05-11T01:53:05.794688+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

131 extracted references · 131 canonical work pages · 1 internal anchor

  1. [1]

    R. Milner. Communication and concurrency. 1989

    work page 1989

  2. [2]

    R. Milner. A calculus of communicating systems. 1980

    work page 1980

  3. [3]

    C. A. R. Hoare , title =. Communications of the ACM , volume =. 1978 , month = aug, doi =

    work page 1978

  4. [4]

    C. A. R. Hoare , title =. 1985 , isbn =

    work page 1985

  5. [5]

    W. Fokkink. Introduction to process algebra. 2007

    work page 2007

  6. [6]

    Y. Wang. Algebraic theory for true concurrency. 2023

    work page 2023

  7. [7]

    Y. Wang. Handbook of truly concurrent process algebra. 2023

    work page 2023

  8. [8]

    Information and Computation , year=

    A calculus of mobile processes, I , author=. Information and Computation , year=

    work page

  9. [9]

    Information and Computation , volume=

    A calculus of mobile processes, II , author=. Information and Computation , volume=

    work page

  10. [10]

    Proceedings of the 1st ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC 1982) , pages=

    Four Combinators for Concurrency , author=. Proceedings of the 1st ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC 1982) , pages=. 1982 , organization=

    work page 1982

  11. [11]

    Logics and Models of Concurrent Systems , editor=

    Notes on Algebraic Calculi of Processes , author=. Logics and Models of Concurrent Systems , editor=. 1985 , publisher=

    work page 1985

  12. [12]

    Computational Problems in Abstract Algebra , pages=

    Simple word problems in universal algebras , author=. Computational Problems in Abstract Algebra , pages=. 1970 , publisher=

    work page 1970

  13. [13]

    Vaandrager

    F.W. Vaandrager. Verification of two communication protocols by means of process algebra. 1986

    work page 1986

  14. [14]

    DAIMI Report Series , number=

    Models for concurrency , author=. DAIMI Report Series , number=

    work page

  15. [15]

    Journal of the Acm , volume=

    A Logic for True Concurrency , author=. Journal of the Acm , volume=

    work page

  16. [16]

    1979 , publisher=

    Petri nets, event structures and domains, 1 , author=. 1979 , publisher=

    work page 1979

  17. [17]

    advanced course on Petri nets , pages=

    Event structures , author=. advanced course on Petri nets , pages=. 1986 , organization=

    work page 1986

  18. [18]

    DAIMI Report Series , number=

    An introduction to event structures , author=. DAIMI Report Series , number=

    work page

  19. [19]

    Mathematical Foundations of Computer Science 1999: 24th International Symposium, MFCS’99, Poland, September 6--10, 1999 Proceedings 24 , pages=

    On plain and hereditary history-preserving bisimulation , author=. Mathematical Foundations of Computer Science 1999: 24th International Symposium, MFCS’99, Poland, September 6--10, 1999 Proceedings 24 , pages=. 1999 , organization=

    work page 1999

  20. [20]

    Journal of Logical and Algebraic Methods in Programming , volume=

    Reduction of event structures under history preserving bisimulation , author=. Journal of Logical and Algebraic Methods in Programming , volume=. 2016 , publisher=

    work page 2016

  21. [21]

    Fundamenta Informaticae , volume=

    A non-interleaving semantics for CCS based on proved transitions , author=. Fundamenta Informaticae , volume=. 1988 , publisher=

    work page 1988

  22. [22]

    Theoretical Computer Science , volume=

    A partial ordering semantics for CCS , author=. Theoretical Computer Science , volume=. 1990 , publisher=

    work page 1990

  23. [23]

    Automata, Languages and Programming: Ninth Colloquium Aarhus, Denmark, July 12--16, 1982 9 , pages=

    Event structure semantics for CCS and related languages , author=. Automata, Languages and Programming: Ninth Colloquium Aarhus, Denmark, July 12--16, 1982 9 , pages=. 1982 , organization=

    work page 1982

  24. [24]

    Handbook of process algebra , pages=

    Structural operational semantics , author=. Handbook of process algebra , pages=. 2001 , publisher=

    work page 2001

  25. [25]

    Communications of the ACM , volume=

    Letters to the editor: go to statement considered harmful , author=. Communications of the ACM , volume=. 1968 , publisher=

    work page 1968

  26. [26]

    1972 , publisher=

    Structured programming , author=. 1972 , publisher=

    work page 1972

  27. [27]

    Fundamentals of Software Engineering: Third IPM International Conference, FSEN 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected Papers 3 , pages=

    A process-theoretic look at automata , author=. Fundamentals of Software Engineering: Third IPM International Conference, FSEN 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected Papers 3 , pages=. 2010 , organization=

    work page 2009

  28. [28]

    Technische Universiteit Eindhoven, Syllabus 2IT15 , year=

    Models of computation: automata and processes , author=. Technische Universiteit Eindhoven, Syllabus 2IT15 , year=

    work page

  29. [29]

    Distributed Computing and Internet Technology: 7th International Conference, ICDCIT 2011, Bhubaneshwar, India, February 9-12, 2011

    Computations and interaction , author=. Distributed Computing and Internet Technology: 7th International Conference, ICDCIT 2011, Bhubaneshwar, India, February 9-12, 2011. Proceedings 7 , pages=. 2011 , organization=

    work page 2011

  30. [30]

    CONCUR 2012--Concurrency Theory: 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012

    Turing meets milner , author=. CONCUR 2012--Concurrency Theory: 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings 23 , pages=. 2012 , organization=

    work page 2012

  31. [31]

    Implementation and Application of Automata: 19th International Conference, CIAA 2014, Giessen, Germany, July 30--August 2, 2014

    Partial derivative and position bisimilarity automata , author=. Implementation and Application of Automata: 19th International Conference, CIAA 2014, Giessen, Germany, July 30--August 2, 2014. Proceedings 19 , pages=. 2014 , organization=

    work page 2014

  32. [32]

    Mathematical Structures in Computer Science , volume=

    Expressiveness modulo bisimilarity of regular expressions with parallel composition , author=. Mathematical Structures in Computer Science , volume=. 2016 , publisher=

    work page 2016

  33. [33]

    Journal of the ACM (JACM) , volume=

    A characterization of regular expressions under bisimulation , author=. Journal of the ACM (JACM) , volume=. 2007 , publisher=

    work page 2007

  34. [34]

    Journal of logical and algebraic methods in programming , volume=

    On series-parallel pomset languages: rationality, context-freeness and automata , author=. Journal of logical and algebraic methods in programming , volume=. 2019 , publisher=

    work page 2019

  35. [35]

    , author=

    Learning pomset automata. , author=. FoSSaCS , pages=

    work page

  36. [36]

    Foundations of Software Technology and Theoretical Computer Science: 18th Conference, Chennai, India, December 17-19, 1998

    A Kleene iteration for parallelism , author=. Foundations of Software Technology and Theoretical Computer Science: 18th Conference, Chennai, India, December 17-19, 1998. Proceedings 18 , pages=. 1998 , organization=

    work page 1998

  37. [37]

    Annual Symposium on Theoretical Aspects of Computer Science , pages=

    Series-parallel posets: algebra, automata and languages , author=. Annual Symposium on Theoretical Aspects of Computer Science , pages=. 1998 , organization=

    work page 1998

  38. [38]

    Theoretical Computer Science , volume=

    Series-parallel languages and the bounded-width property , author=. Theoretical Computer Science , volume=. 2000 , publisher=

    work page 2000

  39. [39]

    Information and Computation , volume=

    Rationality in algebras with a series operation , author=. Information and Computation , volume=. 2001 , publisher=

    work page 2001

  40. [40]

    41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021) , year=

    Branching automata and pomset automata , author=. 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021) , year=

    work page 2021

  41. [41]

    Computation and Concurrency

    Computation and concurrency , author=. arXiv preprint arXiv:2409.02595 , year=

    work page internal anchor Pith review Pith/arXiv arXiv

  42. [42]

    Proceedings of the London Mathematical Society , volume=

    On computable numbers, with an application to the Entscheidungsproblem , author=. Proceedings of the London Mathematical Society , volume=. 1936 , doi=

    work page 1936

  43. [43]

    A correction , author=

    On computable numbers, with an application to the Entscheidungsproblem. A correction , author=. Proceedings of the London Mathematical Society , volume=. 1937 , doi=

    work page 1937

  44. [44]

    Transactions of the American Mathematical Society , volume=

    On the computational complexity of algorithms , author=. Transactions of the American Mathematical Society , volume=. 1965 , doi=

    work page 1965

  45. [45]

    Information and Control , volume=

    One-tape, off-line Turing machine computations , author=. Information and Control , volume=. 1965 , doi=

    work page 1965

  46. [46]

    IEEE Transactions on Electronic Computers , volume=

    Real-time computation and recursive functions not real-time computable , author=. IEEE Transactions on Electronic Computers , volume=. 1962 , doi=

    work page 1962

  47. [47]

    Journal of the ACM (JACM) , volume=

    Two-Tape Simulation of Multitape Turing Machines , author=. Journal of the ACM (JACM) , volume=. 1966 , doi=

    work page 1966

  48. [48]

    Journal of Computer and System Sciences , volume=

    Deterministic multitape automata computations , author =. Journal of Computer and System Sciences , volume=

    work page

  49. [49]

    Automata studies , volume=

    Representation of events in nerve nets and finite automata , author=. Automata studies , volume=. 1956 , publisher=

    work page 1956

  50. [50]

    Journal of the ACM (JACM) , volume=

    Two complete axiom systems for the algebra of regular events , author=. Journal of the ACM (JACM) , volume=. 1966 , publisher=

    work page 1966

  51. [51]

    J. H. Conway. Regular algebra and finite machines. 1971

    work page 1971

  52. [52]

    D. Kozen. On induction vs. *-continuity. Proc. Workshop on Logics of Programs 1981. 1981

    work page 1981

  53. [53]

    D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. 1990

    work page 1990

  54. [54]

    V. Pratt. Dynamic algebras and the nature of induction. Proc. 12th ACM Symp. on Theory of Computing. 1980

    work page 1980

  55. [55]

    W. Kuich. The Kleene and Parikh theorem in complete semirings. Proc. 14th Colloq. Automata, Languages, and Programming. 1987

    work page 1987

  56. [56]

    1990 , publisher=

    On Kleene algebras and closed semirings , author=. 1990 , publisher=

    work page 1990

  57. [57]

    D. Kozen. Kleene algebra with tests and commutativity conditions. TACAS. 1996

    work page 1996

  58. [58]

    Springer International Publishing , year=

    Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages , author=. Springer International Publishing , year=

    work page

  59. [59]

    R. Milner. A complete inference system for a class of regular behaviours. J. Comput. System Sci. 1984

    work page 1984

  60. [60]

    Ukrainskii Matematicheskii Zhurnal , volume=

    On defining relations for the algebra of regular events , author=. Ukrainskii Matematicheskii Zhurnal , volume=

    work page

  61. [61]

    Information processing letters , volume=

    A complete equational axiomatization for prefix iteration , author=. Information processing letters , volume=. 1994 , publisher=

    work page 1994

  62. [62]

    Fundamenta Informaticae , volume=

    A complete axiomatization for prefix iteration in branching bisimulation , author=. Fundamenta Informaticae , volume=. 1996 , publisher=

    work page 1996

  63. [63]

    BRICS Report Series , volume=

    A complete equational axiomatization for prefix iteration with silent steps , author=. BRICS Report Series , volume=

    work page

  64. [64]

    Information and Computation , volume=

    An equational axiomatization for multi-exit iteration , author=. Information and Computation , volume=. 1997 , publisher=

    work page 1997

  65. [65]

    Lecture notes in computer science , pages=

    Axiomatizing flat iteration , author=. Lecture notes in computer science , pages=. 1997 , publisher=

    work page 1997

  66. [66]

    Theoretical Computer Science , volume=

    Non-regular iterators in process algebra , author=. Theoretical Computer Science , volume=. 2001 , publisher=

    work page 2001

  67. [67]

    The Computer Journal , volume=

    Process algebra with iteration and nesting , author=. The Computer Journal , volume=. 1994 , publisher=

    work page 1994

  68. [68]

    1993 , publisher=

    Process algebra with iteration , author=. 1993 , publisher=

    work page 1993

  69. [69]

    Fokkink and H

    W. Fokkink and H. Zantema. Basic process algebra with iteration: completeness of its equational axioms. Comput. J. 1994

    work page 1994

  70. [70]

    Algebraic Methodology and Software Technology: Proceedings of the 5th International Conference, AMAST'96 Munich, Germany, July 1--5 , pages=

    On the completeness of the equations for the Kleene star in bisimulation , author=. Algebraic Methodology and Software Technology: Proceedings of the 5th International Conference, AMAST'96 Munich, Germany, July 1--5 , pages=. 1996 , organization=

    work page 1996

  71. [71]

    Grabmayer and W

    C. Grabmayer and W. Fokkink. A complete proof system for 1-Free regular expressions modulo bisimilarity. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. 2020

    work page 2020

  72. [72]

    Grabmayer

    C. Grabmayer. Structure-constrained process graphs for the process semantics of regular expressions. Proceedings 11th International Workshop on Computing with Terms and Graphs. 2021

    work page 2021

  73. [73]

    Grabmayer

    C. Grabmayer. A coinductive version of Milner’s proof system for regular expressions modulo bisimilarity. Proceedings of the 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). 2021

    work page 2021

  74. [74]

    Grabmayer

    C. Grabmayer. Milner’s proof system for regular expressions modulo bisimilarity is complete: crystallization: near-collapsing process graph interpretations of regular expressions. Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. 2022

    work page 2022

  75. [75]

    arXiv preprint arXiv:2303.08553 , year=

    The Image of the Process Interpretation of Regular Expressions is Not Closed under Bisimulation Collapse , author=. arXiv preprint arXiv:2303.08553 , year=

    work page arXiv

  76. [76]

    E. Cohen. Hypotheses in Kleene algebra. 1994

    work page 1994

  77. [77]

    Doumane and D

    A. Doumane and D. Kuperberg and D. Pous and P. Pradic. Kleene algebra with hypotheses. Proceedings of the FOSSACS. 2019. 2019

    work page 2019

  78. [78]

    Cohen and D

    E. Cohen and D. Kozen and F. Smith. The complexity of Kleene algebra with tests. 1996

    work page 1996

  79. [79]

    D. Kozen. On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 2000. doi:10.1145/343369.3433785

    work page doi:10.1145/343369.3433785 2000

  80. [80]

    Angus and D

    A. Angus and D. Kozen. Kleene algebra with tests and program schematology. 2001

    work page 2001

Showing first 80 references.