{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:11:20Z","timestamp":1754482280336,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028748","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"232-243","source":"Crossref","is-referenced-by-count":3,"title":["On the limitations of ordered representations of functions"],"prefix":"10.1007","author":[{"given":"Jayram S.","family":"Thathachar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"23_CR1","series-title":"Berichte aus der Informatik","first-page":"71","volume-title":"4. GI\/ITG\/GME Workshop zur Methoden des Entwurfs und der Verifikation Digitaler Systeme","author":"B. Becker","year":"1996","unstructured":"B. Becker, R. Drechsler, and R. Enders. On the computational power of bit-level and word level decision diagrams. In 4. GI\/ITG\/GME Workshop zur Methoden des Entwurfs und der Verifikation Digitaler Systeme, Berichte aus der Informatik, pages 71\u201380, Kreischa, March 1996. Shaker Verlag, Aachen."},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Amos Beimel, Francesco Bergadano, Nader H. Bshouty, Eyal Kushilevitz, and Stefano Varricchio. On the applications of multiplicity automata in learning. In 37th Annual Symposium on Foundations of Computer Science, Burlington, Vermont, 14\u201316 October 1996. IEEE.","DOI":"10.1109\/SFCS.1996.548494"},{"issue":"8","key":"23_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"23_CR4","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R. E. Bryant","year":"1991","unstructured":"R. E. Bryant. On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Transactions on Computers, 40(2):205\u2013213, February 1991.","journal-title":"IEEE Transactions on Computers"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Binary decision diagrams and beyond: Enabling technologies for formal verification. In International Conference on Computer Aided Design, pages 236\u2013245, Los Alamitos, Ca., USA, November 1995. IEEE Computer Society Press.","DOI":"10.1109\/ICCAD.1995.480018"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"R.E. Bryant and Y.-A. Chen. Verification of arithmetic circuits with binary moment diagrams. In 32nd ACM\/IEEE Design Automation Conference, Pittsburgh, June 1995.","DOI":"10.1145\/217474.217583"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"R.E. Bryant and Y.-A. Chen. Bit-level analysis of an SRT divider circuit. In 33rd ACM\/IEEE Design Automation Conference, 1996.","DOI":"10.1145\/240518.240643"},{"issue":"4","key":"23_CR8","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"J.R. Burch, E.M. Clarke, D.E. Long, K.L. MacMillan, and D.L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401\u2013424, April 1994.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"23_CR9","first-page":"1","volume-title":"Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science","author":"J.R. Burch","year":"1990","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 1\u201333, Washington, D.C., June 1990. IEEE CS Press."},{"issue":"1","key":"23_CR10","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/S0022-0000(71)80005-3","volume":"5","author":"J. W. Carlyle","year":"1971","unstructured":"J. W. Carlyle and A. Paz. Realizations by stochastic finite automata. Journal of Computer and System Sciences, 5(1):26\u201340, February 1971.","journal-title":"Journal of Computer and System Sciences"},{"key":"23_CR11","volume-title":"First International Conference on Formal Methods in Computer-Aided Design","author":"Y-A. Chen","year":"1996","unstructured":"Y-A. Chen, E. Clarke, P H. Ho, Y Hoskote, T Kam, M. Khaira, J. O' Leary, and X. Zhao. Verification of all circuits in a foating-pont unit using word-level model checking. In First International Conference on Formal Methods in Computer-Aided Design, volume 1166 of Lecture Notes Comp. Sci., pages 19\u201333, Palo Alto, CA, November 1996. Springer Verlag."},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Ying-An Chen and R.E. Bryant. +PHDD: an efficient graph representation for floating point circuit verification. In International Conference on Computer Aided Design, pages 2\u20137, Los Alamitos, Ca., USA, November 1997. IEEE Computer Society Press","DOI":"10.1109\/ICCAD.1997.643251"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"E. Clarke, K.L. McMillian, X. Zhao, M. Fujita, and J.C.-Y Yang. Spectral transforms for large boolean functions with application to technologic mapping. In 30th ACM\/IEEE Design Automation Conference, pages 54-60, Dallas, TX, June 1993.","DOI":"10.1145\/157485.164569"},{"key":"23_CR14","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume":"131","author":"E. M. Clarke","year":"1982","unstructured":"E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons from branching time temporal logic. Lecture Notes Comp. Sci., 131:52\u201371, 1982.","journal-title":"Lecture Notes Comp. Sci."},{"key":"23_CR15","first-page":"159","volume-title":"International Conference on Computer Aided Design","author":"E. M. Clarke","year":"1995","unstructured":"E. M. Clarke, M. Fujita, and X. Zhao. Hybrid decision diagrams-overcoming limitations of MTBDDs and BMDs. In International Conference on Computer Aided Design, pages 159\u2013163, Los Alamitos, CA, November 1995. IEEE Computer Society Press."},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, S. M. German, and X. Zhao. Verifying the SRT division algorithm using theorem proving techniques. Lecture Notes in Computer Science, 1102, 1996.","DOI":"10.1007\/3-540-61474-5_62"},{"issue":"4","key":"23_CR17","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"R. M. Clarke","year":"1996","unstructured":"Raymund M. Clarke and Jeanette M. Wing.Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626\u2013643, December 1996.","journal-title":"itACM Computing Surveys"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"M. Diezfelbinger, J. Hromkovic, and G. Schnitger. A comparison of two lower bound methods for communication complexity. In Symposium on Mathematical Foundations of Computer Science, pages 326\u2013335, 1994.","DOI":"10.1007\/3-540-58338-6_79"},{"key":"23_CR19","unstructured":"R. Enders. Note on the complexity of binary moment diagram representations. In IFIP WG 10.5 Workshop on Applications of Reed-Muller Expansion in Circuit Design, pages 191\u2013197, 1995."},{"key":"23_CR20","first-page":"197","volume":"53","author":"M. Fliess","year":"1974","unstructured":"M. Fliess. Matrices de Hankel. J. Math. Pures et Appl., 53:197\u2013224, 1974.","journal-title":"J. Math. Pures et Appl."},{"issue":"10","key":"23_CR21","doi-asserted-by":"publisher","first-page":"1197","DOI":"10.1109\/12.324545","volume":"43","author":"J. Gergov","year":"1994","unstructured":"J. Gergov and Ch. Meinel. Efficient boolean manipulation with OBDD's can be extended to read-once only branching programs. IEEE Transactions on Computers, 43(10):1197\u20131209, October 1994.","journal-title":"IEEE Transactions on Computers"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Andr\u00e1s Hajnal, Wolfgang Maass, and Gy\u00f6rgy Tur\u00e1n. On the communication complexity of graph properties. In Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, pages 186\u2013191, Chicago, Illinois, 2\u20134 May 1988.","DOI":"10.1145\/62212.62228"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Harju and Karhumaki. The equivalence problem of multitape finite automata. Theoretical Computer Science, 78, 1991.","DOI":"10.1016\/0304-3975(91)90356-7"},{"key":"23_CR24","volume-title":"Communication complexity","author":"E. Kushilevitz","year":"1997","unstructured":"Eyal Kushilevitz and Noam Nisan. Communication complexity. Cambridge University Press, Cambridge [England]; New York, 1997."},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"Y.-T. Lai and S. Sastry. Edge-valued binary decision diagrams for multi-level hierarchical verification. In 29th ACM\/IEEE Design Automation Conference, pages 608\u2013613, 1992.","DOI":"10.1109\/DAC.1992.227813"},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Tak Wah Lam and Larry Ruzzo. Results on communication complexity classes. Journal of Computer and System Sciences, 44, 1992.","DOI":"10.1016\/0022-0000(92)90025-E"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Thomas Lengauer. VLSI theory. In Handbook of Theoretical Computer Science, volume 1. The MIT Press\/Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88071-0.50021-7"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Richard J. Lipton and Robert Sedgewick. Lower bounds for VLSI. In Conference Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computation, pages 300\u2013307, Milwaukee, Wisconsin, 11\u201313 May 1981.","DOI":"10.1145\/800076.802482"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Kurt Mehlhorn and Erik M. Schmidt. Las Vegas is better than determinism in VLSI and distributed computing (extended abstract). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, pages 330\u2013337, San Francisco, California, May 1982.","DOI":"10.1145\/800070.802208"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"C. Papadimitriou and M. Sipser. Communication complexity. Journal of Computer and System Sciences, 28, 1984.","DOI":"10.1016\/0022-0000(84)90069-2"},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Stephen Ponzio. A lower bound for integer multiplication with read-once branching programs. In Proceedings of the Twenty-Seventh Annual ACM Symposium on Theory of Computing, pages 130\u2013139, Las Vegas, Nevada, 29 May-1 June 1995.","DOI":"10.1145\/225058.225098"},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Andrew Chi-Chih Yao. Some complexity questions related to distributive computing (preliminary report). In Conference Record of the Eleventh Annual ACM Symposium on Theory of Computing, pages 209\u2013213, Atlanta, Georgia, 30 April-2 May 1979.","DOI":"10.1145\/800135.804414"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028748","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T01:44:31Z","timestamp":1736127871000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028748"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/bfb0028748","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}