Liveness with incomprehensible ranking

13Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

This article is free to access.

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. © Springer-Verlag 2004.

References Powered by Scopus

Limits for automatic verification of finite-state concurrent systems

311Citations
N/AReaders
Get full text

Automatic deductive verification with invisible invariants

175Citations
N/AReaders
Get full text

Reducing model checking of the many to the few

156Citations
N/AReaders
Get full text

Cited by Powered by Scopus

Model checking and abstraction to the aid of parameterized systems (a survey)

51Citations
N/AReaders
Get full text

Proving Liveness of Parameterized Programs

27Citations
N/AReaders
Get full text

Liveness with invisible ranking

20Citations
N/AReaders
Get full text

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Cite

CITATION STYLE

APA

Fang, Y., Piterman, N., Pnueli, A., & Zuck, L. (2004). Liveness with incomprehensible ranking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2988, 482–496. https://doi.org/10.1007/978-3-540-24730-2_36

Readers' Seniority

Tooltip

PhD / Post grad / Masters / Doc 4

67%

Lecturer / Post doc 2

33%

Readers' Discipline

Tooltip

Computer Science 5

83%

Mathematics 1

17%

Save time finding and organizing research with Mendeley

Sign up for free