Please use this identifier to cite or link to this item:
Title: Liveness with invisible ranking
Authors: Fang, Yi
Piterman, Nir
Pnueli, Amir
Zuck, Lenore
First Published: 17-Mar-2006
Publisher: Springer Verlag
Citation: International Journal on Software Tools for Technology Transfer, 2006, 8 (3), pp. 261-279.
Abstract: The method of invisible invariants was developed originally in order to verify safety properties of parameterized systems in a fully automatic manner. The method is based on (1) a project&generalize heuristic to generate auxiliary constructs for parameterized systems and (2) a small-model theorem, implying that it is sufficient to check the validity of logical assertions of a certain syntactic form on small instantiations of a parameterized system. The approach can be generalized to any deductive proof rule that (1) requires auxiliary constructs that can be generated by project&generalize, and (2) the premises resulting when using the constructs are of the form covered by the small-model theorem. The method of invisible ranking, presented here, generalizes the approach to liveness properties of parameterized systems. Starting with a proof rule and cases where the method can be applied almost “as is,” the paper progresses to develop deductive proof rules for liveness and extend the small-model theorem to cover many intricate families of parameterized systems.
DOI Link: 10.1007/s10009-005-0193-x
ISSN: 1433-2779
eISSN: 1433-2787
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: © Springer-Verlag 2006. Deposited with reference to the publisher's archiving policy available on the SHERPA/RoMEO website. The original publication is available at
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
main.pdf291.49 kBUnknownView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.