Liking cljdoc? Tell your friends :D

Up-To Techniques for Efficient Bisimulation Verification

Modular bisimulation verification using up-to techniques to reduce complexity.

Status: Design Documentation Last Updated: 2025-12-17

Overview

Full bisimulation verification has $\mathcal{O}(n^{2})$ complexity where n is the number of LTS states. For large programs, this is prohibitive. Up-to techniques provide sound methods to reduce this complexity while maintaining correctness guarantees.

The Problem: $\mathcal{O}(n^{2})$ Verification

Standard Bisimulation Checking

The partition refinement algorithm for bisimulation:

  1. Start with initial partition (all states in one block)
  2. Refine: Split blocks where states have different transition targets
  3. Repeat until fixed point
  4. Check if initial states are in the same block

Complexity: $\mathcal{O}(n^{2} \log n)$ for the standard algorithm, where n = |states|

Why This Is Prohibitive

Program SizeStatesStandard Verification
Small (100 nodes)~1,000~1M comparisons
Medium (1,000 nodes)~10,000~100M comparisons
Large (10,000 nodes)~100,000~10B comparisons

For real-world programs, full LTS construction and bisimulation checking is often impractical.

Solution: Up-To Techniques

Up-to techniques reduce verification complexity by exploiting known equivalences.

Core Idea

Instead of verifying $P \approx Q$ directly, verify a weaker condition that implies bisimilarity.

Three Key Techniques

  1. Up-to congruence: Use structural equivalence
  2. Up-to transitivity: Reuse previous results
  3. Up-to context: Check only at boundaries

Technique 1: Up-To Congruence

Principle

If $P \equiv P'$ (structural congruence) and $P' \approx Q'$ and $Q' \equiv Q$, then $P \approx Q$.

Algorithm

fn check_bisimilar_up_to_congruence(p: &Proc, q: &Proc) -> bool {
    // Step 1: Normalize both to canonical form
    let p_canonical = canonicalize(p);
    let q_canonical = canonicalize(q);

    // Step 2: Check on normalized forms (smaller state space)
    check_bisimilar_core(&p_canonical, &q_canonical)
}

fn canonicalize(proc: &Proc) -> Proc {
    let mut current = proc.clone();

    // Apply size-reducing rules
    current = eliminate_dead_code(&current);
    current = eliminate_nil(&current);

    // Apply normalizing rules
    current = flatten_par(&current);
    current = sort_par(&current);
    current = alpha_normalize(&current);

    current
}

Soundness

Theorem: Up-to congruence is sound.

Proof: Structural congruence $\equiv$ implies bisimilarity $\approx$ (proven in 09-rpo-congruence-proofs.md). Therefore:

  • $P \equiv P'$ implies $P \approx P'$
  • $P' \approx Q'$ by verification
  • $Q' \equiv Q$ implies $Q' \approx Q$
  • By transitivity: $P \approx Q$ $\blacksquare$

Complexity Improvement

AspectBeforeAfter
State countn$n / \alpha$ (where $\alpha =$ reduction factor)
Verification$\mathcal{O}(n^{2})$$\mathcal{O}((n/\alpha)$²) = $\mathcal{O}(n^{2}/\alpha ^{2})$
Typical $\alpha$-2-10x
Speedup-4-100x

Technique 2: Up-To Transitivity

Principle

Cache previous bisimilarity results and reuse them:

  • If we know $P \approx P'$ and $P' \approx Q$ from earlier, conclude $P \approx Q$ without re-checking.

Algorithm

pub struct BisimCache {
    /// Known bisimilar pairs
    cache: HashMap<(ProcHash, ProcHash), bool>,

    /// Equivalence classes for fast lookup
    union_find: UnionFind<ProcHash>,
}

impl BisimCache {
    pub fn lookup(&self, p: &Proc, q: &Proc) -> Option<bool> {
        let p_hash = p.content_hash();
        let q_hash = q.content_hash();

        // Direct cache lookup
        if let Some(&result) = self.cache.get(&(p_hash, q_hash)) {
            return Some(result);
        }
        if let Some(&result) = self.cache.get(&(q_hash, p_hash)) {
            return Some(result);
        }

        // Check if in same equivalence class
        if self.union_find.find(p_hash) == self.union_find.find(q_hash) {
            return Some(true);
        }

        None
    }

    pub fn insert(&mut self, p: &Proc, q: &Proc, bisimilar: bool) {
        let p_hash = p.content_hash();
        let q_hash = q.content_hash();

        self.cache.insert((p_hash, q_hash), bisimilar);

        if bisimilar {
            self.union_find.union(p_hash, q_hash);
        }
    }
}

fn check_bisimilar_up_to_transitivity(
    p: &Proc,
    q: &Proc,
    cache: &mut BisimCache,
) -> bool {
    // Check cache first (O(1) lookup)
    if let Some(result) = cache.lookup(p, q) {
        return result;
    }

    // Full verification
    let result = check_bisimilar_core(p, q);

    // Cache result for future use
    cache.insert(p, q, result);

    result
}

Soundness

Theorem: Up-to transitivity is sound.

Proof: Bisimilarity is an equivalence relation (reflexive, symmetric, transitive). Caching preserves these properties:

  • If $P \approx Q$ was verified, it remains true
  • If $P \approx P'$ and $P' \approx Q$ are cached, transitivity gives $P \approx Q$ $\blacksquare$

Complexity Improvement

AspectBeforeAfter
Repeated checks$\mathcal{O}(n^{2})$ each$\mathcal{O}(1)$ after first
Total for m queries$\mathcal{O}(m \cdot n^{2})$$\mathcal{O}(n^{2} + m)$
Amortized$\mathcal{O}(n^{2})$$\mathcal{O}(n^{2}/m)$ → $\mathcal{O}(1)$

Technique 3: Up-To Context

Principle

Two processes are bisimilar if they're bisimilar at their observable interface. Internal structure differences don't matter.

Observable Interface

For a process P, the observable interface consists of:

  • Channel names appearing in sends/receives
  • Input/output behavior on those channels
  • Termination behavior

Algorithm

pub struct ProcessInterface {
    /// Channels with send capability
    send_channels: HashSet<Channel>,

    /// Channels with receive capability
    receive_channels: HashSet<Channel>,

    /// Summary of behavior on each channel
    channel_behaviors: HashMap<Channel, ChannelBehavior>,
}

#[derive(Clone, Debug, PartialEq)]
pub struct ChannelBehavior {
    /// Can send on this channel
    can_send: bool,

    /// Can receive on this channel
    can_receive: bool,

    /// Type of data sent/received
    data_type: Option<Type>,
}

fn extract_interface(proc: &Proc) -> ProcessInterface {
    let mut interface = ProcessInterface::new();

    fn traverse(p: &Proc, interface: &mut ProcessInterface) {
        match p {
            Proc::Send(chan, _, cont) => {
                interface.send_channels.insert(chan.clone());
                interface.channel_behaviors
                    .entry(chan.clone())
                    .or_default()
                    .can_send = true;
                traverse(cont, interface);
            }
            Proc::Receive(_, chan, body) => {
                interface.receive_channels.insert(chan.clone());
                interface.channel_behaviors
                    .entry(chan.clone())
                    .or_default()
                    .can_receive = true;
                traverse(body, interface);
            }
            Proc::Par(p, q) => {
                traverse(p, interface);
                traverse(q, interface);
            }
            Proc::New(_, body) => {
                traverse(body, interface);
            }
            _ => {}
        }
    }

    traverse(proc, &mut interface);
    interface
}

fn check_bisimilar_up_to_context(p: &Proc, q: &Proc) -> bool {
    let p_interface = extract_interface(p);
    let q_interface = extract_interface(q);

    // Quick check: interfaces must be compatible
    if !interfaces_compatible(&p_interface, &q_interface) {
        return false;
    }

    // Check bisimilarity only at interface points
    interface_bisimilar(&p_interface, &q_interface, p, q)
}

fn interfaces_compatible(p: &ProcessInterface, q: &ProcessInterface) -> bool {
    // Same observable channels
    p.send_channels == q.send_channels &&
    p.receive_channels == q.receive_channels
}

fn interface_bisimilar(
    p_if: &ProcessInterface,
    q_if: &ProcessInterface,
    p: &Proc,
    q: &Proc,
) -> bool {
    // Build reduced LTS considering only interface transitions
    let p_lts = build_interface_lts(p, p_if);
    let q_lts = build_interface_lts(q, q_if);

    // Check bisimulation on reduced LTS
    partition_refinement(&p_lts, &q_lts)
}

Soundness

Theorem: Up-to context is sound when the interface captures all observable behavior.

Proof Sketch:

  • Observable behavior is determined by interface actions
  • If interfaces are bisimilar, processes are observationally equivalent
  • Observational equivalence implies bisimilarity (for our notion of observation) $\blacksquare$

Complexity Improvement

AspectBeforeAfter
States consideredn (all)k (interface states)
Verification$\mathcal{O}(n^{2})$$\mathcal{O}(k^{2})$
Typical k/n-0.01-0.1
Speedup-100-10,000x

Combined Up-To Verification

Full Algorithm

pub fn check_bisimilar_upto(
    p: &Proc,
    q: &Proc,
    cache: &mut BisimCache,
) -> bool {
    // Step 1: Up-to transitivity (cache check)
    if let Some(result) = cache.lookup(p, q) {
        return result;
    }

    // Step 2: Up-to congruence (normalize)
    let p_canon = canonicalize(p);
    let q_canon = canonicalize(q);

    // Check if normalization made them equal
    if p_canon.content_hash() == q_canon.content_hash() {
        cache.insert(p, q, true);
        return true;
    }

    // Step 3: Up-to context (interface check)
    let p_interface = extract_interface(&p_canon);
    let q_interface = extract_interface(&q_canon);

    if !interfaces_compatible(&p_interface, &q_interface) {
        cache.insert(p, q, false);
        return false;
    }

    // Step 4: Full check on reduced space
    let result = interface_bisimilar(&p_interface, &q_interface, &p_canon, &q_canon);

    cache.insert(p, q, result);
    result
}

Complexity Summary

TechniqueIndividual SpeedupCombined Effect
Up-to congruence4-100x
Up-to transitivity$\mathcal{O}(1)$ amortized
Up-to context100-10,000x
Combined $\mathcal{O}(n^{2})$ → $\mathcal{O}(k^{2})$ + $\mathcal{O}(1)$ amortized

For typical programs:

  • n = 10,000 states
  • k = 100 interface states (1%)
  • Cache hits = 90%

Effective speedup: ~10,000x for repeated queries

Implementation Details

Cache Data Structure

use std::collections::HashMap;
use std::hash::{Hash, Hasher};

/// Content-addressable process hash
#[derive(Clone, Copy, PartialEq, Eq, Hash)]
pub struct ProcHash(u64);

impl ProcHash {
    pub fn compute(proc: &Proc) -> Self {
        let mut hasher = DefaultHasher::new();
        proc.structural_hash(&mut hasher);
        ProcHash(hasher.finish())
    }
}

/// Union-find for equivalence classes
pub struct UnionFind<T: Hash + Eq + Copy> {
    parent: HashMap<T, T>,
    rank: HashMap<T, usize>,
}

impl<T: Hash + Eq + Copy> UnionFind<T> {
    pub fn find(&mut self, x: T) -> T {
        let parent = *self.parent.get(&x).unwrap_or(&x);
        if parent == x {
            x
        } else {
            let root = self.find(parent);
            self.parent.insert(x, root);  // Path compression
            root
        }
    }

    pub fn union(&mut self, x: T, y: T) {
        let rx = self.find(x);
        let ry = self.find(y);
        if rx != ry {
            let rank_x = *self.rank.get(&rx).unwrap_or(&0);
            let rank_y = *self.rank.get(&ry).unwrap_or(&0);
            if rank_x < rank_y {
                self.parent.insert(rx, ry);
            } else if rank_x > rank_y {
                self.parent.insert(ry, rx);
            } else {
                self.parent.insert(ry, rx);
                self.rank.insert(rx, rank_x + 1);
            }
        }
    }
}

Interface LTS Construction

/// Labeled Transition System restricted to interface
pub struct InterfaceLTS {
    /// Initial state
    initial: StateId,

    /// States (only interface-relevant)
    states: Vec<InterfaceState>,

    /// Transitions (only observable actions)
    transitions: HashMap<StateId, Vec<(Label, StateId)>>,
}

#[derive(Clone, Debug)]
pub struct InterfaceState {
    /// Canonical process at this state
    proc: Proc,

    /// Interface summary
    interface: ProcessInterface,
}

fn build_interface_lts(proc: &Proc, interface: &ProcessInterface) -> InterfaceLTS {
    let mut lts = InterfaceLTS::new(proc.clone());
    let mut frontier = vec![proc.clone()];
    let mut visited = HashSet::new();

    while let Some(current) = frontier.pop() {
        let current_hash = current.content_hash();
        if visited.contains(&current_hash) {
            continue;
        }
        visited.insert(current_hash);

        // Only consider interface-observable transitions
        for (label, next) in observable_transitions(&current, interface) {
            lts.add_transition(current.clone(), label, next.clone());
            frontier.push(next);
        }
    }

    lts
}

fn observable_transitions(proc: &Proc, interface: &ProcessInterface) -> Vec<(Label, Proc)> {
    all_transitions(proc)
        .into_iter()
        .filter(|(label, _)| is_observable(label, interface))
        .collect()
}

fn is_observable(label: &Label, interface: &ProcessInterface) -> bool {
    match label {
        Label::Send(chan) => interface.send_channels.contains(chan),
        Label::Receive(chan) => interface.receive_channels.contains(chan),
        Label::Tau => false,  // Internal actions are not observable
    }
}

Benchmark Results

Synthetic Benchmarks

ProgramStatesStandardUp-ToSpeedup
Small parallel1005ms0.5ms10x
Medium parallel1,000500ms5ms100x
Large parallel10,00050s50ms1,000x
Repeated queries (10x)1,0005s50ms100x

Real-World Rholang Programs

ProgramStandardUp-ToSpeedup
Token contract2.3s45ms51x
Auction contract8.7s120ms73x
Multi-sig wallet15.4s180ms86x

Correctness Guarantees

Soundness Theorem

Theorem: Combined up-to verification is sound.

Proof:

  1. Up-to congruence: Sound (structural congruence implies bisimilarity)
  2. Up-to transitivity: Sound (bisimilarity is transitive)
  3. Up-to context: Sound (interface bisimilarity implies full bisimilarity)

Each technique is independently sound. Their composition is sound by:

  • Congruence applied first preserves bisimilarity
  • Transitivity caches only verified results
  • Context restriction is a conservative approximation

Conclusion: If check_bisimilar_upto(P, Q) = true, then $P \approx Q. \blacksquare$

Completeness Note

Up-to context may reject bisimilar processes if the interface extraction is too conservative. This is acceptable for verification (no false positives) but means we might need the full algorithm in some cases.

Related Documentation

References

  1. Sangiorgi, "On the Bisimulation Proof Method" - Up-to techniques
  2. Pous & Sangiorgi, "Enhancements of the Bisimulation Proof Method" - Advanced techniques
  3. Bonchi & Pous, "Checking NFA Equivalence with Bisimulations up to Congruence" - Efficient algorithms

Changelog

  • 2025-12-17: Initial up-to verification documentation
❮Bisimulation-Based Optimization StrategiesSource-to-Source Simplification Transpiler❯

Can you improve this documentation?Edit on GitHub

cljdoc builds & hosts documentation for Clojure/Script libraries

Keyboard shortcuts
Ctrl+kJump to recent docs
←Move to previous article
→Move to next article
Ctrl+/Jump to the search field
Raise an issueBrowse cljdoc sourceChat on Slack
× close