Abstract
The paper deals with the proof method of verification by augmented finitary abstraction (VAA), which presents an effective approach to the verification of the temporal properties of (potentially infinitestate) reactive systems. The method consists of a two-step process by which, in a first step, the system and its temporal specification are combined an then abstracted into a finite-state Büchi automaton. The second step uses model checking to establish emptiness of the abstracted automaton.
The (VAA) method can be considered as a viable alternative to verification by temporal deduction which, up to now, has been the main method shown to be complete for the verification of infinite-state systems.
The paper presents a general recipe for the abstraction of Büchi automata which is shown to be sound, where soundness means that emptiness of the abstract automaton implies emptiness of the concrete (infinitestate) automaton. To make the method applicable for the verification of liveness properties, pure abstraction is sometimes no longer adequate.We show that by augmenting the system by an appropriate (and standardly constructible) progress monitor, we obtain an augmented system, whose computations are essentially the same as the original system, and which may now be abstracted while preserving the desired liveness properties. We then proceed to show that the (VAA) method is sound and complete for proving all properties expressible by temporal logic (including both safety and liveness). Completeness establishes that whenever an infinite-state Büchi automaton has no computations, there exists a finitary abstraction which abstracts the automaton, augmented by an appropriate progress monitor, into a finite-state Büchi automaton with no computations
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Properties preserving simulations. CAV’92, LNCS 663.
N. Bjørner, I.A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. In 1st Intl. Conf. on Principles and Practice of Constraint Programming, LNCS 967, 1995.
S. Bensalem, Y. Lakhnech, and S. Owre. Abstractions of infinite state systems compositionally and automatically. CAV’98, LNCS 1427.
I.A. Browne, Z. Manna, and H.B. Sipma. Generalized verification diagrams. In FSTTSC’95, LNCS 1026.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL’77.
E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at ltl model checking. CAV’94, LNCS 818.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Trans. Prog. Lang. Sys., 16(5):1512–1542, 1994.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking. In Model Checking, Abstraction and Composition, volume 152 of Nato ASI Series F, pages 477–498. Springer-Verlag, 1996.
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. POPL’78.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Prog. Lang. Sys., 19(2), 1997.
O. Grumberg, N. Francez, J.A. Makowski, and W.-P. de Roever. A proof rule for fair termination. Inf. and Comp., 66:83–101, 1985.
S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. CAV’93, LNCS 697.
Y. Kesten and A. Pnueli. Deductive verification of fair discrete systems. Technical report, the Weizmann Institute, 1998.
Y. Kesten and A. Pnueli. Modularization and Abstraction: The Keys to Formal Verification. MFCS’98, LNCS 1450.
Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. ICALP’98, LNCS 1443.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. POPL’85.
D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In ICALP’81, LNCS 115.
Z. Manna, A. Anuchitanukul, N. Bjørner, A. Browne, E. Chang, M. Colon, L. De Alfaro, H. Devarajan, H. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, 1994.
Z. Manna, A. Brown, H. B. Sipma, and T. E. Uribe. Visual abstractions for temporal verification. AMAST’98.
Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97–130, 1991.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.
Z. Manna and A. Pnueli. Temporal verification diagrams. In Theoretical Aspects of Computer Software, LNCS 789, 1994.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
H.B. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. CAV’96.
T. E. Uribe. Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Stanford University, 1999.
M. Y. Vardi. Verification of concurrent programs-the automata-theoretic framework. Annals of Pure Applied Logic, 51:79–98, 1991.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS’86.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kesten, Y., Pnueli, A. (1999). Verifying Liveness by Augmented Abstraction. In: Flum, J., Rodriguez-Artalejo, M. (eds) Computer Science Logic. CSL 1999. Lecture Notes in Computer Science, vol 1683. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48168-0_11
Download citation
DOI: https://doi.org/10.1007/3-540-48168-0_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66536-6
Online ISBN: 978-3-540-48168-3
eBook Packages: Springer Book Archive