Binary Decision Diagrams (BDDs) are used in symbolic model checking to represent set of states. Variations of decision diagrams have been introduced as extensions of BDDs. The first extension is removing the constraint of having only binary values, such as Multi-way Decision Diagrams (MDDs ) that can have variables with different domains. It is also possible to extend the range of the encoded function from boolean to integer or real ranges. Both multi-terminal and edge-valued decision diagrams extend this range.

Meddly is a C++ Library that supports both multi-terminal and edge-valued MDDs, and differ- ent reduction rules [2]. It is an ongoing project at Iowa State University (ISU), lead by Prof. Ciardo and Prof. Miner. Currently it supports quasi, fully, and identity-reduction rules. In my internship, I implemented two new reduction rules, constant and CIdentity reduction rules and some basic operations that are useful for model checking.

The concepts that were used during implementation are introduced in Chapter 1. In Chapter 2, the implemented reduction rules and algorithms of some operations are described. This chapter is specially written to guide other researchers to change/add a reduction rule in Meddly. Finally, possible conclusion and future works are presented.