Decidability of Parameterized Verification

Abstract

Parameterized model checking is an active research field that considers automated verification of distributed or concurrent systems, for all numbers of participating processes. In our recent book [11] we surveyed literature on decidability of parameterized verification. The system models, as well as the proof methods, that are studied in this field are similar to those from distributed computing. For instance, we survey results for token passing systems and ad hoc networks. The proof methods for undecidability include simulation of two-counter machines. For decidability, we survey cut-off results that provide conditions to reduce parameterized verification to model checking of fixed-size systems. We believe that the results are of interest to the readers of the Distributed Computing Column, and in this short note we want to give a taste of parameterized model checking.