PaperlayerView exact revision on arXiv

Source-linked AI summary

A Lumpability-Driven Taxonomy of Strong and Weak Stochastic Bisimilarities with Their Congruence Properties

Riccardo Romanello, Andrea Esposito, Marco Bernardo, Carla Piazza, Sabina Rossi

arXiv:2609.11893v1cs.LO

TL;DR

PEPA stochastic bisimilarities are scattered across the literature under terminology that makes comparison and selection difficult. The paper unifies the equivalences by induced lumpability, maps their relationships and compositionality, and identifies how their taxonomy varies in three special cases.

  • Problem

    PEPA stochastic bisimilarities are defined across scattered sources with inconsistent names, making it difficult to compare them and choose an equivalence for an application.

    Source: §1 · p. 2

  • Method

    The paper uniformly names six strong and weak PEPA bisimilarities by their induced ordinary, exact, or strict lumping, then analyzes their taxonomy, special cases, and congruence properties.

    Source: §1 · pp. 2–3

  • Results

    The paper establishes all and only the inclusions among the six bisimilarities, examines three special-case taxonomies, and finds all six congruent for cooperation and hiding but some not for prefix or choice.

    Source: §1 · p. 3, §7 · p. 38

  • Takeaways & Limitations

    The taxonomy and compositionality results provide a reference for selecting the coarsest equivalence adequate for an application's properties.

    Source: §1 · p. 3

    Even over time-reversible CTMCs, the bisimilarities generally remain distinct because they observe transition activity types while reversibility constrains cumulative rates.

    Source: §5.1 · p. 22

Abstract

from arXiv · show

We study the relationships among the stochastic bisimulation-style equivalences over PEPA - Performance Evaluation Process Algebra definable according to the well known notions of lumpability for the continuous-time Markov chains (CTMCs) underlying process terms. Lumpability is a central tool in the analysis of a CTMC, because it results in aggregations of the state space enjoying properties that are useful for efficiently computing the state probability distribution of the original chain. At the level of process terms, various stochastic bisimilarities accounting for activity types and cumulative rates can be defined over PEPA, which induce different kinds of lumping. Since the formalisations of some of them are scattered across the literature, where they appear under different, and sometimes clashing, names, we collect them within a single, uniform framework, renaming each bisimilarity in a consistent way after the kind of lumping it induces. We present strong and weak variants of what we call ordinary, exact, and strict bisimilarities and show that they respectively induce ordinary, exact, and strict lumpings. We then organise the six bisimilarities into a taxonomy establishing all and only the inclusions holding among them. We also analyse how the taxonomy changes in three special cases: process terms whose underlying CTMCs are time reversible, process terms with no activities of unobservable types, and process terms with no recursion. The paper concludes by investigating the compositionality properties of the six bisimilarities. Some of them are not congruences with respect to the prefix and/or choice operators of PEPA. In that case we single out either a set of process terms over which congruence with respect to those operators is achieved, or the coarsest congruence with respect to them that is contained in the considered bisimilarity.

1. Introduction

The paper brings scattered PEPA stochastic bisimilarities into a common framework organized by the kinds of CTMC lumping they induce. It maps their inclusions, special-case behavior, and compositionality properties to help compare the equivalences.

1. Introduction

  • The paper collects ordinary, exact, and strict lumpability with six strong and weak PEPA bisimilarities, naming each after the lumping it induces.The six are strong and weak ordinary, exact, and strict bisimilarities.Source: §1 · pp. 2–3
  • The taxonomy establishes all and only the inclusions among the six bisimilarities, including several strict inclusions and pairwise incomparabilities.It also examines how the taxonomy changes for time-reversible CTMCs, terms without unobservable activities, and terms without recursion.Source: §1 · p. 3
  • All six bisimilarities are congruences for cooperation and hiding, while some fail congruence for prefix or choice.For those cases, the paper identifies term sets where congruence holds or the coarsest contained congruence.Source: §1 · p. 3

Related Work.

  • No prior work had organized PEPA stochastic bisimilarities into a single spectrum according to the lumpings they induce.Earlier research studied behavioural-equivalence taxonomies and CTMC lumpability, while definitions and names for PEPA equivalences remained dispersed.Source: §1 · p. 2, Related Work · p. 3

Structure of the Paper.

  • The paper proceeds from CTMC lumpability and PEPA semantics to the six bisimilarities, their taxonomy, special cases, and compositionality.It concludes with future work.Source: Structure of the Paper · p. 4

2. Continuous-Time Markov Chains

This section establishes CTMC terminology and reviews ordinary, exact, and strict lumpability, including their relationship to time reversibility. It also describes how strict and exact lumpability behave under reversal for stationary and reversible CTMCs, and notes that ordinary lumpability need not become exact under reversal.

2.1. CTMC Terminology.

  • Lumpability aggregates equivalent CTMC states into macro-states, and ordinary, exact, and strict lumpability constrain outgoing, incoming, and both flows, respectively.Reversing time swaps incoming and outgoing flows, underpinning the connection between lumpability and reversibility.Source: §2.1 · p. 5

2.2. Ordinary Lumpability.

  • Ordinary lumpability requires states in each class to have equal cumulative rates to every other class, enabling an aggregate CTMC that preserves the original process’s analysis.The condition is necessary and sufficient for the aggregate process to remain a CTMC for every initial distribution.Source: §2.2 · pp. 5–6, §2.1 · p. 5

2.3. Exact Lumpability.

  • Exact lumpability requires equal cumulative rates into each state of a class from every class, including its own, and in an ergodic chain makes equivalent states equiprobable at steady state.Unlike ordinary lumpability, exact lumpability supports recovering the original steady-state probabilities from the lumped chain by local equidistribution.Source: §2.3 · p. 7

2.4. Strict Lumpability.

  • Strict lumpability requires both outgoing- and incoming-flow conditions, and the example admits no non-trivial strict lumping.In the example, the only strict lumping is the partition induced by the identity relation.Source: §2.4 · p. 8

2.5. Time Reversibility.

  • A CTMC is time reversible when its stationary process has the same joint distributions when observed forward or backward in time.Detailed balance characterizes reversibility using the equilibrium distribution; Kolmogorov’s criterion provides an alternative that does not require knowing that distribution.Source: §2.5 · pp. 9–10

2.6. Relationship between Lumpability and Reversibility.

  • For a stationary CTMC, exact lumpability of the forward chain implies ordinary lumpability of its time-reversed chain.Exact lumpability makes equivalent states equiprobable, so reversed rates translate the forward chain’s incoming-flow condition into an outgoing-flow condition.Source: §2.6 · p. 10
  • Ordinary lumpability for a CTMC does not in general imply exact lumpability for its reversed process.Source: §2.6 · p. 10
  • For a stationary CTMC, an equivalence is a strict lumpability exactly when it is a strict lumpability for the reversed process.Source: §2.6 · p. 10
  • If an equivalence is a strict lumpability for a stationary CTMC, both its forward and reversed aggregate processes satisfy the Markov property.Source: §2.6 · p. 10
  • For a reversible CTMC, an equivalence is a strict lumpability exactly when it is an exact lumpability.Source: §2.6 · p. 10

3. Performance Evaluation Process Algebra

This section introduces PEPA as a stochastic process algebra and explains how its syntax and operational semantics yield an underlying CTMC.

3.1. Syntax of PEPA.

  • PEPA combines activities and components in a stochastic process calculus used to calculate performance measures and prove functional properties.Activities carry a type and a rate; τ denotes unobservable activities, and rates may be positive reals or unspecified.Source: §3.1 · p. 11
  • PEPA's operators construct component behaviour: choice races activities, cooperation combines components, and hiding changes selected activity types to τ.In cooperation, components synchronize on shared types and act independently on types outside the cooperation set.Source: §3.1 · pp. 11–12

3.2. Operational Semantics.

  • Operational rules generate each component's derivation graph, where transition multiplicities matter and guardedness ensures finitely many outgoing transitions per state.The derivative set is finite when recursive constant definitions contain no cooperation or hiding.Source: §3.2 · p. 12

3.3. Underlying Stochastic Process.

  • For finite, performance-closed components, behaviour over time forms a CTMC whose transition rate between states sums the rates of transitions connecting them.Performance-closed components have no transitions labelled with unspecified rates.Source: §3.3 · p. 13

4. Lumpability-Driven Bisimilarities over PEPA

The section defines six strong and weak PEPA bisimilarities named for the ordinary, exact, or strict lumpings they induce. Strong variants treat τ like other activities; weak variants give τ special treatment.

4. Lumpability-Driven Bisimilarities over PEPA

  • Each of the six bisimilarities is defined as the union of all bisimulations of its kind; the weak variants distinguish τ by giving it special treatment.The strong variants handle τ like all other activities.Source: §4 · p. 14

4.1. Ordinary Bisimilarities.

  • Strong and weak ordinary bisimilarities induce ordinary lumpings; weak ordinary bisimilarity is coarser because it abstracts from τ-activities within an equivalence class.Strong ordinary bisimilarity also compares cumulative conditional transition rates toward the same class, unlike ordinary lumpability.Source: §4.1 · pp. 14–15

4.2. From Outgoing to Incoming Cumulative Rates.

  • Exact bisimilarities constrain incoming cumulative rates, restricted to components reachable from the process, to avoid triviality from unreachable components.The strong and weak exact variants induce exact lumpings on performance-closed, self-loop-free components; the weak variant relaxes constraints on internal τ flows while preserving steady-state equiprobability within classes.Source: §4.3 · pp. 16–17, §4.2 · p. 16

4.3. Exact Bisimilarities.

  • The strong and weak exact variants induce exact lumpings for performance-closed, self-loop-free components.Strong exact bisimilarity permits recovery of the original steady-state probability distribution from the aggregate chain under this scope; weak exact bisimilarity relaxes internal τ-flow constraints while preserving within-class steady-state equiprobability.Source: §4.3 · pp. 16–17

4.4. Strict Bisimilarities.

  • Strict bisimilarities require both ordinary outgoing-flow and exact incoming-flow conditions, and their strong and weak variants induce strict lumpings.The stated results apply to performance-closed, self-loop-free components.Source: §4.4 · p. 18

5. Taxonomy

The section establishes the inclusion taxonomy of six stochastic bisimilarities over PEPA and examines how it changes under time reversibility, absence of τ-activities, and absence of recursion. It also presents witness components and examples distinguishing equivalences, including ordinary from exact bisimulation in the non-recursive case.

5.1. Taxonomy over C.

  • Weak ordinary, exact, and strict bisimilarities can relate components separated by a repeatable τ-loop, whereas none of the corresponding strong bisimilarities can.Unlike classical τ-abstraction laws, these weak bisimilarities do not equate a sequence of timed τ-activities with one τ-activity of the same average duration.Source: §5.1 · p. 19
  • Over C, the only strict inclusions are ∼s⊂∼o⊂≈o, ∼s⊂∼e⊂≈e, ≈s⊂≈o, ≈s⊂≈e, and ∼s⊂≈s; no other pairwise inclusion holds.The taxonomy also makes ∼o, ∼e, and ≈s pairwise incomparable, as well as ≈o and ≈e.Source: §5.1 · pp. 20–21
  • For time-reversible CTMCs, exact and strict bisimilarities induce the same lumping, but the bisimilarities themselves can remain distinct.When all activities share one action type, the equivalences themselves coincide under time reversibility: ∼e = ∼s and ≈e = ≈s.Source: §5.1 · pp. 21–23

5.2. Taxonomies over Cnτ and Cnr.

  • Without τ-activities, each strong bisimilarity coincides with its corresponding weak version.The τ-related conditions of the weak definitions are vacuously satisfied in this case.Source: §5.2 · p. 23
  • Without recursion, weak ordinary bisimilarity can abstract a τ-tail that weak exact and strict bisimilarities cannot abstract under the same partition.Weak ordinary bisimilarity is more restrictive than classical τ-abstracting equivalences, and ordinary and exact bisimilarities are no longer incomparable without recursion; weak exact and strict bisimilarity relates (τ, r1) . 0 and (τ, r2) . 0 only when r1 = r2.Source: §5.2 · pp. 23–24
  • P3 and P4 are strongly ordinary-, exact-, and strict-bisimilar despite having different transition structures.Each has cumulative α rate 2 · r to a class containing only terminal states, where no further class can be reached.Source: §5.2 · p. 24
  • P5 and P6 are strongly exact-bisimilar but not strongly ordinary-bisimilar when their second action types or rates differ.They share the same initial α exit rate, but ordinary bisimulation distinguishes their different subsequent transitions.Source: §5.2 · pp. 24–25
  • For non-recursive terms, exact bisimilarity requires equal total exit rates for each action type, while strict bisimilarity depends only on its outgoing condition.Every class of derivatives of a term has zero cumulative rate back to that term, since its derivation graph is acyclic.Source: §5.2 · p. 25
  • Over Cnr, strong strict and strong ordinary bisimilarity coincide, as do weak strict and weak ordinary; weak ordinary and weak exact are incomparable.The remaining relationships are ∼o ⊂ ∼e, ≈s ⊂ ≈o, ≈s ⊂ ≈e, ∼o ⊂ ≈o, and ∼e = ≈e.Source: §5.2 · p. 25

6. Compositionality Properties

This section examines compositional reasoning and state-space minimization for the six bisimilarities, characterizing when PEPA prefix and choice preserve them, including cases requiring recursion-free terms. It also identifies rooted weak ordinary bisimilarity as the coarsest choice congruence contained in weak ordinary bisimilarity.

6.1. Compositionality of Strong Bisimilarities.

  • Strong ordinary bisimilarity is a congruence for all PEPA operators, a property proved in.The theorem covers prefix, choice, cooperation, and hiding.Source: §6.1 · p. 26
  • Strong exact and strong strict bisimilarity are congruences for PEPA operators other than prefix and choice.Their cooperation and hiding congruence results are stated in Theorems 6.2 and 6.3.Source: §6.1 · pp. 26–27
  • For recursive components, strong strict bisimilarity can fail under prefix and choice when added contexts change incoming-transition structure.The examples show previously equivalent components distinguished after prefixing or choice; strong exact bisimilarity can also fail under these operators.Source: §6.1 · pp. 28–29
  • Strong exact bisimilarity can fail under prefix and choice for recursive components, as the added terms may have different incoming transitions.The examples also show cases where exact-equivalent components remain equivalent after particular prefix or choice additions, so the failures are not universal for every context.Source: §6.1 · pp. 29–30
  • Over components without recursion, strong exact and strong strict bisimilarity are congruences for prefix and choice.The results establish preservation under both prefixing and adding a choice component on either side.Source: §6.1 · pp. 30–31

6.2. Compositionality of Weak Bisimilarities.

  • Weak ordinary bisimilarity is a congruence for PEPA operators other than choice, including prefix, cooperation, and hiding.The choice failure is addressed with a rooted variant that matches the components’ first activities, including τ activities under the stated condition.Source: §6.2 · p. 32
  • Rooted weak ordinary bisimilarity is the coarsest congruence with respect to choice contained in weak ordinary bisimilarity.P1 ≈ro P2 holds exactly when P1 + P ≈o P2 + P for every P; the rooted variant requires precise matching of first activities, including τ when the reached ≈o-class contains both components.Source: §6.2 · p. 33
  • Weak exact and strict bisimilarities are congruences for PEPA operators other than prefix and choice; restricting to components without recursion permits compositionality for those two operators.For weak exact bisimilarity, the stated no-recursion result covers prefix and both placements of choice.Source: §6.2 · pp. 34, 36
  • For recursion-free components, the proof constructs weak exact bisimulations that extend related pairs through prefixing and choice.For choice, it constructs extensions for both Q1 + Q and Q + Q1; the no-recursion condition is used in the rate arguments.Source: §6.2 · pp. 36–37
  • Weak strict bisimilarity is preserved by prefixing and by adding the same recursion-free process on either side of a choice.Theorem 6.16 states that if P1 ≈s P2 in Cnr, then a . P1 ≈s a . P2 and both P1 + P ≈s P2 + P and P + P1 ≈s P + P2 hold for every P in Cnr.Source: §6.2 · p. 37

7. Conclusion

The paper unifies six PEPA bisimilarities by induced lumping, maps their inclusions and special-case changes, and establishes their compositionality profile. It also identifies future axiomatization and noninterference directions.

7. Conclusion

  • The six strong and weak bisimilarities induce ordinary, exact, and strict lumpings and are organised by all and only their valid inclusions.The taxonomy is also examined for reversible CTMCs, terms without τ-activities, and terms without recursion.Source: §7 · p. 38
  • All six bisimilarities are congruences for cooperation and hiding, while some fail congruence for prefix or choice.For those cases, the paper identifies either a term set restoring congruence or the coarsest contained congruence.Source: §7 · p. 38
  • Future theoretical work includes sound and complete axiomatizations for the six bisimilarities.The paper notes that laws are already known for strong ordinary bisimilarity over PEPA and for the three strong bisimilarities over a reversible stochastic process algebra.Source: §7 · p. 38
  • Weak stochastic equivalences support noninterference properties that cover timing covert channels as well as functional information flows.The security scheme compares behaviour in isolation with behaviour while cooperating with an arbitrary high-level attacker.Source: §7 · p. 38
  • PSNI uses weak ordinary bisimilarity and EPSNI uses weak exact bisimilarity; strict variants have not been used for quantitative noninterference.Source: §7 · pp. 38–39
  • Future work could test how the bisimilarity taxonomy transfers to noninterference properties and examine strict bisimilarities for reversible stochastic systems.The coincidence of strict and exact lumpabilities over reversible CTMCs motivates strict variants as candidates in that setting.Source: §7 · p. 39
Loading 2609.11893v1…