Liveness with Incomprehensible Ranking

10 years 7 months ago
Liveness with Incomprehensible Ranking
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-projectand-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
Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Authors Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
Comments (0)