The Robotics Institute

Carnegie Mellon Robotics Institute

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Abstract

This paper presents optimizations for verifying systems with complex time-invariant constraints. These constraints arise naturally from modeling physical systems, e.g., in establishing the relationship between different components in a system. To verify constraint-rich systems, we propose two new optimizations. The first optimization is a simple, yet powerful, extension of the conjunctive-partitioning algorithm. The second is a collection of BDD-based macro-extraction and macro-expansion algorithms to remove state variables. We show that these two optimizations are essential in verifying constraint-rich problems; in particular, this work has enabled the verification of fault diagnosis models of the Nomad robot (an Antarctic meteorite explorer) and of the NASA Deep Space One spacecraft.

Keywords

Symbolic model checking, Binary Decision Diagram (BDD), time-invariant constraints, redundant state-variable elimination, macro

Notes

Number of pages: 25

Text Reference

B. Yang, Reid Simmons, R. Bryant, and D. O'Hallaron, "Optimizing Symbolic Model Checking for Constraint-Rich Models," tech. report CMU-CS-99-118, Computer Science Department, Carnegie Mellon University, March, 1999

BibTeX Reference

@techreport{Simmons_1999_2651,
   author = "B. Yang and Reid Simmons and R. Bryant and D. O'Hallaron",
   title = "Optimizing Symbolic Model Checking for Constraint-Rich Models",
   booktitle = "",
   institution = "Computer Science Department",
   month = "March",
   year = "1999",
   number= "CMU-CS-99-118",
   address= "Pittsburgh, PA",
}

The Robotics Institute

Menu