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, HISC level-wise synthesis, as well as flat (treats HISC project as if it was a flat project) nonblocking and controllability checks.

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

The BDDsd algorithms can be accessed from the BDD Tools menu of a flat project 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. This restriction does not apply if you are only doing a nonblocking or untimed controllabilty check.

DESpot does not currently allow one to directly specify which events are forcible in a timed DES. Instead it uses the sampled-data supervisory control assumption that the set of forcible events is equal to the set of prohibitable (controllable non-tick) events.

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   |   Distributed Tools »