Abstract
Binary Decision Graphs are an extension of Binary Decision Diagrams that can represent some infinite boolean functions. Three refinements of BDGs corresponding to classes of infinite functions of increasing complexity are presented. The first one is closed by intersection and union, the second one by intersection, and the last one by all boolean operations. The first two classes give rise to a canonical representation, which, when restricted to finite functions, are the classical BDDs. The paper also gives new insights in to the notion of variable names and the possibility of sharing variable names that can be of interest in the case of finite functions.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Anuchitanakul, A., Manna, Z., AND Uribe, T. E. Differential BDDs. In Computer Science Today (September 1995), J. van Leeuwen, Ed., vol. 1000 of Lecture Notes in Computer Sciencs, Springer-Verlag, pp. 218–233.
Bagnara, R. A reactive implementation of pos using ROBDDs. In 8th International Symposium on Programming Languages, Implementation, Logic and Programs (September 1996), H. Kuchen and S. D. Swierstra, Eds., vol. 1140 of Lecture Notes in Computer Science, Springer-Verlag, pp. 107–121.
Billon, J. P. Perfect normal form for discrete programs. Tech. Rep. 87039, BULL, 1987.
Bryant, R. E. Graph based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35 (August 1986), 677–691.
Bryant, R. E. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24,3 (September 1992), 293–318.
Büchi, J. R. On a decision method in restricted second order arithmetics. In International Congress on Logic, Methodology and Philosophy of Science (1960), E. Nagel et al., Eds., Stanford University Press.
Burch, J. R., Clarke, E. M., Mcmillan, K. L., Dill, D. L., AND Hwang, J. Symbolic modek checking: 1020 states and beyond. In Fifth Annual Symposium on Logic in Computer Science (June 1990).
Corsini, M.-M., Musumbi, K., AND Rauzy, A. The μ-calculus over finite domains as an abstract semantics of Prolog. In Workshop on Static Analysis (September 1992), M. Billaud, P. Castran, M.-M. Corsini, K. Musumbu, and A. Rauzy, Eds., no. 81–82 in Bigre.
Cousot, P., AND Cousot, R. Abstract interpretation; a unified lattice model for static analysis of programs by construction of approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages (POPL–77) (1977), pp. 238–252.
Fujita, M., Fujisawa, H., AND Kawato, N. Evaluation and improvements of boolean comparison method based on binary decision diagram. In International Conference on Computer-Aided Design (November 1988), IEEE, pp. 3–5.
Gupta, A., AND Fisher, A. L. Parametric circuit representation using inductive boolean functions. In Computer Aided Verification (1993), C. Courcoubetis, Ed., vol. 697 of Lecture Notes in Computer Science, Springer-Verlag, pp. 15–28.
Jeong, S.-W., Plessier, B., Hachtel, G. D., AND Somenzi, F. Variable ordering and selection for FSM traversal. In International Conference on Computer-Aided Design (November 1991), IEEE, pp. 476–479.
Le Charlier, B., And Van Hentenryck, P. Groundness analysis for Prolog: Implementation and evaluation of the domain prop. In PEPM’93 (1993).
Madre, J.-C., AND Coudert, O. A logically complete reasoning maintenance system based on a logical constraint solver. In 12th International Joint Conference on Artificial Intelligence (1991), pp. 294–299.
Manna, Z., AND Pnueli, A. The anchored version of the temporal framework. In Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency (May/June 1988), J. W. de Bakker, W. P. de Roever, and G. Rozenberg, Eds., vol. 354 of Lecture Notes in Computer Science, Springer-Verlag, pp. 201–284.
Mauborgne, L. Abstract interpretation using typed decision graphs. Science of Computer Programming 31,1 (May 1998), 91–112.
Mauborgne, L.Representation of Sets of Trees for Abstract Interpretation. PhD thesis, École Polytechnique, 1999.
Michie, D. “memo” functions and machine learning. Nature 218 (April 1968), 19–22.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mauborgne, L. (1999). Binary Decision Graphs. In: Cortesi, A., Filé, G. (eds) Static Analysis. SAS 1999. Lecture Notes in Computer Science, vol 1694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48294-6_7
Download citation
DOI: https://doi.org/10.1007/3-540-48294-6_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66459-8
Online ISBN: 978-3-540-48294-9
eBook Packages: Springer Book Archive