On the Influence of the State Encoding on OBDD-Representations of Finite State Machines

Christoph Meinel; Thorsten Theobald

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 33, Issue: 1, page 21-31
  • ISSN: 0988-3754

Abstract

top
Ordered binary decision diagrams are an important data structure for the representation of Boolean functions. Typically, the underlying variable ordering is used as an optimization parameter. When finite state machines are represented by OBDDs the state encoding can be used as an additional optimization parameter. In this paper, we analyze the influence of the state encoding on the OBDD-representations of counter-type finite state machines. In particular, we prove lower bounds, derive exact sizes for important encodings and construct a worst-case encoding which leads to exponential-size OBDDs.

How to cite

top

Meinel, Christoph, and Theobald, Thorsten. "On the Influence of the State Encoding on OBDD-Representations of Finite State Machines." RAIRO - Theoretical Informatics and Applications 33.1 (2010): 21-31. <http://eudml.org/doc/222070>.

@article{Meinel2010,
abstract = { Ordered binary decision diagrams are an important data structure for the representation of Boolean functions. Typically, the underlying variable ordering is used as an optimization parameter. When finite state machines are represented by OBDDs the state encoding can be used as an additional optimization parameter. In this paper, we analyze the influence of the state encoding on the OBDD-representations of counter-type finite state machines. In particular, we prove lower bounds, derive exact sizes for important encodings and construct a worst-case encoding which leads to exponential-size OBDDs. },
author = {Meinel, Christoph, Theobald, Thorsten},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {ordered binary decision diagrams; Boolean functions},
language = {eng},
month = {3},
number = {1},
pages = {21-31},
publisher = {EDP Sciences},
title = {On the Influence of the State Encoding on OBDD-Representations of Finite State Machines},
url = {http://eudml.org/doc/222070},
volume = {33},
year = {2010},
}

TY - JOUR
AU - Meinel, Christoph
AU - Theobald, Thorsten
TI - On the Influence of the State Encoding on OBDD-Representations of Finite State Machines
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 33
IS - 1
SP - 21
EP - 31
AB - Ordered binary decision diagrams are an important data structure for the representation of Boolean functions. Typically, the underlying variable ordering is used as an optimization parameter. When finite state machines are represented by OBDDs the state encoding can be used as an additional optimization parameter. In this paper, we analyze the influence of the state encoding on the OBDD-representations of counter-type finite state machines. In particular, we prove lower bounds, derive exact sizes for important encodings and construct a worst-case encoding which leads to exponential-size OBDDs.
LA - eng
KW - ordered binary decision diagrams; Boolean functions
UR - http://eudml.org/doc/222070
ER -

References

top
  1. A. Aziz, S. Taziran and R.K. Brayton, BDD variable ordering for interacting finite state machines, in Proc. 31st ACM/IEEE Design Automation Conference (San Diego, CA, 1994) 283-288.  
  2. J. Bern, Ch. Meinel and A. Slobodová, Global rebuilding of OBDDs - avoiding memory requirement maxima, in Proc. Computer-Aided Verification, Springer, Berlin, Lecture Notes in Computer Science939 (1995) 4-15.  
  3. B. Bollig and I. Wegener, Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput.45 (1996) 993-1002.  Zbl1048.68571
  4. R.E. Bryant, Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput.C-35 (1986) 677-691.  Zbl0593.94022
  5. R.E. Bryant, Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys24 (1992) 293-318.  
  6. J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan and D.L. Dill, Symbolic model checking for sequential circuit verification. IEEE Trans. Computer-Aided Design of Integrated Circuits13 (1994) 401-424.  
  7. O. Coudert, C. Berthet and J. C. Madre, Verification of synchronous sequential machines using symbolic execution, in Proc. Workshop on Automatic Verification Methods for Finite State Machines, Springer, Berlin, Lecture Notes in Computer Science407 (1989) 365-373.  
  8. O. Coudert and J. C. Madre, The implicit set paradigm: a new approach to finite state system verification. Formal Methods in System Design6 (1995) 133-145.  
  9. A. Ghosh, S. Devadas and A. R. Newton, Sequential logic testing and verification, Kluwer Academic Publishers, Boston, MA (1992).  
  10. R.W. Hamming, Coding and information theory, Prentice-Hall, Englewood Cliffs, NJ (1980).  Zbl0431.94001
  11. Ch. Meinel and A. Slobodová, On the complexity of constructing optimal ordered binary decision diagrams, in Proc. Mathematical Foundations in Computer Science, Springer, Berlin, Lecture Notes in Computer Science841 (1994) 515-524.  
  12. Ch. Meinel, F. Somenzi and T. Theobald, Linear sifting of decision diagrams, in Proc. 34th ACM/IEEE Design Automation Conference (Anaheim, CA, 1997) 202-207.  
  13. Ch. Meinel and T. Theobald, Local encoding transformations for optimizing OBDD-representations of finite state machines, in Proc. International Conference on Formal Methods in Computer-Aided Design (Palo Alto, CA), Springer, Berlin, Lecture Notes in Computer Science1166 (1996) 404-418.  
  14. R. Rudell, Dynamic variable ordering for ordered binary decision diagrams, in Proc. IEEE International Conference on Computer-Aided Design (Santa Clara, CA, 1993) 42-47.  
  15. S. Tani, K. Hamaguchi and S. Yajima, The complexity of the optimal variable ordering problems of shared binary decision diagrams, in Proc. International Symposium on Algorithms and Computation, Springer, Berlin, Lecture Notes in Computer Science762 (1993) 389-398.  Zbl0925.68198
  16. I. Wegener, Efficient data structures for Boolean functions. Discrete Math.136 (1994) 347-372.  Zbl0939.68597

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.