BDD Tools


BDD Tools perform most of the same checks as found in Tools, however the algorithms used benefit from the use of binary decision diagrams (BDD), where as the regular Tools use automata-based algorithms (i.e. algorithms that use explicit lists of states and transitions). These tools use the BDD package BuDDy which can be found at http://sourceforge.net/projects/buddy/ and includes documentation for the package.

BDDhisc Algorithms

The BDDhisc algorithms can be accessed from the BDD Tools menu of an HPE window. These algorithms include all the standard HISC checks as well as HISC level-wise synthesis. Algorithms for flat nonblocking and controllability checks have not yet been integrated. To check these properties for a non HISC project, the user could create a dummy high-level and interface and then populate the low-level with the plants and supervisors of the flat system. They can then do a subsystem LD nonblocking and controllability check for the low-level.

The BDDhisc algorithms now support verification of HISC systems that include low data events. They also now contain experimental level-wise synthesis algorithms for HISC systems containing LD events.

When the user selects to do an HISC level-wise synthesis, a dialogue pops up to allow the user to select between different output file formats. If the user selects "DES," the synthesis result will be saved in a "*_sup.txt" text file, one per subsystem. This can produce extremely large files for large examples.

If the user selects "BDD," the synthesis results will be saved in "*.bdd" and "*.dot" files, one for each controllable event. The "*.bdd" is the output format used by BuDDy, and "*.dot" is the file format used by the Graphviz program (http://www.graphviz.org/). They represent the BDD predicate which evaluates to true only for those states of the indicated subsystem at which the event should be enabled. Each event is only given in terms of a single component, as the enablement of an event in HISC is uniquely determined by a single subsystem and relevant interfaces. For more information, see:

Raoguang Song and Ryan J. Leduc, "Symbolic synthesis and verification of hierarchical interface-based supervisory control," Proc. of 8th International Workshop on Discrete Event Systems, pages 419-426, Ann Arbor, USA, July, 2006.

BDDsd Algorithms - not yet integrated

The BDDsd algorithms can be accessed from the BDD Tools menu of a flat window. They include nonblocking, untimed controllability, SD controllability, proper time behavior, S-singular prohibitable behavior, plant completeness, and activity-loop-free checks. Currently, BDDsd requires that each DES in the project must contain a controllable event called tick, with alias t. For more information, see:

Ryan Leduc and Yu Wang, "Sampled-data supervisory control," in Proc. 10th International Workshop on Discrete Event Systems (WODES'10), pages 353-359, Berlin, Germany, Aug 2010.


« Export to BDDhisc   |   Save Project »