BDD-based Symbolic Model Checking
The BDD (Binary Decision Diagram) module implements symbolic model checking for Boolean programs using Z3’s Boolean reasoning capabilities. This prover performs both forward and backward reachability analysis to verify safety properties.
Overview
BDD-based symbolic model checking is a technique that uses Binary Decision Diagrams to represent and manipulate Boolean functions efficiently. In EFMC, this is implemented using Z3’s Boolean reasoning capabilities rather than traditional BDD libraries.
Algorithm
The BDD prover implements two main approaches:
Forward Reachability Analysis: 1. Start with the initial states 2. Iteratively compute the image (successor states) using the transition relation 3. Continue until a fixpoint is reached or the maximum number of iterations is exceeded 4. Check if the computed reachable states satisfy the safety property
Backward Reachability Analysis: 1. Start with the negation of the safety property (bad states) 2. Iteratively compute the pre-image (predecessor states) using the transition relation 3. Continue until a fixpoint is reached or the maximum number of iterations is exceeded 4. Check if the initial states are contained in the computed bad states
Usage
The BDD prover can be used as follows:
from aria.efmc.engines.bdd import BDDProver
from aria.efmc.sts import TransitionSystem
# Create transition system
sts = TransitionSystem(...)
# Create BDD prover with forward analysis
prover = BDDProver(sts, use_forward=True, max_iterations=1000)
# Solve the verification problem
result = prover.solve()
if result.is_safe:
print("System is safe")
print(f"Invariant: {result.invariant}")
else:
print("System is unsafe or unknown")
Configuration Options
use_forward: Boolean flag to choose between forward (True) and backward (False) analysis
max_iterations: Maximum number of iterations for fixpoint computation (default: 1000)
Limitations
Currently uses Z3’s Boolean reasoning rather than dedicated BDD libraries
Future Improvements
Integration with dedicated BDD libraries (e.g., CUDD) for better performance