Abstract
Finite Automata are basic structures that appear in many areas of Computer Science and other disciplines. The emergence of new tools based on automata for the manipulation of infinite structures [4,5,1] makes a crucial challenge of improving the efficiency of automata packages. The present work is motivated by model-checking problems. where most of the algorithms are based on fixed point computations that share many identical subcomputations. A promising track is the realization of a BDD-like package because BDDs have proved these capability to take advantage of this aspect when using cache technique. Since Bryant’s original publication of BDD algorithms [2], there has been a great deal of research in the area. One of the most powerful applications of BDDs has been symbolic model checking, used to formally verify digital circuits and other finite state systems [3]. A BDD package is based on an efficient implementation of the if-then-else (ITE) operator. It uses essentially two principles:
-
(1) a hash table, called unique table, maintains a strong canonical form in BDDs and stores a forest of BDDs sharing common substructures,
-
(2) a hash table, called computed cache, keeps subresults when evaluating a recursive ITE operation.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
We’re sorry, something doesn't seem to be working properly.
Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.
References
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast Acceleration of Symbolic Transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)
Bryant, R.: Graph based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 10e20 states and beyond. Information and Computation 98(2), 97–109 (1998)
Elgaard, J., Klarlund, N., Moller, A.: Mona 1.x: new techniques for WS1S and WS2S. In: CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 1–19. Springer, Heidelberg (2000)
Yang, B., Bryant, R.E., O’Hallaron, D.R., Biere, A., Coudert, O., Janssen, G., Ranjan, R.K., Somenzi, F.: A performance study of BDD-based model checking. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 255–289. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Couvreur, JM. (2005). A BDD-Like Implementation of an Automata Package. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds) Implementation and Application of Automata. CIAA 2004. Lecture Notes in Computer Science, vol 3317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30500-2_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-30500-2_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24318-2
Online ISBN: 978-3-540-30500-2
eBook Packages: Computer ScienceComputer Science (R0)