Using Combinatorial Optimization Methods for Quantification Scheduling

  • P. Chauhan
  • E. Clarke
  • S. Jha
  • J. Kukula
  • H. Veith
  • D. Wang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


Model checking is the process of verifying whether a model of a concurrent system satisfies a specified temporal property. Symbolic algorithms based on Binary Decision Diagrams (BDDs) have significantly increased the size of the models that can be verified. The main problem in symbolic model checking is the image computation problem, i.e., efficiently computing the successors or predecessors of a set of states. This paper is an in-depth study of the image computation problem. We analyze and evaluate several new heuristics, metrics, and algorithms for this problem. The algorithms use combinatorial optimization techniques such as hill climbing, simulated annealing, and ordering by recursive partitioning to obtain better results than was previously the case. Theoretical analysis and systematic experimentation are used to evaluate the algorithms.


Simulated Annealing Model Check Boolean Function Transition Relation Simulated Annealing Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [BCL91a]
    J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in Symbolic Model Checking. In 28th ACM/IEEE Design Automation Conference, 1991.Google Scholar
  2. [BCL91b]
    J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic Model Checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proceedings of the International Conference on Very Large Scale Int egration, Edinburgh, Scotland, August 1991.Google Scholar
  3. [B’e92]
    C. J. P. B’elisle. Convergence theorems for a class of simulated annealing algorithms. Journal of Applied Probability, 29:885–892, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [BJ92]
    T. N. Bui and C. Jones. Finding good approximate vertex and edge partitions is NP-hard. Information Processing Letters, 42:153–159, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [CCGR99]
    A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, Proceedings of International Conference on Computer-Aided Verification (CAV’99), number 1633 in Lecture Notes in Computer Science, pages 495–499. Springer, July 1999.Google Scholar
  6. [CGP00]
    E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.Google Scholar
  7. [FM82]
    C.M. Fiduccia and R.M. Mattheyses. A linear time heuristic for improving network partitions. In 19th ACM/IEEE Design Automation Conference, pages 175–181, 1982.Google Scholar
  8. [GB94]
    D. Geist and I. Beer. Efficient Model Checking by automated ordering of transition relation partitions. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV’94), volume 818 of LNCS, pages 299–310, Stanford, CA, USA, 1994. Springer-Verlag.Google Scholar
  9. [GJ79]
    Michael R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., 1979.Google Scholar
  10. [Haj85]
    B. Hajek. A tutorial survey of theory and applications of simulated annealing. In Proc. 24th IEEE Conf. Decision and Control, pages 755–760, 1985.Google Scholar
  11. [KJV83]
    S. Kirkpatrick, C. D. Gelatt Jr., and M. P. Vecchi. Optimization by simulated annealing. Science, 220:671–679, 1983.CrossRefMathSciNetGoogle Scholar
  12. [KL70]
    Brian Kernighan and S. Lin. An efficient heuristic procedure for partitioning graphs. The Bell System Technical Journal, pages 291–307, February 1970.Google Scholar
  13. [MKRS00]
    In-Ho Moon, James H. Kukula, Kavita Ravi, and Fabio Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the 37th Design Automation Conference (DAC’00), pages 26–28, Los Angeles, June 2000.Google Scholar
  14. [MRR+53]
    N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, and E. Teller. Equation of state calculations by fast computing machines. Journal of Chemical Phyics, 21(6):1087–1092, 1953.CrossRefGoogle Scholar
  15. [MS00]
    In-Ho Moon and Fabio Somenzi. Border-block triangular form and conjunction schedule in image computation. In Warren A. Hunt Jr. and Steven D. Johnson, editors, Proceedings of the Formal Methods in Computer Aided Design (FMCAD’00), volume 1954 of LNCS, pages 73–90, November 2000.CrossRefGoogle Scholar
  16. [RAP+95]
    R.K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R.K. Brayton. Efficient BDD algorithms for FSM synthesis and verification. In IEEE/ACM International Workshop on Logic Synthesis, Lake Tahoe, 1995. IEEE/ACM.Google Scholar
  17. [TSL+90]
    H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDDs. In Proceedings of the IEEE international Conference on Computer Aided Design (ICCAD), pages 130–133, November 1990.Google Scholar
  18. [Yan99]
    Bwolen Yang. Optimizing Model Checking Based on BDD Characterization. PhD thesis, Carnegie Mellon University, Computer Science Department, May 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • P. Chauhan
    • 1
  • E. Clarke
    • 1
  • S. Jha
    • 2
  • J. Kukula
    • 3
  • H. Veith
    • 4
  • D. Wang
    • 1
  1. 1.Carnegie Mellon UniversityItaly
  2. 2.University of WisconsinMadison
  3. 3.Synopsys Inc.USA
  4. 4.TU ViennaAustria

Personalised recommendations