Liveness with incomprehensible ranking

Yi Fang, Nir Piterman, Amir Pnueli, Lenore Zuck

    Research output: Contribution to journalArticle

    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.

    Original languageEnglish (US)
    Pages (from-to)482-496
    Number of pages15
    JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume2988
    StatePublished - Dec 1 2004

    Fingerprint

    Liveness
    Ranking
    Assertion
    Ranking Function
    Topology
    Auxiliary Variables
    Simplify
    Model
    Heuristics
    Sufficient
    Verify
    Ring
    Generalise
    Invariant
    Theorem

    ASJC Scopus subject areas

    • Theoretical Computer Science
    • Computer Science(all)

    Cite this

    Liveness with incomprehensible ranking. / Fang, Yi; Piterman, Nir; Pnueli, Amir; Zuck, Lenore.

    In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 2988, 01.12.2004, p. 482-496.

    Research output: Contribution to journalArticle

    @article{c4dbe21a104b46e1bd5a8972684bdabe,
    title = "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-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.",
    author = "Yi Fang and Nir Piterman and Amir Pnueli and Lenore Zuck",
    year = "2004",
    month = "12",
    day = "1",
    language = "English (US)",
    volume = "2988",
    pages = "482--496",
    journal = "Lecture Notes in Computer Science",
    issn = "0302-9743",
    publisher = "Springer Verlag",

    }

    TY - JOUR

    T1 - Liveness with incomprehensible ranking

    AU - Fang, Yi

    AU - Piterman, Nir

    AU - Pnueli, Amir

    AU - Zuck, Lenore

    PY - 2004/12/1

    Y1 - 2004/12/1

    N2 - 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.

    AB - 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.

    UR - http://www.scopus.com/inward/record.url?scp=35048869668&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=35048869668&partnerID=8YFLogxK

    M3 - Article

    VL - 2988

    SP - 482

    EP - 496

    JO - Lecture Notes in Computer Science

    JF - Lecture Notes in Computer Science

    SN - 0302-9743

    ER -