Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
This work addresses the problem of parameterized verification for concurrent systems, offering a unified approach that is incremental but extends and improves on prior results.
The authors tackled the problem of verifying systems with a parametric number of concurrent processes by introducing a framework based on well-structured systems and a 01-counter abstraction, which allows deciding verification problems like control-state reachability and coverability in a fixed finite abstraction. They showed that this framework applies to various systems from the literature, including reconfigurable broadcast networks and disjunctive systems, providing a unified explanation and extending existing results.
We introduce a new framework for verifying systems with a parametric number of concurrently running processes. The systems we consider are well-structured with respect to a specific well-quasi order. This allows us to decide a wide range of verification problems, including control-state reachability, coverability, and target, in a fixed finite abstraction of the infinite state-space, called a 01-counter system. We show that several systems from the parameterized verification literature fall into this class, including reconfigurable broadcast networks (or systems with lossy broadcast), disjunctive systems, synchronizations and systems with a fixed number of shared finite-domain variables. Our framework provides a simple and unified explanation for the properties of these systems, which have so far been investigated separately. Additionally, it extends and improves on a range of the existing results, and gives rise to other systems with similar properties.