Application of OBDD Diagrams in Verification of Tabular Rule Systems

• Autorzy: Szwed P. , Ligęza A.
• Języki publikacji: EN

Abstrakty

EN

This paper examines the application of Ordered Binary Decision Diagrams (OBDD) to modelling and verification of quality properties of rule systems. The transformation of an intentional specification of a tabular rule system into OBDD data structures was proposed and techniąues of verification of such ąuality properties as completeness, determinism and redundancy of rules were described.

Słowa kluczowe

EN

binary decision diagrams; OBDD; tabular rule systems; verification

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Schedae Informaticae
• Rocznik: 2005
• Tom: Vol. 14
• Strony: 75--94
• Opis fizyczny: Bibliogr. 16 poz., rys.

Twórcy

autor

Szwed P.

• Institute of Automatics, AGH Uniuersity of Science and Technology, Mickiewicza 30, 30-059 Kraków, Poland

autor

Ligęza A.

• Institute of Automatics, AGH Uniuersity of Science and Technology, Mickiewicza 30, 30-059 Kraków, Poland

Bibliografia

• [1] Ligeza A.; Logical analysis of completeness of rule-based systems with dual resolution, in: Proceedings of EUROVAV-97 – 4th European Symposium on the Validation and Verification of Knowledge Based Systems, Leuven, Belgium, 1997, pp. 19–29.
• [2] Ligeza A.; Towards logical analysis of tabular rule-based systems, in: R.R. Wagner, (ed.); 9th International Workshop on Database and Expert Systems Applications, Vienna, Austria, 1998, pp. 30–35; extended version submitted to Journal of Intelligent Systems.
• [3] Bryant E.R.; Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys, September 1992, 24(3), 1992, pp. 293–318.
• [4] Bryant E.R.; Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, 8(35), 1986, pp. 677–691.
• [5] Andersen H.R.; An Introduction to Binary Decision Diagrams, Lecture Notes for 49285, Advanced Algorithms E97, October 1997, Department of Information Technology, Technical University of Denmark, http://www.it.dtu.dk/~hra/.
• [6] Meinel Ch., Theobald T.; Ordered Binary Decision Diagrams and Their Significance in Computer-Aided Design of VLSI Circuits, Universität Trier TU München, Technical Report 98-01. ftp://ftp.informatik.uni-trier.de/pub/Users-Root/reports.
• [7]Wegener I.; The Complexity of Boolean Functions, John Wiley & Sons and Teubner-Verlag, 1987.
• [8] Minato S.; Binary Decision Diagrams and Applications for VLSI CAD, Kluwer Academic Publishers, 1996.
• [9] Somenzi F.; CUDD: Colorado University Decision Diagram Package, 1996. ftp://vlsi.colorado.edu/pub/.
• [10] Koutsofios E., North S.C.; Drawing graphs with dot, Technical Report 910904-59113-08TM, AT&T Bell Laboratories, Murray Hill, NJ, September 1991.
• [11]Minato S.; Binary Decision Diagrams and Applications for VLSI CAD, Kluwer Academic Publishers, 1996.
• [12] McMillan K.L.; Symbolic Model Checking, Kluwer Academic Publishers, 1993.
• [13]Meinel Ch., Stangier Ch.; OBDD-based verification of communication protocols – methods for the verification of data link protocols, Technical Report 97-28, Universität Trier, 1997.
• [14]Coudert O., Berthet C., Madre J.C.; Verification of synchronous sequential machines using symbolic execution, in: Proc. Workshop on Automatic Verification Methods for Finite State Machines, volume 407 of Lecture Notes in Computer Science, Springer, 1989, pp. 365–373.
• [15] Wegener I., The Complexity of Boolean Functions, John Wiley & Sons and Teubner-Verlag, 1987.
• [16] Ligeza A.; Granular Algebra: Towards a Calculus of Semi-Partitions for Analysis, Manipulation and Verification of Tabular Systems, in: Proceedings of the Sixteenth European Meeting on Cybernetics and Systems Research, Vol. II, R. Trappl, (ed.), Austrian Society for Cybernetic Studies, Vienna, Austria, 2002, pp. 806–811.