Biodivine BDD-based SCC detection algorithms

BDD-based algorithms for symbolic strongly connected component (SCC) detection in Boolean networks.

This crate provides efficient symbolic algorithms for computing SCCs and reachability in asynchronous Boolean networks, using Binary Decision Diagrams (BDDs) as the underlying representation. It builds on top of biodivine-lib-param-bn for Boolean network modeling and symbolic graph operations.

Features

• Symbolic SCC detection: Find all non-trivial strongly connected components using forward-backward or chain-based algorithms
• Symbolic attractor detection: Find all attractors using Xie-Beerel symbolic algorithm with interleaved transition guided reduction.
• Reachability analysis: Compute forward and backward reachable sets using BFS or saturation-based strategies
• Trimming: Remove trivial sink/source states before SCC computation
• Long-lived filtering: Optionally filter SCCs that can be escaped via a single variable update
• Cancellable computations: All algorithms support cooperative cancellation via the cancel-this crate

Quick Start

Add the dependency to your Cargo.toml:

[dependencies]
biodivine-algo-bdd-scc = "0.1"
biodivine-lib-param-bn = "0.6"

Basic SCC Enumeration

use biodivine_algo_bdd_scc::scc::{FwdBwdScc, SccConfig};
use biodivine_lib_param_bn::BooleanNetwork;
use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph;
use computation_process::Stateful;

fn example() {
    // Load a Boolean network from a file
    let bn = BooleanNetwork::try_from_file("model.aeon").unwrap();
    let graph = SymbolicAsyncGraph::new(&bn).unwrap();
  
    // Create an SCC configuration with default settings
    let config = SccConfig::new(graph.clone());
  
    // Enumerate all non-trivial SCCs
    for scc in FwdBwdScc::configure(config, &graph) {
      let scc = scc.unwrap();
      println!("Found SCC with {} states", scc.exact_cardinality());
    } 
}

Reachability Analysis

use biodivine_algo_bdd_scc::reachability::ForwardReachability;
use biodivine_lib_param_bn::BooleanNetwork;
use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph;
use computation_process::Algorithm;

fn example() {
    let bn = BooleanNetwork::try_from_file("model.aeon").unwrap();
    let graph = SymbolicAsyncGraph::new(&bn).unwrap();
  
    // Compute all states reachable from a given initial set
    let initial = graph.mk_unit_colored_vertices().pick_vertex();
    let reachable = ForwardReachability::run(&graph, initial).unwrap();
  
    println!("Reachable states: {}", reachable.exact_cardinality()); 
}

Available Algorithms

SCC Detection

Reachability

Trimming

Attractors

The crate also provides symbolic attractor enumeration algorithms in the [attractor] module, plus a small CLI (biodivine_attractor) behind the build-binary feature.

Command-Line Tool

The crate includes binaries for SCC and attractor enumeration. Build them with:

cargo build --release --features build-binary

Usage:

# Enumerate all SCCs using the default forward-backward algorithm
./target/release/biodivine_scc model.aeon

# Use the chain algorithm with verbose logging
./target/release/biodivine_scc model.aeon --algorithm=chain -v

# Enumerate only long-lived SCCs (cannot be escaped by one variable update)
./target/release/biodivine_scc model.aeon --long-lived

# Enumerate only the first 5 SCCs
./target/release/biodivine_scc model.aeon --count=5

# Enumerate attractors using ITGR + Xie-Beerel (default)
./target/release/biodivine_attractor model.aeon

# Enumerate attractors using only Xie-Beerel
./target/release/biodivine_attractor model.aeon --algorithm=xie-beerel

Testing

Run the test suite:

# Basic tests (can take a few minutes)
cargo test

License

This project is licensed under the MIT License.

References

The general idea of SCC decomposition for colored graphs (i.e., with logical parameters) was presented here:

Beneš, Nikola, Luboš Brim, Samuel Pastva, and David Šafránek. "Symbolic coloured SCC decomposition." In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 64-83. Cham: Springer International Publishing, 2021. DOI

Furthermore, the attractor detection algorithms are adapter from this paper:

Beneš, Nikola, Luboš Brim, Samuel Pastva, and David Šafránek. "Computing bottom SCCs symbolically using transition guided reduction." In International Conference on Computer Aided Verification, pp. 505-528. Cham: Springer International Publishing, 2021. DOI

The chain algorithm is also loosely based on:

Larsen, Casper Abild, Simon Meldahl Schmidt, Jesper Steensgaard, Anna Blume Jakobsen, Jaco van de Pol, and Andreas Pavlogiannis. "A truly symbolic linear-time algorithm for SCC decomposition." In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 353-371. Cham: Springer Nature Switzerland, 2023. DOI