Crate merc_reduction

Expand description

§Overview

This crate provides various algorithms for reducing labeled transition systems (LTS) modulo various equivalence relations, see merc_lts. These algorithms can also be used to compare LTS for equivalence. For now the equivalences that are supported are strong bisimulation, branching bisimulation, and weak bisimulation.

§Usage

The main functionalities of this crate of provided by the reduce_lts and compare_lts functions, which can be used to reduce and compare LTS using all available equivalence relations. These functions, and many functions in this crate, accept the inputs by value, since these reductions often need to preprocess the given LTS (.e.g,)

use merc_lts::LTS;
use merc_lts::read_aut;
use merc_reduction::reduce_lts;
use merc_reduction::Equivalence;
use merc_utilities::Timing;

let lts = read_aut(b"des(0, 6, 7)
(0, a, 1)
(0, a, 2)
(1, b, 3)
(1, c, 4)
(2, b, 5)
(2, c, 6)
" as &[u8], Vec::new()).unwrap();

let mut timings = Timing::new();
assert_eq!(lts.num_of_states(), 7); // The original has 6 states
let reduced = reduce_lts(lts, Equivalence::StrongBisim, &mut timings);
assert_eq!(reduced.num_of_states(), 3);

§Authors

This crate was developed by Jan J. Martens and Maurice Laveaux. The main signature based branching bisimulation algorithm is described in the paper:

“Faster Signature Refinement for Branching Bisimilarity Minimization”. Jan J. Martens, Maurice Laveaux. TACAS 2026.

§Safety

This crate contains minimal unsafe code, but modules that don’t use unsafe code are clearly marked as such.

§Minimum Supported Rust Version

We do not maintain an official minimum supported rust version (MSRV), and it may be upgraded at any time when necessary.

§License

All MERC crates are licensed under the BSL-1.0 license. See the LICENSE file in the repository root for more information.

Structs§

Block: A block stores a subset of the elements in a partition.
BlockIter
BlockPartition: A partition that explicitly stores a list of blocks and their indexing into the list of elements.
BlockPartitionBuilder
BlockTag: A zero sized tag for the block.
IndexedPartition: Defines a partition based on an explicit indexing of elements to their block number.
Signature: The type of a signature. We use sorted vectors to avoid the overhead of hash sets that might have unused values.
SimpleBlock: A super::Block that stores a subset of the elements in a partition, but with individual stable elements.
SimpleBlockIter
SimpleBlockPartition: A partition that explicitly stores a list of blocks and their indexing into the list of elements. Similar to super::BlockPartition but without taking the stability of individual elements into account.

Enums§

Equivalence

Traits§

Partition: A trait for partition refinement algorithms that expose the block number for every state. Can be used to compute the quotient labelled transition system.

Functions§

branching_bisim_signature: Returns the branching bisimulation signature for branching bisimulation.
branching_bisim_signature_inductive: The inductive version of branching_bisim_signature_sorted. Assumes that the input LTS has no tau-cycles, and is topologically sorted.
branching_bisim_signature_sorted: The same as branching_bisim_signature, but assuming that the input LTS is topological sorted, and contains no tau-cycles.
branching_bisim_sigref: Computes a branching bisimulation partitioning using signature refinement
branching_bisim_sigref_naive: Computes a branching bisimulation partitioning using signature refinement without dirty blocks.
combine_partition: Combines two partitions into a new partition.
compare_lts
has_tau_loop: Returns true iff the labelled transition system has tau-loops.
is_tau_hat: Returns true if the label is the special tau_hat label for the given LTS.
is_valid_refinement: Returns true iff the given partition is a strong bisimulation partition
preprocess_branching: Perform the preprocessing necessary for branching bisimulation with the sorted signature see branching_bisim_signature_sorted.
quotient_lts_block: Optimised implementation for block partitions.
quotient_lts_naive: Returns a new LTS based on the given partition.
reduce_lts: Reduces the given LTS modulo the given equivalence using signature refinement
reorder_partition: Reorders the blocks of the given partition according to the given permutation.
scc_decomposition: Computes the strongly connected component partitioning of the given LTS.
sort_topological: Returns a topological ordering of the states of the given LTS.
strong_bisim_signature: Returns the signature for strong bisimulation.
strong_bisim_sigref: Computes a strong bisimulation partitioning using signature refinement
strong_bisim_sigref_naive: Computes a strong bisimulation partitioning using signature refinement
tau_scc_decomposition: Computes the strongly connected tau component partitioning of the given LTS.
weak_bisim_signature_sorted: Computes the weak bisimulation signature.
weak_bisim_signature_sorted_taus: This computes only tau signatures.
weak_bisim_sigref_naive: Computes a branching bisimulation partitioning using signature refinement without dirty blocks.
weak_bisimulation: Apply weak bisimulation reduction

Type Aliases§

BlockIndex: The index for blocks.
SignatureBuilder: The builder used to construct the signature.