search

timbeurskens / rsbdd

A Reduced-order Binary Decision Diagram (RoBDD) SAT solver written in Rust
7 stars 2 forks source link

Model checking #33

Closed timbeurskens closed 2 years ago

timbeurskens commented 2 years ago

BDDs can be quite efficient in solving the model checking problem. By translating a kripke-structure to a boolean formula we can verify LTL/CTL properties on the model. The RsBDD DSL can be used as an intermediate output.

timbeurskens commented 2 years ago

https://www.cs.cmu.edu/~emc/15-820A/reading/lecture_1.pdf

timbeurskens commented 2 years ago

https://pure.tue.nl/ws/files/47012215/625651-1.pdf