Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction

Paul Eichler, Swen Jacobs, Chana Weil-Kennedy

TL;DR

A new framework for verifying systems with a parametric number of concurrently running processes that allows for 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.

Abstract

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.

Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction

TL;DR

A new framework for verifying systems with a parametric number of concurrently running processes that allows for 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.

Abstract

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.
Paper Structure (18 sections, 25 theorems, 3 equations, 5 figures, 2 tables)

This paper contains 18 sections, 25 theorems, 3 equations, 5 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Types of Steps
  4. Reduction of Parameterized Safety Verification to the 01-CS
  5. Parameterized Reachability Problems
  6. The Cardinality Reachability Problem
  7. Deciding the CRP for $\preceq_0$-compatible Counter Systems
  8. Parameterized Model Checking of Trace Properties
  9. Transition Counter Systems
  10. Conclusion
  12. Additional Examples for Section \ref{['sec:prelim']}
  13. Additional Details for Section \ref{['sec:basic']}
  14. Additional Details for \ref{['sec:reach']}
  15. CRP
  16. ...and 3 more sections

Key Result

lemma 1

Let $\mathcal{C}=(C,Q,\mathcal{T})$ a CS, and $(c,\mathbf{v^\alpha})$ a configuration in $C \times \{0,1\}^Q$. Let $(d,\mathbf{w})$ a configuration in $C \times \mathbb{N}^Q$. Then $(c,\mathbf{v^\alpha}) \preceq_0 (d,\mathbf{w})$ if and only if $\alpha(d,\mathbf{w})=(c,\mathbf{v^\alpha})$.

Figures (5)

  • Figure 1: A lossy broadcast protocol with two controller states and three user states.
  • Figure 2: A synchronization protocol with two controller states and three user states.
  • Figure 3: Example system with spurious loop
  • Figure 4: A disjunctive system with two controller states and three user states.
  • Figure 5: An ASM system with four controller states (i.e., variable valuations) and three user states.

Theorems & Definitions (51)

  • definition 1
  • remark 1
  • definition 2
  • remark 2
  • lemma 1
  • lemma 2
  • proof
  • lemma 3
  • proof : Partial
  • lemma 4
  • ...and 41 more