pith. sign in

arxiv: 2604.06443 · v1 · submitted 2026-04-07 · 💻 cs.LO · math.LO

The complexity of bisimilarity on pointmass processes

Mart\'in Santiago Moroni , Pedro S\'anchez Terraf This is my paper

Pith reviewed 2026-05-10 17:52 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords bisimilarityanalytic setsBorel setsnondeterministic labelled Markov processesdescriptive set theorymodal logicE0 equivalencewell-founded processes
0
0 comments X

The pith

Bisimilarity on nondeterministic labelled Markov processes with finitely supported measures is analytic, and Borel when the processes are well-founded.

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

The paper determines the descriptive complexity of bisimilarity, the relation that equates states with identical observable behavior, on nondeterministic labelled Markov processes over uncountable spaces. For the family of processes that assign the same finitely supported measure to each state and label, this relation is analytic. When the processes are well-founded and therefore terminate, the relation simplifies to Borel. The authors establish a lower bound by showing that the equivalence relation E0 of eventual agreement between binary sequences reduces to bisimilarity, which in turn implies that no countable fragment of basic modal logic with denumerable conjunctions can characterize bisimilarity on low-rank processes.

Core claim

Bisimilarity is analytic for processes with a uniform assignment of finitely-supported measures to each state and label. More finely, bisimilarity on the space of countable Kripke frames is classifiable by countable structures. Bisimilarity of well-founded processes is Borel. The relation of eventual equality of binary sequences E0 reduces to bisimilarity. As a consequence, there is no countable fragment of basic modal logic with denumerable conjunctions that characterizes bisimilarity for processes of small rank. The previous Borel definability is applied to study the well-founded part of discrete uniform processes over uncountable spaces.

What carries the argument

The bisimilarity relation on nondeterministic labelled Markov processes, which holds between states when their transition measures to bisimilar successor states match exactly for every label.

If this is right

  • Bisimilarity on the space of countable Kripke frames is classifiable by countable structures.
  • Bisimilarity of well-founded processes is a Borel set.
  • The equivalence relation E0 reduces to bisimilarity.
  • No countable fragment of basic modal logic with denumerable conjunctions characterizes bisimilarity for processes of small rank.
  • The well-founded part of discrete uniform processes over uncountable spaces admits Borel analysis.

Where Pith is reading between the lines

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

  • Verification procedures for continuous-state probabilistic systems may need to accommodate analytic but non-Borel relations in general.
  • Analogous complexity bounds could hold for other equivalences such as simulation or trace equivalence on the same models.
  • The results may inform the search for decidable or approximable fragments of bisimilarity in infinite-state systems.

Load-bearing premise

The processes are defined over uncountable standard Borel spaces and admit a uniform assignment of finitely-supported measures to each state and label.

What would settle it

A concrete nondeterministic labelled Markov process over an uncountable Borel space whose bisimilarity relation lies outside the analytic sets, or a well-founded process whose bisimilarity relation is not Borel.

Figures

Figures reproduced from arXiv: 2604.06443 by Mart\'in Santiago Moroni, Pedro S\'anchez Terraf.

Figure 1
Figure 1. Figure 1: The trees A(N) and A({0, 2, 4, . . . }). , Proof. We divide the construction of the function B into two steps: 1. Let M : 2N → (Tr N) N be given by M(x) = (A(mi(x)))i∈N. We show that M is continuous; let u ∈ N <N: (πn ◦ M) −1 [{T ∈ Tr N | u ∈ T}] = = {x ∈ 2 N | u ∈ πn(M(x))} = {x ∈ 2 N | u ∈ A(mn(x))} = ( ∅, if u is not admissible, {x ∈ 2 N | mn(x)(u0) = 1}, if u is admissible. The continuity of mn ensures… view at source ↗
Figure 2
Figure 2. Figure 2: The tree B(x) with explicit A(m0(x)) for x = {0, 2, 4, . . . }. Theorem 2.23. If x, y ⊆ N, then x E0 y ⇐⇒ (B(x), ∅) ∼ (B(y), ∅). Consequently, E0 ≤B ∼WF≤ω+2 . Proof. (⇒) If x and y differ on finitely many elements, the set of their finite modifications is the same and there exists a bijection h : N → N such that mn(x) = mh(n)(y). The relation R ⊆ B(x) × B(y) that glues the roots and the corresponding repre… view at source ↗
Figure 3
Figure 3. Figure 3: Obtaining a first-order structure from a pointed UMLTS. [PITH_FULL_IMAGE:figures/full_fig_p031_3.png] view at source ↗
read the original abstract

We assess the descriptive complexity of *bisimilarity* or "equality of behavior" on a family of Markov decision processes over uncountable standard Borel spaces, namely *nondeterministic labelled Markov processes* (NLMP). We show that bisimilarity is analytic for processes with a uniform assignment of finitely-supported measures to each state and label. More finely, we obtain that bisimilarity on the space of countable Kripke frames (or labelled transition systems) is classifiable by countable structures. We show that bisimilarity of well-founded ("terminating") processes is Borel. We also provide a lower complexity bound by reducing the relation of eventual equality of binary sequences $E_0$ to the former. As a consequence, there is no countable fragment of basic modal logic with denumerable conjunctions that characterizes bisimilarity for processes of small rank. We finally apply the previous Borel definability to study the well-founded part of discrete uniform processes over uncountable spaces.

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 / 2 minor

Summary. The manuscript studies the descriptive set-theoretic complexity of bisimilarity on nondeterministic labelled Markov processes (NLMP) over uncountable standard Borel spaces, focusing on pointmass processes with uniform finitely-supported measures. It establishes that bisimilarity is analytic in this setting and classifiable by countable structures when restricted to countable Kripke frames. For well-founded (terminating) processes, bisimilarity is shown to be Borel. A lower bound is obtained by reducing the eventual equality relation E0 to bisimilarity, implying that no countable fragment of basic modal logic with denumerable conjunctions characterizes bisimilarity for processes of small rank. The results are applied to analyze the well-founded part of discrete uniform processes.

Significance. If the claims hold, the work provides precise complexity bounds for behavioral equivalence in continuous-state probabilistic systems using standard descriptive set theory. The analytic upper bound, the Borel result for well-founded processes, the explicit E0 reduction establishing hardness, and the derived modal-logic non-characterization are all load-bearing contributions. The classification by countable structures for Kripke frames and the application to discrete uniform processes add further value. These results help delineate the boundary between Borel and analytic definability for bisimilarity and have implications for verification and logical expressiveness.

minor comments (2)
  1. §1 (Introduction): the term 'pointmass processes' is used in the title and abstract but is not explicitly defined until later; a one-sentence clarification linking it to the uniform finitely-supported measure assignment would improve readability for readers outside descriptive set theory.
  2. The E0 reduction (presumably in §4 or §5) is central to the hardness claim; while the abstract states it clearly, ensuring the reduction is spelled out with explicit mappings between binary sequences and process states would strengthen the presentation.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive report, accurate summary of our contributions on the descriptive complexity of bisimilarity for NLMP pointmass processes, and the recommendation of minor revision. We are pleased that the analytic upper bound, Borel result for well-founded processes, E0-hardness, and modal-logic implications are recognized as load-bearing.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The derivation relies on standard descriptive-set-theoretic constructions (analytic and Borel sets over standard Borel spaces) together with an explicit reduction from the external E0 equivalence relation on binary sequences. The upper bounds (analyticity under uniform finitely-supported measures, Borel for well-founded processes) and the modal-logic non-characterization consequence follow directly from these external tools once the process space and measure restrictions are fixed; no step equates a claimed result to a fitted parameter or to a self-citation that itself presupposes the target claim. The paper is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard results from descriptive set theory and modal logic without introducing new free parameters or postulated entities.

axioms (2)
  • standard math Standard properties of standard Borel spaces and the Borel/analytic hierarchy
    Invoked to define the state spaces and assign complexity classes to bisimilarity.
  • domain assumption Basic properties of bisimilarity on labelled transition systems and Markov processes
    Used as the definition of the equivalence relation under study.

pith-pipeline@v0.9.0 · 5467 in / 1212 out tokens · 36777 ms · 2026-05-10T17:52:23.511030+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

  1. [1]

    Arveson , `` title An Invitation to C*-Algebras '', series Graduate texts in mathematics volume 39 , publisher Springer-Verlag ( year 1976 )

    author W. Arveson , `` title An Invitation to C*-Algebras '', series Graduate texts in mathematics volume 39 , publisher Springer-Verlag ( year 1976 )

    work page 1976

  2. [2]

    Blackburn , author J.v

    author P. Blackburn , author J.v. Benthem , author F. Wolter , `` title Handbook of Modal Logic '', series Studies in Logic and Practical Reasoning volume 3 , publisher Elsevier Science Inc. , address New York, NY, USA ( year 2006 )

    work page 2006

  3. [3]

    Danos , author J

    author V. Danos , author J. Desharnais , author F. Laviolette , author P. Panangaden , title Bisimulation and cocongruence for probabilistic systems , journal Inf. Comput. volume 204 : pages 503--523 ( year 2006 )

    work page 2006

  4. [4]

    D'Argenio , author P

    author P.R. D'Argenio , author P. S\' a nchez Terraf , author N. Wolovick , title Bisimulations for non-deterministic labelled M arkov processes , journal Mathematical Structures in Comp. Sci. volume 22 : pages 43--68 ( year 2012 )

    work page 2012

  5. [5]

    D'Argenio , author N

    author P.R. D'Argenio , author N. Wolovick , author P. S \'a nchez Terraf , author P. Celayes , title Nondeterministic labeled M arkov processes: Bisimulations and logical characterization , in: booktitle QEST , pages 11--20 ( year 2009 )

    work page 2009

  6. [6]

    Friedman , author L

    author H. Friedman , author L. Stanley , title A B orel reducibility theory for classes of countable structures , journal Journal of Symbolic Logic volume 54 : pages 894--914 ( year 1989 )

    work page 1989

  7. [7]

    Gao , `` title Invariant Descriptive Set Theory '', Chapman & Hall/CRC Pure and Applied Mathematics, publisher CRC Press ( year 2008 )

    author S. Gao , `` title Invariant Descriptive Set Theory '', Chapman & Hall/CRC Pure and Applied Mathematics, publisher CRC Press ( year 2008 )

    work page 2008

  8. [8]

    Goranko , author M

    author V. Goranko , author M. Otto , title Model theory of modal logic , in: editor P. Blackburn , editor J. Van Benthem , editor F. Wolter (Eds.), booktitle Handbook of Modal Logic , series Studies in Logic and Practical Reasoning volume 3 , publisher Elsevier : pages 249--329 ( year 2007 )

    work page 2007

  9. [9]

    Halmos , `` title Measure Theory '', publisher Van Nostrand Company, Inc

    author P.R. Halmos , `` title Measure Theory '', publisher Van Nostrand Company, Inc. ( year 1950 )

    work page 1950

  10. [10]

    Harrington , author A.S

    author L. Harrington , author A.S. Kechris , author A. Louveau , title A Glimm-Effros dichotomy for Borel equivalence relations , journal Journal of the American Mathematical Society volume 3 : pages 903--928 ( year 1990 )

    work page 1990

  11. [11]

    Kechris , `` title Classical Descriptive Set Theory '', series Graduate Texts in Mathematics volume 156 , publisher Springer-Verlag ( year 1994 )

    author A.S. Kechris , `` title Classical Descriptive Set Theory '', series Graduate Texts in Mathematics volume 156 , publisher Springer-Verlag ( year 1994 )

    work page 1994

  12. [12]

    Moroni , author P

    author M.S. Moroni , author P. S \'a nchez Terraf , title A classification of bisimilarities for general M arkov decision processes , journal Mathematical Structures in Computer Science volume 35 ( year 2025 )

    work page 2025

  13. [13]

    S \'a nchez Terraf , title Bisimilarity is not B orel , journal Mathematical Structures in Computer Science volume 27 : pages 1265--1284 ( year 2017 )

    author P. S \'a nchez Terraf , title Bisimilarity is not B orel , journal Mathematical Structures in Computer Science volume 27 : pages 1265--1284 ( year 2017 )

    work page 2017

  14. [14]

    Wolovick , `` title Continuous Probability and Nondeterminism in Labeled Transition Systems '', Ph.D

    author N. Wolovick , `` title Continuous Probability and Nondeterminism in Labeled Transition Systems '', Ph.D. thesis, Universidad Nacional de C\'ordoba ( year 2012 )

    work page 2012