Abstract
This paper investigates the use of abstract-interpretationinspired techniques for improving the performance of procedures for determining when systems satisfy formulas in branching-time temporal logic. A framework for abstracting system descriptions is developed, and a particular method for generating abstract systems from given abstractions on system states is defined and shown to be both safe and optimal, in the sense that concrete systems satisfy all the temporal formulas enjoyed by their abstracted counterparts. One may then use a model checker on an abstracted (and hence smaller) system in order to infer properties of a concrete system.
Research supported by NSF grant CCR-9120995, ONR Young Investigator Award N00014-92-J-1582, NSF Young Investigator Award CCR-9257963, and NSF grant CCR-9402807.
Research supported in part by NSF grant CCR-9404619.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Bensalem, A. Bouajjani, C. Loiseaux and J. Sifakis. Property prerving simulations. In CAV 92, LNCS 663, 1992.
J. R. Burch, E. M. Clarke and D. E. Long. Symbolic model checking with partitioned transition relations. In VLSI 91, Edinburgh, Scotland, 1990.
E. M. Clarke, O. Grumberg and D. Long. Model checking and abstraction. In Proc of XIX POPL, Jan 1992.
R. Cleaveland, S. P. Iyer, D. Yankalevich. Abstractions for preserving all CTL* formulae Tech Report 94–03, NCSU Computer Science Department, 1994.
E. M. Clarke, E. A. Emerson and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2):244–263, 1986.
P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In VI POPL, 1979.
P. Cousot and R. Cousot. Comparing the Galois connection and the widening/narrowing approaches to abstract interpretation. In Proc of Conference on Programming Language Implementation and Logic Programming, LNCS 631, August, 1992.
D. Dams, O. Grumberg and R. Gerth. Abstract Interpretation of Reactive Systems: Abstractions Preserving ∀CTL*, ∃CTL* and CTL*. In IEEE PRO-COMONET. Nov, 1994.
E. A. Emerson and J. Y. Halpern. “Sometimes” and “not never” revisited: on branching time versus linear time temporal logic. JACM, 33(1):151–178, 1986.
N. Jones and P. Nielsen. Abstract Interpretation: a Semantic-Based Tool for Program Analysis. To appear in Handbook of Logic in Computer Science, (ed) S. Abramsky, D. Gabbay and T. S. E. Maibaum.
P. Kelb. Model Checking and Abstraction: A framework approximating both truth and failure information. University of Oldenburg, March 30, 1994.
K. Larsen. Modal Specifications. In Proc. of CAV '89, (ed) J. Sifakis, LNCS Vol. 407, pp: 232–246, 1989.
Z. Manna and A. Pnueli. Temporal Logic of Reactive and Concurrent Systems Springer-Verlag, 1992.
J. P. Quielle and J. Sifakis. Specification and Verification of Concurrent Systems in Cesar. In Proc of V International Symposium on Programming, LNCS Vol 137, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cleaveland, R., Iyer, P., Yankelevich, D. (1995). Optimality in abstractions of model checking. In: Mycroft, A. (eds) Static Analysis. SAS 1995. Lecture Notes in Computer Science, vol 983. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60360-3_32
Download citation
DOI: https://doi.org/10.1007/3-540-60360-3_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60360-3
Online ISBN: 978-3-540-45050-4
eBook Packages: Springer Book Archive