Automating Cut-off for Multi-parameterized Systems

By: Youssef Hanna, David Samuelson, Samik Basu, and Hridesh Rajan

Download Paper
Theorem 2

Abstract

Verifying that a parameterized system satisfies certain desired properties amounts to verifying an infinite family of the system instances. This problem is undecidable in general, and as such a number of sound and incomplete techniques have been proposed to address it. Existing techniques typically focus on parameterized systems with a single parameter, (i.e., on systems where the number of processes of exactly one type is dependent on the parameter); however, many systems in practice are multi-parameterized, where multiple parameters are used to specify the number of different types of processes in the system. In this work, we present an automatic verification technique for multi-parameterized systems, prove its soundness and show that it can be applied to systems irrespective of their communication topology. We present a prototype realization of our technique in our tool Golok, and demonstrate its practical applicability using a number of multi-parameterized systems.

ACM Reference

Hanna, Y. et al. 2010. Automating Cut-off for Multi-parameterized Systems. The 12th International Conference on Formal Engineering Methods (ICFEM 2010) (Shanghai, China, Nov. 2010).

BibTeX Reference

@inproceedings{hanna2010automating,
  author = {Youssef Hanna and David Samuelson and Samik Basu and Hridesh Rajan},
  title = {Automating Cut-off for Multi-parameterized Systems},
  booktitle = {The 12th International Conference on Formal Engineering Methods (ICFEM 2010)},
  year = {2010},
  month = {November},
  address = {Shanghai, China},
  entrysubtype = {conference},
  abstract = {
    Verifying that a parameterized system satisfies certain desired properties
    amounts to verifying an infinite family of the system instances. This problem
    is undecidable in general, and as such a number of sound and incomplete
    techniques have been proposed to address it. Existing techniques typically
    focus on parameterized systems with a single parameter, (i.e., on systems
    where the number of processes of exactly one type is dependent on the
    parameter); however, many systems in practice are multi-parameterized, where
    multiple parameters are used to specify the number of different types of
    processes in the system. In this work, we present an automatic verification
    technique for multi-parameterized systems, prove its soundness and show that
    it can be applied to systems irrespective of their communication topology. We
    present a prototype realization of our technique in our tool Golok, and
    demonstrate its practical applicability using a number of multi-parameterized
    systems.
  }
}