Abstract
The methods of Invisible Invariants and Invisible Ranking were developed originally in order to verify temporal properties of parameterized systems in a fully automatic manner. These methods are based on an instantiate-project-and-generalize heuristic for the automatic generation of auxiliary constructs and a small model property implying that it is sufficient to check validity of a deductive rule premises using these constructs on small instantiations of the system. The previous version of the method of Invisible Ranking was restricted to cases where the helpful assertions and ranking functions for a process depended only on the local state of this process and not on any neighboring process, which seriously restricted the applicability of the method, and often required the introduction of auxiliary variables.
In this paper we extend the method of Invisible Ranking to cases where the helpful assertions and ranking functions of a process may also refer to other processes. We first develop an enhanced version of the small model property, making it applicable to assertions that refer both to processes and their immediate neighbors. This enables us to apply the Invisible Ranking method to parameterized systems with ring topologies. For cases where the auxiliary assertions refer to all processes, we develop a novel proof rule which simplifies the selection of the next helpful transition, and enables the validation of the premises possible under the (old) small model theorem.
This research was supported in part by NSF grant CCR-0205571, ONR grant N000140310916, the Minerva Center for Verification of Reactive Systems, the European Community IST project “Advance”, and the Israel Science Foundation grant 106/02-1.
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
Apt, K.R., Kozen, D.: Limits for automatic program verification of finite-state concurrent systems. IPL 22(6) (1986)
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 221. Springer, Heidelberg (2001)
Bjørner, N., Browne, I.A., Chang, E., Colón, M., Kapur, A., Manna, Z., Sipma, H.B., Uribe, T.E.: STeP: The Stanford Temporal Prover, User’s Manual. Technical Report STAN-CS-TR-95-1562, CS Department, Stanford University (November 1995)
Clarke, E.M., Grumberg, O., Jha, S.: Verifying parametrized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 395–407. Springer, Heidelberg (1995)
Colon, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442–454. Springer, Heidelberg (2002)
Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 236–255. Springer, Heidelberg (2000)
Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: 22nd POPL (1995)
Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with invisible ranking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 223–238. Springer, Heidelberg (2004)
Gyuris, V., Sistla, A.P.: On-the-fly model checking under fairness that exploits symmetry. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 424–438. Springer, Heidelberg (1998)
Gribomont, E.P., Zenner, G.: Automated verification of szymanski’s algorithm. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, p. 220. Springer, Heidelberg (2000)
Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 381–392. Springer, Heidelberg (2003)
Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: 24th POPL (1997)
McMillan, K.L.: Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 110–121. Springer, Heidelberg (1998)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety (1995)
Owre, S., Shankar, N., Rushby, J.M.: User guide for the PVS specification and verification system (draft). Tech. report, CS Lab., SRI International, CA (1993)
Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)
Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1,∞)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002)
Shahar, E.: The TLV Manual (2000), http://www.wisdom.weizmann.ac.il/~verify/tlv
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fang, Y., Piterman, N., Pnueli, A., Zuck, L. (2004). Liveness with Incomprehensible Ranking. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_36
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive