In: Proc. IEEE Int. Conf. on Systems, Man, and Cybernetics (SMC'98), 11-14 October 1998, San Diego, CA, pages 722-727. 1998.
Abstract: Binary decision diagrams (BBDs) have been used to represent relations, as well as operations for modeling, analysis and synthesis of DEDS. To utilize the structure of integers and arithmetic operations effectively. With tools for efficient relational representation, it is possible to improve scalability of DEDS computations, as illustrated by the modeling and analysis of the landing gear controller of the Swedish fighter aircraft JAS 39 Grippen. A relational model, represented both by a BDD and an IDD, is automatically generated from a 1200 lines of Pascal implementation, which contains 105 binary variables of which 26 are state variables. Function specifications expressed with temporal algebra are verified using tools for dynamic analysis, which are also used to computer the relation representing the set of all reachable states in the model. The landing gear controller serves as a benchmark test of BDDs and IDDs. The IDDs reduced the computation time by 50 percent.
Keywords: binary decision diagrams, discrete-event systems, integer decision diagrams, reachability analysis, symbolic tools, temporal algebras.