Abstract
An abstraction/refinement paradigm for the full propositional μ-calculus is presented. No distinction is made between universal or existential fragments. Necessary conditions for conservative verification are provided, along with a fully automatic symbolic model checking abstraction algorithm. The algorithm begins with conservative verification of an initial abstraction. If the conclusion is negative, it derives a “goal set” of states which require further resolution. It then successively refines, with respect to this goal set, the approximations made in the subformulas, until the given formula is verified or computational resources are exhausted.
Work supported by NSF/DARPA grant MIP-94-22268 and SRC contract 95-DJ-560.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
F. Balarin and A. L. Sangiovanni-Vincentelli. An iterative approach to language containment. In C. Courcoubetis, editor, Fifth Conference on Computer Aided Verification (CAV '93). Springer-Verlag, Berlin, 1993. LNCS 697.
R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eigth Conference on Computer Aided Verification (CAV'96), pages 428–432. Springer-Verlag, Rutgers University, 1996. LNCS 1102.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug. 1986.
J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In Proceedings of the Design Automation Conference, pages 403–407, San Francisco, CA, June 1991.
J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In Proceedings of the Design Automation Conference, pages 46–51, June 1990.
H. Cho, G. D. Hachtel, E. Macii, B. Plessier, and F. Somenzi. Algorithms for approximate FSM traversal based on state space decomposition. In Proceedings of the Design Automation Conference, pages 25–30, Dallas, TX, June 1993.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by constructions or approximation of fixpoints. In Proceedings of the ACM Symposium on the Principles of Programming Languages, pages 238–250, 1977.
M. Dam. CTL* and ECTL* as fragments of the modal μ-calculus. Theoretical Computer Science, 126: 77–97, 1994.
E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium of Logic in Computer Science, pages 267–278, June 1986.
D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation parititons. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV'94), pages 299–310, Berlin, 1994. Springer-Verlag. LNCS 818.
P. Kelb, D. Dams, and R. Gerth. Practical symbolic model checking of the full μ-calculus using compositional abstractions. Technical Report 95-31, Department of Computing Science, Eindhoven University of Technology, 1995.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.
W. Lee, A. Pardo, J. Jang, G. Hachtel, and F. Somenzi. Tearing based abstraction for CTL model checking. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 76–81, 1996.
D. E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie-Mellon University, July 1993.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.
C. Pixley, S.-W. Jeong, and G. D. Hachtel. Exact calculation of synchronization sequences based on binary decision diagrams. In Proceedings of the Design Automation Conference, pages 620–623, Anaheim, CA, June 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pardo, A., Hachtel, G.D. (1997). Automatic abstraction techniques for propositional μ-calculus model checking. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_5
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive