B D D   M O D E L  C H E C K I NG  T O O L S home page

Index:

general description
download
contact

G e n e r a l   D e s c r i p t i o n

BDD-CTL and BDD-LTL are symbolic model checkers for safe (1-bounded) Petri nets. Both tools use a ZBDD (Zero-suppressed Binary Decision Diagram) library.

BDD-CTL is a symbolic implementation of the classical CTL model checking algorithm.

BDD-LTL was developed as a prototype tool by J. Spranger for demonstration and validation of the symbolic methods of his Ph.D. Thesis. Three LTL algorithms are implemented, see the thesis for more details:

• Backward cycle search is an adaptation of the classical LTL algorithm by E.A. Emerson and C.-L. Lei.
• Forward cycle search was created to overcome the following problem of the backward search: calculation of all possible predecessor markings can lead to the creation of too many non-reachable markings. So the algorithm was modified to work in the forward direction.
• Symbolic deep first search was introduced in the thesis as an advanced algorithm. Both backward and forward cycle search algorithms need the complete generation of the state space before model checking and have the quadratic complexity regarding the size of the state space. Symbolic deep first search is able to work on-the-fly and has a linear complexity in the size of the state space.

The tools are integrated in the Model-Checking Kit developed and maintained at the University of Stuttgart.

D o w n l o a d

Please read the Usage/Modification agreement

BDD-CTL

BDD-LTL

 C o n t a c t 

dsszmc(at)informatik(dot)tu-cottbus(dot)de

. . .  t h e  e n d  . . .